Apply explicit_Complex_I with complex, CSNo_Re, CSNo_Im, 0, 1, Complex_i, add_CSNo, mul_CSNo leaving 9 subgoals.

The subproof is completed by applying unknownprop_3160270a6b7a6c6cbcf3fa0f7866a594ab49f62759e7107cbcc2c897c14f9a79.

Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ο . explicit_Reals {x2 ∈ complex|CSNo_Re x2 = x2} 0 1 add_CSNo mul_CSNo x1 ⟶ x0.

Apply H0 with SNoLe.

Apply complex_real_set_eq with λ x1 x2 . explicit_Reals x1 0 1 add_CSNo mul_CSNo SNoLe.

Apply explicit_Reals_transfer with real, 0, 1, add_SNo, mul_SNo, SNoLe, real, 0, 1, add_CSNo, mul_CSNo, SNoLe, λ x1 . x1 leaving 7 subgoals.

The subproof is completed by applying explicit_Reals_real.

The subproof is completed by applying bij_id with real.

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

Assume H1: x1 0 0.

The subproof is completed by applying H1.

set y1 to be 1

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

Assume H1: x2 y1 y1.

The subproof is completed by applying H1.

Let x1 of type ι be given.

Assume H1: x1 ∈ real.

Let x2 of type ι be given.

Assume H2: x2 ∈ real.

Apply add_SNo_add_CSNo with x1, x2 leaving 2 subgoals.

Apply real_SNo with x1.

The subproof is completed by applying H1.

Apply real_SNo with x2.

The subproof is completed by applying H2.

Let x1 of type ι be given.

Assume H1: x1 ∈ real.

Let x2 of type ι be given.

Assume H2: x2 ∈ real.

Apply unknownprop_e8fe572c395c46aa7a6d67f7a8cd850bf647261d6b3677aecbf3b7ddfa5a7193 with x1, x2 leaving 2 subgoals.

Apply real_SNo with x1.

The subproof is completed by applying H1.

Apply real_SNo with x2.

The subproof is completed by applying H2.

Let x1 of type ι be given.

Assume H1: x1 ∈ real.

Let x2 of type ι be given.

Assume H2: x2 ∈ real.

The subproof is completed by applying iff_refl with SNoLe x1 x2.

Apply complex_real_set_eq with λ x0 x1 . ∀ x2 . x2 ∈ complex ⟶ CSNo_Im x2 ∈ x0.

The subproof is completed by applying complex_Im_real.

The subproof is completed by applying complex_i.

Let x0 of type ι be given.

Assume H0: x0 ∈ complex.

Apply real_complex with CSNo_Re x0.

Apply complex_Re_real with x0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: x0 ∈ complex.

Apply real_complex with CSNo_Im x0.

Apply complex_Im_real with x0.

The subproof is completed by applying H0.

The subproof is completed by applying complex_eta.

The subproof is completed by applying complex_ReIm_split.

Apply unknownprop_5796014feba5197b3bf8ba040a6b1b81462d5deb0d9ee802d5b425665678e22a with λ x0 x1 . add_CSNo x1 1 = 0.

Apply add_CSNo_minus_CSNo_linv with 1.

The subproof is completed by applying unknownprop_33594f786441fb94cfa9c7be2034d88216fac0dbcbe9e223f18185e2cf6cb053.

■

Proofgold Proof