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

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

Proof

Step Hyp Ref Expression
1 cnre ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑧 ∈ ℝ ∃ 𝑤 ∈ ℝ 𝐴 = ( 𝑧 + ( i · 𝑤 ) ) )
2 simpr ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
3 eqcom ⊢ ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) )
4 cru ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
5 4 ancoms ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑧 + ( i · 𝑤 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
6 3 5 bitrid ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
7 6 anass1rs ⊢ ( ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
8 7 rexbidva ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
9 biidd ⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 ↔ 𝑦 = 𝑤 ) )
10 9 ceqsrexv ⊢ ( 𝑧 ∈ ℝ → ( ∃ 𝑥 ∈ ℝ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ 𝑦 = 𝑤 ) )
11 10 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ 𝑦 = 𝑤 ) )
12 8 11 bitrd ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑦 = 𝑤 ) )
13 12 ralrimiva ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ( ∃ 𝑥 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑦 = 𝑤 ) )
14 reu6i ⊢ ( ( 𝑤 ∈ ℝ ∧ ∀ 𝑦 ∈ ℝ ( ∃ 𝑥 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝑦 = 𝑤 ) ) → ∃! 𝑦 ∈ ℝ ∃ 𝑥 ∈ ℝ ( 𝑧 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
15 2 13 14 syl2anc ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ∃! 𝑦 ∈ ℝ ∃ 𝑥 ∈ ℝ ( 𝑧 + ( 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 · 𝑦 ) ) )