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

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 ) → ( 𝐴 ∈ ℝ ↔ ( 𝐵 · 𝐴 ) ∈ ℝ ) )