Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNoLt 0 x0.
Assume H1: SNoLt 0 x1.
Assume H2: not (mul_SNo x0 x1 ∈ real).
Assume H3: SNo x0.
Assume H4: x0 ∈ SNoS_ (ordsucc omega).
Assume H5: SNoLt x0 omega.
Assume H6: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0.
Assume H7: SNo x1.
Assume H8: SNoLev x1 ∈ ordsucc omega.
Assume H9: x1 ∈ SNoS_ (ordsucc omega).
Assume H10: SNoLt x1 omega.
Assume H11: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x1))) (eps_ x3)) ⟶ x2 = x1.
Assume H12: ∀ x2 . x2 ∈ omega ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt 0 x4 ⟶ SNoLt x4 x0 ⟶ SNoLt x0 (add_SNo x4 (eps_ x2)) ⟶ x3) ⟶ x3.
Assume H13: ∀ x2 . x2 ∈ omega ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt 0 x4 ⟶ SNoLt x4 x1 ⟶ SNoLt x1 (add_SNo x4 (eps_ x2)) ⟶ x3) ⟶ x3.
Assume H14: SNo (mul_SNo x0 x1).
Assume H15: SNo (minus_SNo (mul_SNo x0 x1)).
Assume H16: nIn (SNoLev (mul_SNo x0 x1)) omega.
Assume H17: ∀ x2 . SNo x2 ⟶ SNoLev x2 ∈ omega ⟶ SNoLev x2 ∈ SNoLev (mul_SNo x0 x1).
Apply H2.
Apply real_mul_SNo with x0, x1 leaving 2 subgoals.
Apply real_I with x0 leaving 4 subgoals.
The subproof is completed by applying H4.
Assume H18: x0 = omega.
Apply SNoLt_irref with x0.
Apply H18 with λ x2 x3 . SNoLt x0 x3.
The subproof is completed by applying H5.
Assume H18: x0 = minus_SNo omega.
Apply SNoLt_irref with x0.
Apply H18 with λ x2 x3 . SNoLt x3 x0.
Apply SNoLt_tra with minus_SNo omega, 0, x0 leaving 5 subgoals.
Apply SNo_minus_SNo with omega.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H3.
Apply minus_SNo_Lt_contra1 with 0, omega leaving 3 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_omega.
Apply minus_SNo_0 with λ x2 x3 . SNoLt x3 omega.
Apply ordinal_In_SNoLt with omega, 0 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
Apply real_I with x1 leaving 4 subgoals.
Apply SNoS_I with ordsucc omega, x1, SNoLev x1 leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H8.
Apply SNoLev_ with x1.
The subproof is completed by applying H7.
Assume H18: x1 = omega.
Apply SNoLt_irref with x1.
Apply H18 with λ x2 x3 . SNoLt x1 x3.
The subproof is completed by applying H10.
Assume H18: x1 = minus_SNo omega.
Apply SNoLt_irref with x1.
Apply H18 with λ x2 x3 . SNoLt x3 x1.
Apply SNoLt_tra with minus_SNo omega, 0, x1 leaving 5 subgoals.
Apply SNo_minus_SNo with omega.
The subproof is completed by applying SNo_omega.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H7.
Apply minus_SNo_Lt_contra1 with 0, omega leaving 3 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_omega.
Apply minus_SNo_0 with λ x2 x3 . SNoLt x3 omega.
Apply ordinal_In_SNoLt with omega, 0 leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
The subproof is completed by applying H1.
The subproof is completed by applying H11.
■