Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: CSNo x0.
Assume H1: CSNo x1.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Apply CSNo_ReIm_split with mul_CSNo x0 x1, mul_CSNo x1 x0 leaving 4 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
set y2 to be CSNo_Re (mul_CSNo x0 x1)
set y3 to be CSNo_Re (mul_CSNo y2 x1)
Claim L8: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
Assume H8: x4 (CSNo_Re (mul_CSNo y3 y2)).
Apply mul_CSNo_CRe with y2, y3, λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
set y5 to be add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re y3)) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im y2)))
set y6 to be add_SNo (mul_SNo (CSNo_Re x4) (CSNo_Re y3)) (minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)))
Claim L9: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H9: x7 (add_SNo (mul_SNo (CSNo_Re y5) (CSNo_Re x4)) (minus_SNo (mul_SNo (CSNo_Im x4) (CSNo_Im y5)))).
set y8 to be λ x8 . x7
Apply mul_SNo_com with CSNo_Re x4, CSNo_Re y5, λ x9 x10 . y8 (add_SNo x9 (minus_SNo (mul_SNo (CSNo_Im y5) (CSNo_Im x4)))) (add_SNo x10 (minus_SNo (mul_SNo (CSNo_Im y5) (CSNo_Im x4)))) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
set y9 to be λ x9 . y8
set y10 to be minus_SNo (mul_SNo (CSNo_Im y6) (CSNo_Im y5))
set y11 to be minus_SNo (mul_SNo (CSNo_Im y6) (CSNo_Im x7))
Claim L10: ∀ x12 : ι → ο . x12 y11 ⟶ x12 y10
Let x12 of type ι → ο be given.
Assume H10: x12 (minus_SNo (mul_SNo (CSNo_Im x7) (CSNo_Im y8))).
set y13 to be λ x13 . x12
Apply mul_SNo_com with CSNo_Im y8, CSNo_Im x7, λ x14 x15 . y13 (minus_SNo x14) (minus_SNo x15) leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L6.
The subproof is completed by applying H10.
set y12 to be λ x12 x13 . y11 (add_SNo (mul_SNo (CSNo_Re y8) (CSNo_Re x7)) x12) (add_SNo (mul_SNo (CSNo_Re y8) (CSNo_Re x7)) x13)
Apply L10 with λ x13 . y12 x13 y11 ⟶ y12 y11 x13 leaving 2 subgoals.
Assume H11: y12 y11 y11.
The subproof is completed by applying H11.
The subproof is completed by applying L10.
set y7 to be λ x7 . y6
Apply L9 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.
Assume H10: y7 y6 y6.
The subproof is completed by applying H10.
set y8 to be λ x8 . y7
Apply mul_CSNo_CRe with y6, y5, λ x9 x10 . y8 x10 x9 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
The subproof is completed by applying L9.
Let x4 of type ι → ι → ο be given.
Apply L8 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H9: x4 y3 y3.
The subproof is completed by applying H9.
set y2 to be ...
set y3 to be ...
Claim L8: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
Assume H8: x4 (CSNo_Im (mul_CSNo y3 y2)).
Apply mul_CSNo_CIm with y2, y3, λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply add_SNo_com with mul_SNo (CSNo_Im y3) (CSNo_Re y2), mul_SNo ... ..., ... leaving 3 subgoals.
...
...
...
Let x4 of type ι → ι → ο be given.
Apply L8 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H9: x4 y3 y3.
The subproof is completed by applying H9.
■