Search for blocks/addresses/...

Proofgold Proof

pf
Apply explicit_Reals_I with real, 0, 1, add_SNo, mul_SNo, SNoLe leaving 3 subgoals.
The subproof is completed by applying explicit_OrderedField_real.
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Assume H2: lt real 0 1 add_SNo mul_SNo SNoLe 0 x0.
Apply unknownprop_cc21bb1b7a793fd178643e5fcc401b6255545a0d3dee389d449d3dddcddcfb20 with λ x2 x3 . SNoLe 0 x1 ⟶ ∃ x4 . and (x4 ∈ x3) (SNoLe x1 (mul_SNo x4 x0)).
Apply real_Archimedean with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with SNoLt 0 x0.
Assume H3: SNoLe 0 x0.
Assume H4: 0 = x0 ⟶ ∀ x2 : ο . x2.
Apply SNoLeE with 0, x0, SNoLt 0 x0 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 H3.
Assume H5: SNoLt 0 x0.
The subproof is completed by applying H5.
Assume H5: 0 = x0.
Apply FalseE with SNoLt 0 x0.
Apply H4.
The subproof is completed by applying H5.
Apply unknownprop_cc21bb1b7a793fd178643e5fcc401b6255545a0d3dee389d449d3dddcddcfb20 with λ x0 x1 . ∀ x2 . x2 ∈ setexp real x1 ⟶ ∀ x3 . x3 ∈ setexp real x1 ⟶ (∀ x4 . x4 ∈ x1 ⟶ and (and (SNoLe (ap x2 x4) (ap x3 x4)) (SNoLe (ap x2 x4) (ap x2 (add_SNo x4 1)))) (SNoLe (ap x3 (add_SNo x4 1)) (ap x3 x4))) ⟶ ∃ x4 . and (x4 ∈ real) (∀ x5 . x5 ∈ x1 ⟶ and (SNoLe (ap x2 x5) x4) (SNoLe x4 (ap x3 x5))).
The subproof is completed by applying real_complete2.
■