Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Apply nonzero_real_recip_ex with add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)), ∃ x1 . and (x1 ∈ complex) (mul_CSNo x0 x1 = 1) leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7: add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)) = 0.
Apply H1.
Apply CSNo_ReIm_split with x0, 0 leaving 4 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
Apply Re_0 with λ x1 x2 . CSNo_Re x0 = x2.
Apply SNo_zero_or_sqr_pos with CSNo_Re x0, CSNo_Re x0 = 0 leaving 3 subgoals.
Apply real_SNo with CSNo_Re x0.
The subproof is completed by applying L2.
Assume H8: CSNo_Re x0 = 0.
The subproof is completed by applying H8.
Assume H8: SNoLt 0 (mul_SNo (CSNo_Re x0) (CSNo_Re x0)).
Apply FalseE with CSNo_Re x0 = 0.
Apply SNoLt_irref with 0.
Apply H7 with λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with 0, mul_SNo (CSNo_Re x0) (CSNo_Re x0), add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
Apply real_SNo with add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)).
The subproof is completed by applying L6.
The subproof is completed by applying H8.
Apply add_SNo_0R with mul_SNo (CSNo_Re x0) (CSNo_Re x0), λ x1 x2 . SNoLe x1 (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0))) leaving 2 subgoals.
The subproof is completed by applying L4.
Apply add_SNo_Le2 with mul_SNo (CSNo_Re x0) (CSNo_Re x0), 0, mul_SNo (CSNo_Im x0) (CSNo_Im x0) leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
Apply SNo_sqr_nonneg with CSNo_Im x0.
Apply real_SNo with CSNo_Im x0.
The subproof is completed by applying L3.
Apply Im_0 with λ x1 x2 . CSNo_Im x0 = x2.
Apply SNo_zero_or_sqr_pos with CSNo_Im x0, CSNo_Im x0 = 0 leaving 3 subgoals.
Apply real_SNo with CSNo_Im x0.
The subproof is completed by applying L3.
Assume H8: CSNo_Im x0 = 0.
The subproof is completed by applying H8.
Assume H8: SNoLt 0 (mul_SNo (CSNo_Im x0) (CSNo_Im x0)).
Apply FalseE with CSNo_Im x0 = 0.
Apply SNoLt_irref with 0.
Apply H7 with λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with 0, mul_SNo (CSNo_Im x0) (CSNo_Im x0), add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
Apply real_SNo with add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0)).
The subproof is completed by applying L6.
The subproof is completed by applying H8.
Apply add_SNo_0L with mul_SNo (CSNo_Im x0) (CSNo_Im x0), λ x1 x2 . SNoLe x1 (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0))) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply add_SNo_Le1 with 0, mul_SNo (CSNo_Im x0) (CSNo_Im x0), mul_SNo (CSNo_Re x0) (CSNo_Re x0) leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
The subproof is completed by applying L4.
Apply SNo_sqr_nonneg with CSNo_Re x0.
Apply real_SNo with CSNo_Re x0.
The subproof is completed by applying L2.
Let x1 of type ι be given.
Assume H7: (λ x2 . and (x2 ∈ real) (mul_SNo (add_SNo (mul_SNo (CSNo_Re ...) ...) ...) ... = 1)) ....
...
■