Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: CSNo x0.

Assume H1: CSNo x1.

Apply CSNo_ReIm_split with mul_CSNo x0 x1, mul_CSNo x1 x0 leaving 4 subgoals.

Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with x1, x0 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

set y2 to be CSNo_Re (mul_CSNo x1 x0)

Claim L2: ∀ x3 : ι → ο . x3 y2 ⟶ x3 (CSNo_Re (mul_CSNo x0 x1))

Let x3 of type ι → ο be given.

Assume H2: x3 (CSNo_Re (mul_CSNo y2 x1)).

Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with x1, y2, λ x4 . x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

set y4 to be add_SNo (mul_SNo (CSNo_Re y2) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x1)))

Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (add_SNo (mul_SNo (CSNo_Re x1) (CSNo_Re y2)) (minus_SNo (mul_SNo (CSNo_Im x1) (CSNo_Im y2))))

Let x5 of type ι → ο be given.

Assume H3: x5 (add_SNo (mul_SNo (CSNo_Re x3) (CSNo_Re y2)) (minus_SNo (mul_SNo (CSNo_Im x3) (CSNo_Im y2)))).

Apply mul_SNo_com with CSNo_Re y2, CSNo_Re x3, λ x6 x7 . (λ x8 . x5) (add_SNo x6 (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))) (add_SNo x7 (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))) leaving 3 subgoals.

Apply CSNo_ReR with y2.

The subproof is completed by applying H0.

Apply CSNo_ReR with x3.

The subproof is completed by applying H1.

set y6 to be minus_SNo (mul_SNo (CSNo_Im x3) (CSNo_Im y2))

Claim L4: ∀ x7 : ι → ο . x7 y6 ⟶ x7 (minus_SNo (mul_SNo (CSNo_Im y2) (CSNo_Im x3)))

Let x7 of type ι → ο be given.

Apply mul_SNo_com with CSNo_Im x3, CSNo_Im y4, λ x8 x9 . (λ x10 . x7) (minus_SNo x8) (minus_SNo x9) leaving 2 subgoals.

Apply CSNo_ImR with x3.

The subproof is completed by applying H0.

Apply CSNo_ImR with y4.

The subproof is completed by applying H1.

set y7 to be λ x7 x8 . (λ x9 . y6) (add_SNo (mul_SNo (CSNo_Re y4) (CSNo_Re x3)) x7) (add_SNo (mul_SNo (CSNo_Re y4) (CSNo_Re x3)) x8)

Apply L4 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.

Assume H5: y7 y6 y6.

The subproof is completed by applying H5.

The subproof is completed by applying L4.

set y5 to be λ x5 . y4

Apply L3 with λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.

Assume H4: y5 y4 y4.

The subproof is completed by applying H4.

Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with y4, x3, λ x6 x7 . (λ x8 . y5) x7 x6 leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H1.

The subproof is completed by applying L3.

Let x3 of type ι → ι → ο be given.

Apply L2 with λ x4 . x3 x4 y2 ⟶ x3 y2 x4.

Assume H3: x3 y2 y2.

The subproof is completed by applying H3.

set y2 to be ...

Claim L2: ∀ x3 : ι → ο . x3 y2 ⟶ x3 (CSNo_Im (mul_CSNo x0 x1))

Let x3 of type ι → ο be given.

Assume H2: x3 (CSNo_Im (mul_CSNo y2 x1)).

Apply unknownprop_f8168dc7675423b30fd1f30a7c39b8d4f1ba18bd99e8df15949f136f95eea4c7 with x1, y2, λ x4 . x3 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_Re x1) (CSNo_Im y2), mul_SNo (CSNo_Im x1) (CSNo_Re y2), λ x4 . x3 leaving 3 subgoals.

Apply SNo_mul_SNo with CSNo_Re x1, CSNo_Im ... leaving 2 subgoals.

...

Let x3 of type ι → ι → ο be given.

Apply L2 with λ x4 . x3 x4 y2 ⟶ x3 y2 x4.

Assume H3: x3 y2 y2.

The subproof is completed by applying H3.

■

Proofgold Proof