Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Assume H2: SNoLt 0 x0.
Assume H3: SNoLe 0 x1.
Apply real_E with x0, ∃ x2 . and (x2 ∈ omega) (SNoLe x1 (mul_SNo x2 x0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H4: SNo x0.
Assume H5: SNoLev x0 ∈ ordsucc omega.
Assume H6: x0 ∈ SNoS_ (ordsucc omega).
Assume H7: SNoLt (minus_SNo omega) x0.
Assume H8: SNoLt x0 omega.
Assume H9: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0.
Assume H10: ∀ x2 . x2 ∈ omega ⟶ ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x2)))).
Claim L11: ...
...
Apply L11 with ∃ x2 . and (x2 ∈ omega) (SNoLe x1 (mul_SNo x2 x0)).
Let x2 of type ι be given.
Assume H12: (λ x3 . and (x3 ∈ omega) (SNoLe (eps_ x3) x0)) x2.
Apply H12 with ∃ x3 . and (x3 ∈ omega) (SNoLe x1 (mul_SNo x3 x0)).
Assume H13: x2 ∈ omega.
Assume H14: SNoLe (eps_ x2) x0.
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Apply real_E with x1, ∃ x3 . and (x3 ∈ omega) (SNoLe x1 (mul_SNo x3 x0)) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H19: SNo x1.
Assume H20: SNoLev x1 ∈ ordsucc omega.
Assume H21: x1 ∈ SNoS_ (ordsucc omega).
Assume H22: SNoLt (minus_SNo omega) x1.
Assume H23: SNoLt x1 omega.
Assume H24: ∀ x3 . x3 ∈ SNoS_ omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x3 (minus_SNo x1))) (eps_ x4)) ⟶ x3 = x1.
Assume H25: ∀ x3 . x3 ∈ omega ⟶ ∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x1) (SNoLt x1 (add_SNo x4 (eps_ x3)))).
Apply SNoS_ordsucc_omega_bdd_above with x1, ∃ x3 . and (x3 ∈ omega) (SNoLe x1 (mul_SNo x3 x0)) leaving 3 subgoals.
The subproof is completed by applying H21.
The subproof is completed by applying H23.
Let x3 of type ι be given.
Assume H26: (λ x4 . and (x4 ∈ omega) (SNoLt x1 x4)) x3.
Apply H26 with ∃ x4 . and (x4 ∈ omega) (SNoLe x1 (mul_SNo x4 x0)).
Assume H27: x3 ∈ omega.
Assume H28: SNoLt x1 x3.
Let x4 of type ο be given.
Assume H29: ∀ x5 . and (x5 ∈ omega) (SNoLe x1 (mul_SNo x5 x0)) ⟶ x4.
Apply H29 with mul_SNo x3 (exp_SNo_nat 2 x2).
Apply andI with mul_SNo x3 (exp_SNo_nat 2 x2) ∈ omega, SNoLe ... ... leaving 2 subgoals.
...
...
■