Metamath Proof Explorer


Theorem readdcnnred

Description: The sum 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 ( 𝜑𝐵 ∈ ( ℂ ∖ ℝ ) )
Assertion readdcnnred ( 𝜑 → ( 𝐴 + 𝐵 ) ∉ ℝ )

Proof

Step Hyp Ref Expression
1 recnaddnred.a ( 𝜑𝐴 ∈ ℝ )
2 recnaddnred.b ( 𝜑𝐵 ∈ ( ℂ ∖ ℝ ) )
3 2 eldifbd ( 𝜑 → ¬ 𝐵 ∈ ℝ )
4 df-nel ( ( 𝐴 + 𝐵 ) ∉ ℝ ↔ ¬ ( 𝐴 + 𝐵 ) ∈ ℝ )
5 1 recnd ( 𝜑𝐴 ∈ ℂ )
6 2 eldifad ( 𝜑𝐵 ∈ ℂ )
7 5 6 addcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
8 reim0b ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( ( 𝐴 + 𝐵 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = 0 ) )
9 7 8 syl ( 𝜑 → ( ( 𝐴 + 𝐵 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = 0 ) )
10 1 reim0d ( 𝜑 → ( ℑ ‘ 𝐴 ) = 0 )
11 10 oveq1d ( 𝜑 → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) = ( 0 + ( ℑ ‘ 𝐵 ) ) )
12 6 imcld ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℝ )
13 12 recnd ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℂ )
14 13 addid2d ( 𝜑 → ( 0 + ( ℑ ‘ 𝐵 ) ) = ( ℑ ‘ 𝐵 ) )
15 11 14 eqtrd ( 𝜑 → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) = ( ℑ ‘ 𝐵 ) )
16 15 eqeq1d ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) = 0 ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
17 5 6 imaddd ( 𝜑 → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) )
18 17 eqeq1d ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = 0 ↔ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) = 0 ) )
19 reim0b ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
20 6 19 syl ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
21 16 18 20 3bitr4d ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = 0 ↔ 𝐵 ∈ ℝ ) )
22 9 21 bitrd ( 𝜑 → ( ( 𝐴 + 𝐵 ) ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
23 22 notbid ( 𝜑 → ( ¬ ( 𝐴 + 𝐵 ) ∈ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
24 4 23 syl5bb ( 𝜑 → ( ( 𝐴 + 𝐵 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
25 3 24 mpbird ( 𝜑 → ( 𝐴 + 𝐵 ) ∉ ℝ )