Search for blocks/addresses/...

Proofgold Proof

pf
Apply CSNo_ReIm_split with mul_CSNo Complex_i Complex_i, minus_CSNo 1 leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with Complex_i, Complex_i leaving 2 subgoals.
The subproof is completed by applying SNo_Complex_i.
The subproof is completed by applying SNo_Complex_i.
Apply CSNo_minus_CSNo with 1.
The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with Complex_i, Complex_i, λ x0 x1 . x1 = CSNo_Re (minus_CSNo 1) leaving 3 subgoals.
The subproof is completed by applying SNo_Complex_i.
The subproof is completed by applying SNo_Complex_i.
Apply unknownprop_b3da9c8705efa35c67169a2e2027e4447fcfab350671212d3a9a4c69902c0e94 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 unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
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 unknownprop_f8168dc7675423b30fd1f30a7c39b8d4f1ba18bd99e8df15949f136f95eea4c7 with Complex_i, Complex_i, λ x0 x1 . x1 = CSNo_Im (minus_CSNo 1) leaving 3 subgoals.
The subproof is completed by applying SNo_Complex_i.
The subproof is completed by applying SNo_Complex_i.
Apply unknownprop_efd7dfcd3e80202ffcc3e685b73692d3dd99f31e27f878a9cd3b14c55287909a with 1, λ x0 x1 . add_SNo (mul_SNo (CSNo_Re Complex_i) (CSNo_Im Complex_i)) (mul_SNo (CSNo_Im Complex_i) (CSNo_Re Complex_i)) = x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.
Apply Re_i with λ x0 x1 . add_SNo (mul_SNo x1 (CSNo_Im Complex_i)) (mul_SNo (CSNo_Im Complex_i) x1) = minus_SNo (CSNo_Im 1).
Apply Im_i with λ x0 x1 . add_SNo (mul_SNo 0 x1) (mul_SNo x1 0) = minus_SNo (CSNo_Im 1).
Apply Im_1 with λ x0 x1 . add_SNo (mul_SNo 0 1) (mul_SNo 1 0) = minus_SNo x1.
Apply minus_SNo_0 with λ x0 x1 . add_SNo (mul_SNo 0 1) (mul_SNo 1 0) = x1.
Apply mul_SNo_zeroL with 1, λ x0 x1 . add_SNo x1 (mul_SNo 1 0) = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply mul_SNo_zeroR with 1, λ x0 x1 . add_SNo 0 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.
■