Metamath Proof Explorer

Theorem creui

Description: The imaginary part of a complex number is unique. Proposition 10-1.3 of Gleason p. 130. (Contributed by NM, 9-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion creui ⊢A∈ℂ→∃!y∈ℝ∃x∈ℝA=x+i⁢y

Proof

Step Hyp Ref Expression
1 cnre ⊢A∈ℂ→∃z∈ℝ∃w∈ℝA=z+i⁢w
2 simpr ⊢z∈ℝ∧w∈ℝ→w∈ℝ
3 eqcom ⊢z+i⁢w=x+i⁢y↔x+i⁢y=z+i⁢w
4 cru ⊢x∈ℝ∧y∈ℝ∧z∈ℝ∧w∈ℝ→x+i⁢y=z+i⁢w↔x=z∧y=w
5 4 ancoms ⊢z∈ℝ∧w∈ℝ∧x∈ℝ∧y∈ℝ→x+i⁢y=z+i⁢w↔x=z∧y=w
6 3 5 bitrid ⊢z∈ℝ∧w∈ℝ∧x∈ℝ∧y∈ℝ→z+i⁢w=x+i⁢y↔x=z∧y=w
7 6 anass1rs ⊢z∈ℝ∧w∈ℝ∧y∈ℝ∧x∈ℝ→z+i⁢w=x+i⁢y↔x=z∧y=w
8 7 rexbidva ⊢z∈ℝ∧w∈ℝ∧y∈ℝ→∃x∈ℝz+i⁢w=x+i⁢y↔∃x∈ℝx=z∧y=w
9 biidd ⊢x=z→y=w↔y=w
10 9 ceqsrexv ⊢z∈ℝ→∃x∈ℝx=z∧y=w↔y=w
11 10 ad2antrr ⊢z∈ℝ∧w∈ℝ∧y∈ℝ→∃x∈ℝx=z∧y=w↔y=w
12 8 11 bitrd ⊢z∈ℝ∧w∈ℝ∧y∈ℝ→∃x∈ℝz+i⁢w=x+i⁢y↔y=w
13 12 ralrimiva ⊢z∈ℝ∧w∈ℝ→∀y∈ℝ∃x∈ℝz+i⁢w=x+i⁢y↔y=w
14 reu6i ⊢w∈ℝ∧∀y∈ℝ∃x∈ℝz+i⁢w=x+i⁢y↔y=w→∃!y∈ℝ∃x∈ℝz+i⁢w=x+i⁢y
15 2 13 14 syl2anc ⊢z∈ℝ∧w∈ℝ→∃!y∈ℝ∃x∈ℝz+i⁢w=x+i⁢y
16 eqeq1 ⊢A=z+i⁢w→A=x+i⁢y↔z+i⁢w=x+i⁢y
17 16 rexbidv ⊢A=z+i⁢w→∃x∈ℝA=x+i⁢y↔∃x∈ℝz+i⁢w=x+i⁢y
18 17 reubidv ⊢A=z+i⁢w→∃!y∈ℝ∃x∈ℝA=x+i⁢y↔∃!y∈ℝ∃x∈ℝz+i⁢w=x+i⁢y
19 15 18 syl5ibrcom ⊢z∈ℝ∧w∈ℝ→A=z+i⁢w→∃!y∈ℝ∃x∈ℝA=x+i⁢y
20 19 rexlimivv ⊢∃z∈ℝ∃w∈ℝA=z+i⁢w→∃!y∈ℝ∃x∈ℝA=x+i⁢y
21 1 20 syl ⊢A∈ℂ→∃!y∈ℝ∃x∈ℝA=x+i⁢y