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.
The subproof is completed by applying orIR with SNoLe x0 x1, SNoLe x1 x0.
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 SNoLeE with 0, x0, SNoLe 0 (mul_SNo x0 x1) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
Apply real_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Assume H4: SNoLt 0 x0.
Apply SNoLeE with 0, x1, SNoLe 0 (mul_SNo x0 x1) leaving 5 subgoals.
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.
Assume H5: SNoLt 0 x1.
Apply SNoLtLe with 0, mul_SNo x0 x1.
Apply mul_SNo_pos_pos with x0, x1 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.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H5: 0 = x1.
Apply H5 with λ x2 x3 . SNoLe 0 (mul_SNo x0 x2).
Apply mul_SNo_zeroR with x0, λ x2 x3 . SNoLe 0 x3 leaving 2 subgoals.
Apply real_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNoLe_ref with 0.
Assume H4: 0 = x0.
Apply H4 with λ x2 x3 . SNoLe 0 (mul_SNo x2 x1).
Apply mul_SNo_zeroL with x1, λ x2 x3 . SNoLe 0 x3 leaving 2 subgoals.
Apply real_SNo with x1.
The subproof is completed by applying H1.
The subproof is completed by applying SNoLe_ref with 0.
■