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 (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (ap x2 x3)) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x3) (ap x2 x4)) ⟶ 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_decr_upper_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 (add_SNo (ap x3 x4) (minus_SNo (eps_ x4))) x0) (SNoLt x0 (ap x3 x4))) (∀ x5 . x5 ∈ x4 ⟶ SNoLt (ap x3 x4) (ap x3 x5)))) x2.

Apply H9 with x1.

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

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

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 (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0 leaving 2 subgoals.

The subproof is completed by applying H12.

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

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

Apply H13 with SNoLt (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0.

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

Assume H16: SNoLt x0 ....

...

■

Proofgold Proof