Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Apply complex_E with x0, CSNo_Im x0 ∈ real 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 . CSNo_Im x4 ∈ real.
Apply complex_Im_eq with x1, x2, λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
■