Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ complex.

Apply complex_E with x0, x0 = add_CSNo (CSNo_Re x0) (mul_CSNo Complex_i (CSNo_Im x0)) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H1: x1 ∈ real.

Let x2 of type ι be given.

Assume H2: x2 ∈ real.

Assume H3: x0 = SNo_pair x1 x2.

Apply H3 with λ x3 x4 . x4 = add_CSNo (CSNo_Re x4) (mul_CSNo Complex_i (CSNo_Im x4)).

Apply complex_Re_eq with x1, x2, λ x3 x4 . SNo_pair x1 x2 = add_CSNo x4 (mul_CSNo Complex_i (CSNo_Im (SNo_pair x1 x2))) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply complex_Im_eq with x1, x2, λ x3 x4 . SNo_pair x1 x2 = add_CSNo x1 (mul_CSNo Complex_i x4) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply real_Re_eq with x1, λ x3 x4 . SNo_pair x1 x2 = SNo_pair (add_SNo x4 (CSNo_Re (mul_CSNo Complex_i x2))) (add_SNo (CSNo_Im x1) (CSNo_Im (mul_CSNo Complex_i x2))) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply real_Im_eq with x1, λ x3 x4 . SNo_pair x1 x2 = SNo_pair (add_SNo x1 (CSNo_Re (mul_CSNo Complex_i x2))) (add_SNo x4 (CSNo_Im (mul_CSNo Complex_i x2))) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply real_Re_i_eq with x2, λ x3 x4 . SNo_pair x1 x2 = SNo_pair (add_SNo x1 x4) (add_SNo 0 (CSNo_Im (mul_CSNo Complex_i x2))) leaving 2 subgoals.

The subproof is completed by applying H2.

Apply real_Im_i_eq with x2, λ x3 x4 . SNo_pair x1 x2 = SNo_pair (add_SNo x1 0) (add_SNo 0 x4) leaving 2 subgoals.

The subproof is completed by applying H2.

Apply add_SNo_0R with x1, λ x3 x4 . SNo_pair x1 x2 = SNo_pair x4 (add_SNo 0 x2) leaving 2 subgoals.

Apply real_SNo with x1.

The subproof is completed by applying H1.

Apply add_SNo_0L with x2, λ x3 x4 . SNo_pair x1 x2 = SNo_pair x1 x4 leaving 2 subgoals.

Apply real_SNo with x2.

The subproof is completed by applying H2.

set y3 to be SNo_pair x1 x2

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

Assume H4: x4 y3 y3.

The subproof is completed by applying H4.

■