Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CSNo x0.
Assume H1: add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2) = 0.
Claim L2: SNo (CSNo_Re x0)
Apply CSNo_ReR with x0.
The subproof is completed by applying H0.
Claim L3: SNo (CSNo_Im x0)
Apply CSNo_ImR with x0.
The subproof is completed by applying H0.
Claim L4: SNo (exp_SNo_nat (CSNo_Re x0) 2)
Apply SNo_exp_SNo_nat with CSNo_Re x0, 2 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying nat_2.
Claim L5: SNo (exp_SNo_nat (CSNo_Im x0) 2)
Apply SNo_exp_SNo_nat with CSNo_Im x0, 2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying nat_2.
Claim L6: SNo (add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2))
Apply SNo_add_SNo with exp_SNo_nat (CSNo_Re x0) 2, exp_SNo_nat (CSNo_Im x0) 2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply CSNo_ReIm_split with x0, 0 leaving 4 subgoals.
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.
The subproof is completed by applying L2.
Assume H7: CSNo_Re x0 = 0.
The subproof is completed by applying H7.
Assume H7: SNoLt 0 (exp_SNo_nat (CSNo_Re x0) 2).
Apply FalseE with CSNo_Re x0 = 0.
Apply SNoLt_irref with 0.
Apply H1 with λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with 0, exp_SNo_nat (CSNo_Re x0) 2, add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Apply add_SNo_0R with exp_SNo_nat (CSNo_Re x0) 2, λ x1 x2 . SNoLe x1 (add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2)) leaving 2 subgoals.
The subproof is completed by applying L4.
Apply add_SNo_Le2 with exp_SNo_nat (CSNo_Re x0) 2, 0, exp_SNo_nat (CSNo_Im x0) 2 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.
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.
The subproof is completed by applying L3.
Assume H7: CSNo_Im x0 = 0.
The subproof is completed by applying H7.
Assume H7: SNoLt 0 (exp_SNo_nat (CSNo_Im x0) 2).
Apply FalseE with CSNo_Im x0 = 0.
Apply SNoLt_irref with 0.
Apply H1 with λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with 0, exp_SNo_nat (CSNo_Im x0) 2, add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Apply add_SNo_0L with exp_SNo_nat (CSNo_Im x0) 2, λ x1 x2 . SNoLe x1 (add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2)) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply add_SNo_Le1 with 0, exp_SNo_nat (CSNo_Im x0) 2, exp_SNo_nat (CSNo_Re x0) 2 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.
The subproof is completed by applying L2.
■