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 x0 x1.
Apply real_E with x1, ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x0 x2) (SNoLt x2 x1)) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: SNo x1.
Assume H4: SNoLev x1 ∈ ordsucc omega.
Assume H5: x1 ∈ SNoS_ (ordsucc omega).
Assume H6: SNoLt (minus_SNo omega) x1.
Assume H7: SNoLt x1 omega.
Assume H8: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x1))) (eps_ x3)) ⟶ x2 = x1.
Assume H9: ∀ x2 . x2 ∈ omega ⟶ ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x1) (SNoLt x1 (add_SNo x3 (eps_ x2)))).
Claim L10: ...
...
Apply real_pos_eps_ with add_SNo x1 (minus_SNo x0), ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x0 x2) (SNoLt x2 x1)) leaving 3 subgoals.
Apply real_add_SNo with x1, minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply real_minus_SNo with x0.
The subproof is completed by applying H0.
Apply add_SNo_minus_Lt2b with x1, x0, 0 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with x0, λ x2 x3 . SNoLt x3 x1 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H11: (λ x3 . and (x3 ∈ omega) (SNoLt (eps_ x3) (add_SNo x1 (minus_SNo x0)))) x2.
Apply H11 with ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x0 x3) (SNoLt x3 x1)).
Assume H12: x2 ∈ omega.
Assume H13: SNoLt (eps_ x2) (add_SNo x1 (minus_SNo x0)).
Apply H9 with x2, ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x0 x3) (SNoLt x3 x1)) leaving 2 subgoals.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H14: (λ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x1) (SNoLt x1 (add_SNo x4 (eps_ x2))))) x3.
Apply H14 with ∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x0 x4) (SNoLt x4 x1)).
Assume H15: x3 ∈ SNoS_ omega.
Assume H16: and (SNoLt x3 x1) (SNoLt x1 (add_SNo x3 (eps_ x2))).
Apply H16 with ∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x0 x4) (SNoLt x4 x1)).
Assume H17: SNoLt x3 x1.
Assume H18: SNoLt x1 (add_SNo x3 (eps_ x2)).
Apply SNoS_E2 with omega, x3, ∃ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x0 x4) (SNoLt x4 x1)) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H15.
Assume H19: SNoLev x3 ∈ omega.
Assume H20: ordinal (SNoLev ...).
...
■