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 · 𝑦 ) ) )