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∉ℝ