Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Assume H2: SNoLt 0 x0.
Assume H3: SNoLt 0 x1.
Apply dneg with mul_SNo x0 x1 ∈ real.
Assume H4: nIn (mul_SNo x0 x1) real.
Apply real_E with x0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H5: SNo x0.
Assume H6: SNoLev x0 ∈ ordsucc omega.
Assume H7: x0 ∈ SNoS_ (ordsucc omega).
Assume H8: SNoLt (minus_SNo omega) x0.
Assume H9: SNoLt x0 omega.
Assume H10: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0.
Assume H11: ∀ x2 . x2 ∈ omega ⟶ ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x2)))).
Apply real_E with x1, False leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H12: SNo x1.
Assume H13: SNoLev x1 ∈ ordsucc omega.
Assume H14: x1 ∈ SNoS_ (ordsucc omega).
Assume H15: SNoLt (minus_SNo omega) x1.
Assume H16: SNoLt x1 omega.
Assume H17: ∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x1))) (eps_ x3)) ⟶ x2 = x1.
Assume H18: ∀ x2 . x2 ∈ omega ⟶ ∃ x3 . and (x3 ∈ SNoS_ omega) (and (SNoLt x3 x1) (SNoLt x1 (add_SNo x3 (eps_ x2)))).
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Apply mul_SNo_eq_3 with x0, x1, False leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H12.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H27: SNoCutP x2 x3.
Assume H28: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ x5.
Assume H29: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.
Assume H30: ∀ x4 . x4 ∈ ... ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.
...
■