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 \in ℂ \land B \in ℝ \land B \neq 0) \to (A \in ℝ \leftrightarrow B A \in ℝ)$

Proof

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

Metamath Proof Explorer

Theorem mulre

Proof