Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H1: (λ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x2) x3))) x1.

Assume H2: x1 ∈ omega.

Assume H3: ∃ x2 . and (x2 ∈ int) (x0 = mul_SNo (eps_ x1) x2).

Let x2 of type ι be given.

Assume H4: (λ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x1) x3)) x2.

Assume H5: x2 ∈ int.

Assume H6: x0 = mul_SNo (eps_ x1) x2.

Let x3 of type ο be given.

Assume H7: ∀ x4 . and (x4 ∈ omega) (∃ x5 . and (x5 ∈ int) (minus_SNo x0 = mul_SNo (eps_ x4) x5)) ⟶ x3.

Apply H7 with x1.

Apply andI with x1 ∈ omega, ∃ x4 . and (x4 ∈ int) (minus_SNo x0 = mul_SNo (eps_ x1) x4) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x4 of type ο be given.

Assume H8: ∀ x5 . and (x5 ∈ int) (minus_SNo x0 = mul_SNo (eps_ x1) x5) ⟶ x4.

Apply H8 with minus_SNo x2.

Apply andI with minus_SNo x2 ∈ int, minus_SNo x0 = mul_SNo (eps_ x1) (minus_SNo x2) leaving 2 subgoals.

Apply int_minus_SNo with x2.

The subproof is completed by applying H5.

Apply mul_SNo_minus_distrR with eps_ x1, x2, λ x5 x6 . minus_SNo x0 = x6 leaving 3 subgoals.

Apply SNo_eps_ with x1.

The subproof is completed by applying H2.

Apply int_SNo with x2.

The subproof is completed by applying H5.

set y5 to be minus_SNo (mul_SNo (eps_ x1) x2)

Claim L9: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (minus_SNo x0)

Let x6 of type ι → ο be given.

The subproof is completed by applying H6 with λ x7 x8 . (λ x9 . x6) (minus_SNo x7) (minus_SNo x8).

Let x6 of type ι → ι → ο be given.

Apply L9 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H10: x6 y5 y5.

The subproof is completed by applying H10.

■

Proofgold Proof