Metamath Proof Explorer


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 syl5bb ( 𝜑 → ( ( 𝐵 / 𝐴 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
22 4 21 mpbird ( 𝜑 → ( 𝐵 / 𝐴 ) ∉ ℝ )