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

Metamath Proof Explorer

Theorem remim

Description: Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of Gleason p. 132. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion remim ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 cjval ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
2 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
3 2 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
4 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
5 4 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
6 ax-icn ⊢ i ∈ ℂ
7 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
8 7 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
9 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
10 6 8 9 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
11 5 10 5 ppncand ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) )
12 3 11 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) )
13 4 4 readdcld ⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
14 12 13 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ )
15 5 10 10 pnncand ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
16 2 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
17 6 a1i ⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
18 17 8 8 adddid ⊢ ( 𝐴 ∈ ℂ → ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
19 15 16 18 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) )
20 19 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
21 7 7 readdcld ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
22 21 recnd ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
23 mulass ⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
24 6 6 22 23 mp3an12i ⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
25 20 24 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) )
26 ixi ⊢ ( i · i ) = - 1
27 neg1rr ⊢ - 1 ∈ ℝ
28 26 27 eqeltri ⊢ ( i · i ) ∈ ℝ
29 remulcl ⊢ ( ( ( i · i ) ∈ ℝ ∧ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℝ ) → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ )
30 28 21 29 sylancr ⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ )
31 25 30 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ )
32 5 10 subcld ⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
33 cju ⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
34 oveq2 ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
35 34 eleq1d ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( 𝐴 + 𝑥 ) ∈ ℝ ↔ ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ) )
36 oveq2 ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
37 36 oveq2d ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( i · ( 𝐴 − 𝑥 ) ) = ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
38 37 eleq1d ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ↔ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) )
39 35 38 anbi12d ⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ↔ ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ) )
40 39 riota2 ⊢ ( ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) → ( ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
41 32 33 40 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
42 14 31 41 mpbi2and ⊢ ( 𝐴 ∈ ℂ → ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
43 1 42 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )