Let x0 of type ι be given.

Assume H0: x0 ∈ real.

Let x1 of type ο be given.

Assume H1: ∀ x2 . x2 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x2 x3) x0) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3))) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x4) (ap x2 x3)) ⟶ x1.

Apply real_E with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: SNo x0.

Assume H3: SNoLev x0 ∈ ordsucc omega.

Assume H4: x0 ∈ SNoS_ (ordsucc omega).

Assume H6: SNoLt x0 omega.

Assume H7: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0.

Assume H8: ∀ x2 . x2 ∈ omega ⟶ ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x2)))).

Apply SNo_prereal_incr_lower_approx with x0, x1 leaving 4 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

Let x2 of type ι be given.

Assume H9: (λ x3 . and (x3 ∈ setexp (SNoS_ omega) omega) (∀ x4 . x4 ∈ omega ⟶ and (and (SNoLt (ap x3 x4) x0) (SNoLt x0 (add_SNo (ap x3 x4) (eps_ x4)))) (∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x5) (ap x3 x4)))) x2.

Apply H9 with x1.

Assume H10: x2 ∈ setexp (SNoS_ omega) omega.

Assume H11: ∀ x3 . x3 ∈ omega ⟶ and (and (SNoLt (ap x2 x3) x0) (SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3)))) (∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x4) (ap x2 x3)).

Apply H1 with x2 leaving 4 subgoals.

The subproof is completed by applying H10.

Let x3 of type ι be given.

Assume H12: x3 ∈ omega.

Apply H11 with x3, SNoLt (ap x2 x3) x0 leaving 2 subgoals.

The subproof is completed by applying H12.

Assume H13: and (SNoLt (ap x2 x3) x0) (SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3))).

Assume H14: ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x4) (ap x2 x3).

Apply H13 with SNoLt (ap x2 x3) x0.

Assume H15: SNoLt (ap x2 x3) x0.

Assume H16: SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3)).

The subproof is completed by applying H15.

Let x3 of type ι be given.

Assume H12: x3 ∈ omega.

Apply H11 with x3, SNoLt x0 ... leaving 2 subgoals.

...

■

Proofgold Proof