Metamath Proof Explorer

Theorem creur

Description: The real 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 creur ⊢ A ∈ ℂ → ∃! x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y

Proof

Step Hyp Ref Expression
1 cnre ⊢ A ∈ ℂ → ∃ z ∈ ℝ ∃ w ∈ ℝ A = z + i ⁢ w
2 cru ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ z ∈ ℝ ∧ w ∈ ℝ → x + i ⁢ y = z + i ⁢ w ↔ x = z ∧ y = w
3 2 ancoms ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ ℝ → x + i ⁢ y = z + i ⁢ w ↔ x = z ∧ y = w
4 eqcom ⊢ z + i ⁢ w = x + i ⁢ y ↔ x + i ⁢ y = z + i ⁢ w
5 ancom ⊢ y = w ∧ x = z ↔ x = z ∧ y = w
6 3 4 5 3bitr4g ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ ℝ → z + i ⁢ w = x + i ⁢ y ↔ y = w ∧ x = z
7 6 anassrs ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ ℝ → z + i ⁢ w = x + i ⁢ y ↔ y = w ∧ x = z
8 7 rexbidva ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ → ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y ↔ ∃ y ∈ ℝ y = w ∧ x = z
9 biidd ⊢ y = w → x = z ↔ x = z
10 9 ceqsrexv ⊢ w ∈ ℝ → ∃ y ∈ ℝ y = w ∧ x = z ↔ x = z
11 10 ad2antlr ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ → ∃ y ∈ ℝ y = w ∧ x = z ↔ x = z
12 8 11 bitrd ⊢ z ∈ ℝ ∧ w ∈ ℝ ∧ x ∈ ℝ → ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y ↔ x = z
13 12 ralrimiva ⊢ z ∈ ℝ ∧ w ∈ ℝ → ∀ x ∈ ℝ ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y ↔ x = z
14 reu6i ⊢ z ∈ ℝ ∧ ∀ x ∈ ℝ ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y ↔ x = z → ∃! x ∈ ℝ ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y
15 13 14 syldan ⊢ z ∈ ℝ ∧ w ∈ ℝ → ∃! x ∈ ℝ ∃ y ∈ ℝ 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 → ∃ y ∈ ℝ A = x + i ⁢ y ↔ ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y
18 17 reubidv ⊢ A = z + i ⁢ w → ∃! x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y ↔ ∃! x ∈ ℝ ∃ y ∈ ℝ z + i ⁢ w = x + i ⁢ y
19 15 18 syl5ibrcom ⊢ z ∈ ℝ ∧ w ∈ ℝ → A = z + i ⁢ w → ∃! x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y
20 19 rexlimivv ⊢ ∃ z ∈ ℝ ∃ w ∈ ℝ A = z + i ⁢ w → ∃! x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y
21 1 20 syl ⊢ A ∈ ℂ → ∃! x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y