Search for blocks/addresses/...

Proofgold Proof

pf
Apply explicit_OrderedField_I with real, 0, 1, add_SNo, mul_SNo, SNoLe leaving 6 subgoals.
The subproof is completed by applying explicit_Field_real.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Let x2 of type ι be given.
Assume H2: x2 ∈ real.
Apply SNoLe_tra with x0, x1, x2 leaving 3 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Apply real_SNo with x2.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Apply iffI with and (SNoLe x0 x1) (SNoLe x1 x0), x0 = x1 leaving 2 subgoals.
Assume H2: and (SNoLe x0 x1) (SNoLe x1 x0).
Apply H2 with x0 = x1.
Apply SNoLe_antisym with x0, x1 leaving 2 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Assume H2: x0 = x1.
Apply H2 with λ x2 x3 . and (SNoLe x3 x1) (SNoLe x1 x3).
Apply andI with SNoLe x1 x1, SNoLe x1 x1 leaving 2 subgoals.
The subproof is completed by applying SNoLe_ref with x1.
The subproof is completed by applying SNoLe_ref with x1.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Apply SNoLtLe_or with x0, x1, or (SNoLe x0 x1) (SNoLe x1 x0) leaving 4 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Assume H2: SNoLt x0 x1.
Apply orIL with SNoLe x0 x1, SNoLe x1 x0.
Apply SNoLtLe with x0, x1.
The subproof is completed by applying H2.
Assume H2: SNoLe x1 x0.
Apply orIR with SNoLe x0 x1, SNoLe x1 x0.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Let x2 of type ι be given.
Assume H2: x2 ∈ real.
Apply add_SNo_Le1 with x0, x2, x1 leaving 3 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
Apply real_SNo with x2.
The subproof is completed by applying H2.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Assume H2: SNoLe 0 x0.
Assume H3: SNoLe 0 x1.
Apply mul_SNo_zeroR with x0, λ x2 x3 . SNoLe x2 (mul_SNo x0 x1) leaving 2 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
Apply nonneg_mul_SNo_Le with x0, 0, x1 leaving 5 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying SNo_0.
Apply real_SNo with x1.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
■