Theorem recnmulnred

Description: The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023)

	Ref	Expression
Hypotheses	recnaddnred.a	$$⊢\phi \to A\in ℝ$$
	recnaddnred.b	$$⊢\phi \to B\in \left(ℂ\setminus ℝ\right)$$
	cndivrenred.n	$$⊢\phi \to A\ne 0$$
Assertion	recnmulnred	$$⊢\phi \to AB\notin ℝ$$

Proof

Step	Hyp	Ref	Expression
1		recnaddnred.a	$$⊢\phi \to A\in ℝ$$
2		recnaddnred.b	$$⊢\phi \to B\in \left(ℂ\setminus ℝ\right)$$
3		cndivrenred.n	$$⊢\phi \to A\ne 0$$
4	2	eldifbd	$$⊢\phi \to \neg B\in ℝ$$
5		df-nel	$$⊢AB\notin ℝ\leftrightarrow \neg AB\in ℝ$$
6	2	eldifad	$$⊢\phi \to B\in ℂ$$
7		mulre	$$⊢\left(B\in ℂ\wedge A\in ℝ\wedge A\ne 0\right)\to \left(B\in ℝ\leftrightarrow AB\in ℝ\right)$$
8	6 1 3 7	syl3anc	$$⊢\phi \to \left(B\in ℝ\leftrightarrow AB\in ℝ\right)$$
9	8	bicomd	$$⊢\phi \to \left(AB\in ℝ\leftrightarrow B\in ℝ\right)$$
10	9	notbid	$$⊢\phi \to \left(\neg AB\in ℝ\leftrightarrow \neg B\in ℝ\right)$$
11	5 10	syl5bb	$$⊢\phi \to \left(AB\notin ℝ\leftrightarrow \neg B\in ℝ\right)$$
12	4 11	mpbird	$$⊢\phi \to AB\notin ℝ$$