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	addlidd	⊢ ( 𝜑 → ( 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	bitrid	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ∉ ℝ ↔ ¬ 𝐵 ∈ ℝ ) )
25	3 24	mpbird	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∉ ℝ )