This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 cnre ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑧 ∈ ℝ ∃ 𝑤 ∈ ℝ 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) )
2 cru ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
3 2 ancoms ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
4 eqcom ⊢ ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) )
5 ancom ⊢ ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
6 3 4 5 3bitr4g ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ) )
7 6 anassrs ⊢ ( ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ) )
8 7 rexbidva ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ) )
9 biidd ⊢ ( 𝑦 = 𝑤 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑧 ) )
10 9 ceqsrexv ⊢ ( 𝑤 ∈ ℝ → ( ∃ 𝑦 ∈ ℝ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ↔ 𝑥 = 𝑧 ) )
11 10 ad2antlr ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) ↔ 𝑥 = 𝑧 ) )
12 8 11 bitrd ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑥 = 𝑧 ) )
13 12 ralrimiva ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ( ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑥 = 𝑧 ) )
14 reu6i ⊢ ( ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ( ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑥 = 𝑧 ) ) → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
15 13 14 syldan ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
16 eqeq1 ⊢ ( 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
17 16 rexbidv ⊢ ( 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) → ( ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
18 17 reubidv ⊢ ( 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) → ( ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
19 15 18 syl5ibrcom ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) )
20 19 rexlimivv ⊢ ( ∃ 𝑧 ∈ ℝ ∃ 𝑤 ∈ ℝ 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
21 1 20 syl ⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )