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

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		mulre	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℝ ↔ ( 𝐴 · 𝐵 ) ∈ ℝ ) )
8	6 1 3 7	syl3anc	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( 𝐴 · 𝐵 ) ∈ ℝ ) )
9	8	bicomd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
10	9	notbid	⊢ ( 𝜑 → ( ¬ ( 𝐴 · 𝐵 ) ∈ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
11	5 10	bitrid	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
12	4 11	mpbird	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∉ ℝ )