Metamath Proof Explorer

Theorem resubcnnred

Description: The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023)

Ref Expression
Hypotheses recnaddnred.a ⊢ φ → A ∈ ℝ
recnaddnred.b ⊢ φ → B ∈ ℂ ∖ ℝ
Assertion resubcnnred ⊢ φ → A − B ∉ ℝ

Proof

Step Hyp Ref Expression
1 recnaddnred.a ⊢ φ → A ∈ ℝ
2 recnaddnred.b ⊢ φ → B ∈ ℂ ∖ ℝ
3 2 eldifbd ⊢ φ → ¬ B ∈ ℝ
4 df-nel ⊢ A − B ∉ ℝ ↔ ¬ A − B ∈ ℝ
5 1 recnd ⊢ φ → A ∈ ℂ
6 2 eldifad ⊢ φ → B ∈ ℂ
7 5 6 subcld ⊢ φ → A − B ∈ ℂ
8 reim0b ⊢ A − B ∈ ℂ → A − B ∈ ℝ ↔ ℑ ⁡ A − B = 0
9 7 8 syl ⊢ φ → A − B ∈ ℝ ↔ ℑ ⁡ A − B = 0
10 1 reim0d ⊢ φ → ℑ ⁡ A = 0
11 10 oveq1d ⊢ φ → ℑ ⁡ A − ℑ ⁡ B = 0 − ℑ ⁡ B
12 df-neg ⊢ − ℑ ⁡ B = 0 − ℑ ⁡ B
13 11 12 eqtr4di ⊢ φ → ℑ ⁡ A − ℑ ⁡ B = − ℑ ⁡ B
14 13 eqeq1d ⊢ φ → ℑ ⁡ A − ℑ ⁡ B = 0 ↔ − ℑ ⁡ B = 0
15 5 6 imsubd ⊢ φ → ℑ ⁡ A − B = ℑ ⁡ A − ℑ ⁡ B
16 15 eqeq1d ⊢ φ → ℑ ⁡ A − B = 0 ↔ ℑ ⁡ A − ℑ ⁡ B = 0
17 reim0b ⊢ B ∈ ℂ → B ∈ ℝ ↔ ℑ ⁡ B = 0
18 6 17 syl ⊢ φ → B ∈ ℝ ↔ ℑ ⁡ B = 0
19 6 imcld ⊢ φ → ℑ ⁡ B ∈ ℝ
20 19 recnd ⊢ φ → ℑ ⁡ B ∈ ℂ
21 20 negeq0d ⊢ φ → ℑ ⁡ B = 0 ↔ − ℑ ⁡ B = 0
22 18 21 bitrd ⊢ φ → B ∈ ℝ ↔ − ℑ ⁡ B = 0
23 14 16 22 3bitr4d ⊢ φ → ℑ ⁡ A − B = 0 ↔ B ∈ ℝ
24 9 23 bitrd ⊢ φ → A − B ∈ ℝ ↔ B ∈ ℝ
25 24 notbid ⊢ φ → ¬ A − B ∈ ℝ ↔ ¬ B ∈ ℝ
26 4 25 bitrid ⊢ φ → A − B ∉ ℝ ↔ ¬ B ∈ ℝ
27 3 26 mpbird ⊢ φ → A − B ∉ ℝ