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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	recnaddnred.b	⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ ℝ ) )
Assertion	resubcnnred	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∉ ℝ )

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	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
8		reim0b	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐴 − 𝐵 ) ) = 0 ) )
9	7 8	syl	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ∈ ℝ ↔ ( ℑ ‘ ( 𝐴 − 𝐵 ) ) = 0 ) )
10	1	reim0d	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) = 0 )
11	10	oveq1d	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝐵 ) ) = ( 0 − ( ℑ ‘ 𝐵 ) ) )
12		df-neg	⊢ - ( ℑ ‘ 𝐵 ) = ( 0 − ( ℑ ‘ 𝐵 ) )
13	11 12	eqtr4di	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝐵 ) ) = - ( ℑ ‘ 𝐵 ) )
14	13	eqeq1d	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝐵 ) ) = 0 ↔ - ( ℑ ‘ 𝐵 ) = 0 ) )
15	5 6	imsubd	⊢ ( 𝜑 → ( ℑ ‘ ( 𝐴 − 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝐵 ) ) )
16	15	eqeq1d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 − 𝐵 ) ) = 0 ↔ ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝐵 ) ) = 0 ) )
17		reim0b	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
18	6 17	syl	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ℑ ‘ 𝐵 ) = 0 ) )
19	6	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℝ )
20	19	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝐵 ) ∈ ℂ )
21	20	negeq0d	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐵 ) = 0 ↔ - ( ℑ ‘ 𝐵 ) = 0 ) )
22	18 21	bitrd	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ - ( ℑ ‘ 𝐵 ) = 0 ) )
23	14 16 22	3bitr4d	⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 − 𝐵 ) ) = 0 ↔ 𝐵 ∈ ℝ ) )
24	9 23	bitrd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
25	24	notbid	⊢ ( 𝜑 → ( ¬ ( 𝐴 − 𝐵 ) ∈ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
26	4 25	bitrid	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
27	3 26	mpbird	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∉ ℝ )