Theorem cndivrenred

Description: The quotient of an imaginary number and a real 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	cndivrenred	$$⊢\phi \to \left(\frac{B}{A}\right)\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	$$⊢\left(\frac{B}{A}\right)\notin ℝ\leftrightarrow \neg \frac{B}{A}\in ℝ$$
6	2	eldifad	$$⊢\phi \to B\in ℂ$$
7	1	recnd	$$⊢\phi \to A\in ℂ$$
8	6 7 3	divcld	$$⊢\phi \to \frac{B}{A}\in ℂ$$
9		reim0b	$$⊢\frac{B}{A}\in ℂ\to \left(\frac{B}{A}\in ℝ\leftrightarrow \Im \left(\frac{B}{A}\right)=0\right)$$
10	8 9	syl	$$⊢\phi \to \left(\frac{B}{A}\in ℝ\leftrightarrow \Im \left(\frac{B}{A}\right)=0\right)$$
11	6	imcld	$$⊢\phi \to \Im \left(B\right)\in ℝ$$
12	11	recnd	$$⊢\phi \to \Im \left(B\right)\in ℂ$$
13	12 7 3	diveq0ad	$$⊢\phi \to \left(\frac{\Im \left(B\right)}{A}=0\leftrightarrow \Im \left(B\right)=0\right)$$
14	1 6 3	imdivd	$$⊢\phi \to \Im \left(\frac{B}{A}\right)=\frac{\Im \left(B\right)}{A}$$
15	14	eqeq1d	$$⊢\phi \to \left(\Im \left(\frac{B}{A}\right)=0\leftrightarrow \frac{\Im \left(B\right)}{A}=0\right)$$
16		reim0b	$$⊢B\in ℂ\to \left(B\in ℝ\leftrightarrow \Im \left(B\right)=0\right)$$
17	6 16	syl	$$⊢\phi \to \left(B\in ℝ\leftrightarrow \Im \left(B\right)=0\right)$$
18	13 15 17	3bitr4d	$$⊢\phi \to \left(\Im \left(\frac{B}{A}\right)=0\leftrightarrow B\in ℝ\right)$$
19	10 18	bitrd	$$⊢\phi \to \left(\frac{B}{A}\in ℝ\leftrightarrow B\in ℝ\right)$$
20	19	notbid	$$⊢\phi \to \left(\neg \frac{B}{A}\in ℝ\leftrightarrow \neg B\in ℝ\right)$$
21	5 20	syl5bb	$$⊢\phi \to \left(\left(\frac{B}{A}\right)\notin ℝ\leftrightarrow \neg B\in ℝ\right)$$
22	4 21	mpbird	$$⊢\phi \to \left(\frac{B}{A}\right)\notin ℝ$$