Metamath Proof Explorer


Theorem mulre

Description: A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008)

Ref Expression
Assertion mulre ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 rereb ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )
2 1 3ad2ant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )
3 recl ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
4 3 recnd ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
5 4 3ad2ant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
6 simp1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐴 ∈ ℂ )
7 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
8 7 anim1i ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
9 8 3adant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
10 mulcan ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )
11 5 6 9 10 syl3anc ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( ℜ ‘ 𝐴 ) = 𝐴 ) )
12 7 adantr ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → 𝐵 ∈ ℂ )
13 4 adantl ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
14 ax-icn i ∈ ℂ
15 imcl ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
16 15 recnd ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
17 mulcl ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
18 14 16 17 sylancr ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
19 18 adantl ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
20 12 13 19 adddid ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( 𝐵 · ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
21 replim ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
22 21 adantl ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
23 22 oveq2d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · 𝐴 ) = ( 𝐵 · ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
24 mul12 ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) = ( 𝐵 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
25 14 7 16 24 mp3an3an ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) = ( 𝐵 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
26 25 oveq2d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( 𝐵 · ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
27 20 23 26 3eqtr4d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · 𝐴 ) = ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) ) )
28 27 fveq2d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ ( 𝐵 · 𝐴 ) ) = ( ℜ ‘ ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) ) ) )
29 remulcl ( ( 𝐵 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
30 3 29 sylan2 ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
31 remulcl ( ( 𝐵 ∈ ℝ ∧ ( ℑ ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
32 15 31 sylan2 ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
33 crre ( ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ∈ ℝ ) → ( ℜ ‘ ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( 𝐵 · ( ℜ ‘ 𝐴 ) ) )
34 30 32 33 syl2anc ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) + ( i · ( 𝐵 · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( 𝐵 · ( ℜ ‘ 𝐴 ) ) )
35 28 34 eqtr2d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 𝐵 · 𝐴 ) ) )
36 35 eqeq1d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( ℜ ‘ ( 𝐵 · 𝐴 ) ) = ( 𝐵 · 𝐴 ) ) )
37 mulcl ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · 𝐴 ) ∈ ℂ )
38 7 37 sylan ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 · 𝐴 ) ∈ ℂ )
39 rereb ( ( 𝐵 · 𝐴 ) ∈ ℂ → ( ( 𝐵 · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ ( 𝐵 · 𝐴 ) ) = ( 𝐵 · 𝐴 ) ) )
40 38 39 syl ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 · 𝐴 ) ∈ ℝ ↔ ( ℜ ‘ ( 𝐵 · 𝐴 ) ) = ( 𝐵 · 𝐴 ) ) )
41 36 40 bitr4d ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )
42 41 ancoms ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )
43 42 3adant3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ( 𝐵 · ( ℜ ‘ 𝐴 ) ) = ( 𝐵 · 𝐴 ) ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )
44 2 11 43 3bitr2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )