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 ⊢A∈ℂ∧B∈ℝ∧B≠0→A∈ℝ↔B⁢A∈ℝ

Proof

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