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