Let x0 of type ι be given.
Apply SepE with
real,
λ x1 . ∃ x2 . and (x2 ∈ int) (∃ x3 . and (x3 ∈ setminus omega (Sing 0)) (x1 = div_SNo x2 x3)),
x0,
minus_SNo x0 ∈ rational leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H2 with
minus_SNo x0 ∈ rational.
Let x1 of type ι be given.
Apply H3 with
minus_SNo x0 ∈ rational.
Apply H5 with
minus_SNo x0 ∈ rational.
Let x2 of type ι be given.
Apply H6 with
minus_SNo x0 ∈ rational.
Apply setminusE with
omega,
Sing 0,
x2,
minus_SNo x0 ∈ rational leaving 2 subgoals.
The subproof is completed by applying H7.
Apply SepI with
real,
λ x3 . ∃ x4 . and (x4 ∈ int) (∃ x5 . and (x5 ∈ setminus omega (Sing 0)) (x3 = div_SNo x4 x5)),
minus_SNo x0 leaving 2 subgoals.
Apply real_minus_SNo with
x0.
The subproof is completed by applying H1.
Let x3 of type ο be given.
Apply H12 with
minus_SNo x1.
Apply andI with
minus_SNo x1 ∈ int,
∃ x4 . and (x4 ∈ setminus omega (Sing 0)) (minus_SNo x0 = div_SNo (minus_SNo x1) x4) leaving 2 subgoals.
Apply int_minus_SNo with
x1.
The subproof is completed by applying H4.
Let x4 of type ο be given.
Apply H13 with
x2.
Apply andI with
x2 ∈ setminus omega (Sing 0),
minus_SNo x0 = div_SNo (minus_SNo x1) x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply mul_SNo_nonzero_cancel with
x2,
minus_SNo x0,
div_SNo (minus_SNo x1) x2 leaving 5 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L14.
Apply real_SNo with
minus_SNo x0.
Apply real_minus_SNo with
x0.
The subproof is completed by applying H1.
Apply SNo_div_SNo with
minus_SNo x1,
x2 leaving 2 subgoals.
Apply int_SNo with
minus_SNo x1.
Apply int_minus_SNo with
x1.
The subproof is completed by applying H4.
The subproof is completed by applying L11.
set y5 to be ...
Let x6 of type ι → ι → ο be given.
Apply L15 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H16: x6 y5 y5.