Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply real_SNo with
x0.
The subproof is completed by applying H0.
Apply SNoLt_trichotomy_or_impred with
x0,
0,
∃ x1 . and (x1 ∈ real) (mul_SNo x0 x1 = 1) leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply pos_real_recip_ex with
minus_SNo x0,
∃ x1 . and (x1 ∈ real) (mul_SNo x0 x1 = 1) leaving 3 subgoals.
Apply real_minus_SNo with
x0.
The subproof is completed by applying H0.
Apply minus_SNo_Lt_contra2 with
x0,
0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply minus_SNo_0 with
λ x1 x2 . SNoLt x0 x2.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply H4 with
∃ x2 . and (x2 ∈ real) (mul_SNo x0 x2 = 1).
Let x2 of type ο be given.
Apply H7 with
minus_SNo x1.
Apply andI with
minus_SNo x1 ∈ real,
mul_SNo x0 (minus_SNo x1) = 1 leaving 2 subgoals.
Apply real_minus_SNo with
x1.
The subproof is completed by applying H5.
Apply mul_SNo_minus_distrR with
x0,
x1,
λ x3 x4 . x4 = 1 leaving 3 subgoals.
The subproof is completed by applying L2.
Apply real_SNo with
x1.
The subproof is completed by applying H5.
Apply mul_SNo_minus_distrL with
x0,
x1,
λ x3 x4 . x3 = 1 leaving 3 subgoals.
The subproof is completed by applying L2.
Apply real_SNo with
x1.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H3: x0 = 0.
Apply FalseE with
∃ x1 . and (x1 ∈ real) (mul_SNo x0 x1 = 1).
Apply H1.
The subproof is completed by applying H3.
Apply pos_real_recip_ex with
x0.
The subproof is completed by applying H0.