Metamath Proof Explorer


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 syl5bb ( 𝜑 → ( ( 𝐴 · 𝐵 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
12 4 11 mpbird ( 𝜑 → ( 𝐴 · 𝐵 ) ∉ ℝ )