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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	recnaddnred.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ ℝ ) )
	cndivrenred.n	⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion	cndivrenred	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∉ ℝ )

Proof

Step	Hyp	Ref	Expression
1		recnaddnred.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		recnaddnred.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ ℝ ) )
3		cndivrenred.n	⊢ ( 𝜑 → 𝐴 ≠ 0 )
4	2	eldifbd	⊢ ( 𝜑 → ¬ 𝐵 ∈ ℝ )
5		df-nel	⊢ ( ( 𝐵 / 𝐴 ) ∉ ℝ ↔ ¬ ( 𝐵 / 𝐴 ) ∈ ℝ )
6	2	eldifad	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8	6 7 3	divcld	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℂ )
9		reim0b	⊢ ( ( 𝐵 / 𝐴 ) ∈ ℂ → ( ( 𝐵 / 𝐴 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐵 / 𝐴 ) ) = 0 ) )
10	8 9	syl	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐵 / 𝐴 ) ) = 0 ) )
11	6	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℂ )
13	12 7 3	diveq0ad	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐵 ) / 𝐴 ) = 0 ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
14	1 6 3	imdivd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐵 / 𝐴 ) ) = ( ( ℑ ‘ 𝐵 ) / 𝐴 ) )
15	14	eqeq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐵 / 𝐴 ) ) = 0 ↔ ( ( ℑ ‘ 𝐵 ) / 𝐴 ) = 0 ) )
16		reim0b	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
17	6 16	syl	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
18	13 15 17	3bitr4d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐵 / 𝐴 ) ) = 0 ↔ 𝐵 ∈ ℝ ) )
19	10 18	bitrd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
20	19	notbid	⊢ ( 𝜑 → ( ¬ ( 𝐵 / 𝐴 ) ∈ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
21	5 20	bitrid	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
22	4 21	mpbird	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∉ ℝ )