Metamath Proof Explorer

Theorem crim

Description: The real part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion crim ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
5 2 3 4 sylancr ⊢ ( 𝐵 ∈ ℝ → ( i · 𝐵 ) ∈ ℂ )
6 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
7 1 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
8 imval ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) / i ) ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) / i ) ) )
10 2 4 mpan ⊢ ( 𝐵 ∈ ℂ → ( i · 𝐵 ) ∈ ℂ )
11 ine0 ⊢ i ≠ 0
12 divdir ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ∧ ( i ∈ ℂ ∧ i ≠ 0 ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) / i ) = ( ( 𝐴 / i ) + ( ( i · 𝐵 ) / i ) ) )
13 12 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) ∧ ( i ∈ ℂ ∧ i ≠ 0 ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) / i ) = ( ( 𝐴 / i ) + ( ( i · 𝐵 ) / i ) ) )
14 2 11 13 mpanr12 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 + ( i · 𝐵 ) ) / i ) = ( ( 𝐴 / i ) + ( ( i · 𝐵 ) / i ) ) )
15 10 14 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + ( i · 𝐵 ) ) / i ) = ( ( 𝐴 / i ) + ( ( i · 𝐵 ) / i ) ) )
16 divrec2 ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( 𝐴 / i ) = ( ( 1 / i ) · 𝐴 ) )
17 2 11 16 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / i ) = ( ( 1 / i ) · 𝐴 ) )
18 irec ⊢ ( 1 / i ) = - i
19 18 oveq1i ⊢ ( ( 1 / i ) · 𝐴 ) = ( - i · 𝐴 )
20 19 a1i ⊢ ( 𝐴 ∈ ℂ → ( ( 1 / i ) · 𝐴 ) = ( - i · 𝐴 ) )
21 mulneg12 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
22 2 21 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
23 17 20 22 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / i ) = ( i · - 𝐴 ) )
24 divcan3 ⊢ ( ( 𝐵 ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · 𝐵 ) / i ) = 𝐵 )
25 2 11 24 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( ( i · 𝐵 ) / i ) = 𝐵 )
26 23 25 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 / i ) + ( ( i · 𝐵 ) / i ) ) = ( ( i · - 𝐴 ) + 𝐵 ) )
27 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
28 mulcl ⊢ ( ( i ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) ∈ ℂ )
29 2 27 28 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) ∈ ℂ )
30 addcom ⊢ ( ( ( i · - 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · - 𝐴 ) + 𝐵 ) = ( 𝐵 + ( i · - 𝐴 ) ) )
31 29 30 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · - 𝐴 ) + 𝐵 ) = ( 𝐵 + ( i · - 𝐴 ) ) )
32 15 26 31 3eqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 + ( i · - 𝐴 ) ) = ( ( 𝐴 + ( i · 𝐵 ) ) / i ) )
33 1 3 32 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 + ( i · - 𝐴 ) ) = ( ( 𝐴 + ( i · 𝐵 ) ) / i ) )
34 33 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐵 + ( i · - 𝐴 ) ) ) = ( ℜ ‘ ( ( 𝐴 + ( i · 𝐵 ) ) / i ) ) )
35 id ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
36 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
37 crre ⊢ ( ( 𝐵 ∈ ℝ ∧ - 𝐴 ∈ ℝ ) → ( ℜ ‘ ( 𝐵 + ( i · - 𝐴 ) ) ) = 𝐵 )
38 35 36 37 syl2anr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐵 + ( i · - 𝐴 ) ) ) = 𝐵 )
39 9 34 38 3eqtr2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )