Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: CSNo (mul_CSNo Complex_i Complex_i)
Apply CSNo_mul_CSNo with Complex_i, Complex_i leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Claim L1: CSNo (minus_CSNo 1)
Apply CSNo_minus_CSNo with 1.
The subproof is completed by applying CSNo_1.
Apply CSNo_ReIm_split with mul_CSNo Complex_i Complex_i, minus_CSNo 1 leaving 4 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply mul_CSNo_CRe with Complex_i, Complex_i, λ x0 x1 . x1 = CSNo_Re (minus_CSNo 1) leaving 3 subgoals.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_CSNo_CRe with 1, λ x0 x1 . add_SNo (mul_SNo (CSNo_Re Complex_i) (CSNo_Re Complex_i)) (minus_SNo (mul_SNo (CSNo_Im Complex_i) (CSNo_Im Complex_i))) = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_1.
Apply Re_i with λ x0 x1 . add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo (CSNo_Im Complex_i) (CSNo_Im Complex_i))) = minus_SNo (CSNo_Re 1).
Apply Im_i with λ x0 x1 . add_SNo (mul_SNo 0 0) (minus_SNo (mul_SNo x1 x1)) = minus_SNo (CSNo_Re 1).
Apply Re_1 with λ x0 x1 . add_SNo (mul_SNo 0 0) (minus_SNo (mul_SNo 1 1)) = minus_SNo x1.
Apply mul_SNo_zeroL with 0, λ x0 x1 . add_SNo x1 (minus_SNo (mul_SNo 1 1)) = minus_SNo 1 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_SNo_oneL with 1, λ x0 x1 . add_SNo 0 (minus_SNo x1) = minus_SNo 1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply add_SNo_0L with minus_SNo 1.
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
Apply mul_CSNo_CIm with Complex_i, Complex_i, λ x0 x1 . x1 = CSNo_Im (minus_CSNo 1) leaving 3 subgoals.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_CSNo_CIm with 1, λ x0 x1 . add_SNo (mul_SNo (CSNo_Im Complex_i) (CSNo_Re Complex_i)) (mul_SNo (CSNo_Im Complex_i) (CSNo_Re Complex_i)) = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_1.
Apply Re_i with λ x0 x1 . add_SNo (mul_SNo (CSNo_Im Complex_i) x1) (mul_SNo (CSNo_Im Complex_i) x1) = minus_SNo (CSNo_Im 1).
Apply Im_i with λ x0 x1 . add_SNo (mul_SNo x1 0) (mul_SNo x1 0) = minus_SNo (CSNo_Im 1).
Apply Im_1 with λ x0 x1 . add_SNo (mul_SNo 1 0) (mul_SNo 1 0) = minus_SNo x1.
Apply minus_SNo_0 with λ x0 x1 . add_SNo (mul_SNo 1 0) (mul_SNo 1 0) = x1.
Apply mul_SNo_zeroR with 1, λ x0 x1 . add_SNo x1 x1 = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply add_SNo_0L with 0.
The subproof is completed by applying SNo_0.
■