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