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	$$⊢\phi \to A\in ℝ$$
	recnaddnred.b	$$⊢\phi \to B\in \left(ℂ\setminus ℝ\right)$$
Assertion	readdcnnred	$$⊢\phi \to \left(A+B\right)\notin ℝ$$

Proof

Step	Hyp	Ref	Expression
1		recnaddnred.a	$$⊢\phi \to A\in ℝ$$
2		recnaddnred.b	$$⊢\phi \to B\in \left(ℂ\setminus ℝ\right)$$
3	2	eldifbd	$$⊢\phi \to \neg B\in ℝ$$
4		df-nel	$$⊢\left(A+B\right)\notin ℝ\leftrightarrow \neg A+B\in ℝ$$
5	1	recnd	$$⊢\phi \to A\in ℂ$$
6	2	eldifad	$$⊢\phi \to B\in ℂ$$
7	5 6	addcld	$$⊢\phi \to A+B\in ℂ$$
8		reim0b	$$⊢A+B\in ℂ\to \left(A+B\in ℝ\leftrightarrow \Im \left(A+B\right)=0\right)$$
9	7 8	syl	$$⊢\phi \to \left(A+B\in ℝ\leftrightarrow \Im \left(A+B\right)=0\right)$$
10	1	reim0d	$$⊢\phi \to \Im \left(A\right)=0$$
11	10	oveq1d	$$⊢\phi \to \Im \left(A\right)+\Im \left(B\right)=0+\Im \left(B\right)$$
12	6	imcld	$$⊢\phi \to \Im \left(B\right)\in ℝ$$
13	12	recnd	$$⊢\phi \to \Im \left(B\right)\in ℂ$$
14	13	addlidd	$$⊢\phi \to 0+\Im \left(B\right)=\Im \left(B\right)$$
15	11 14	eqtrd	$$⊢\phi \to \Im \left(A\right)+\Im \left(B\right)=\Im \left(B\right)$$
16	15	eqeq1d	$$⊢\phi \to \left(\Im \left(A\right)+\Im \left(B\right)=0\leftrightarrow \Im \left(B\right)=0\right)$$
17	5 6	imaddd	$$⊢\phi \to \Im \left(A+B\right)=\Im \left(A\right)+\Im \left(B\right)$$
18	17	eqeq1d	$$⊢\phi \to \left(\Im \left(A+B\right)=0\leftrightarrow \Im \left(A\right)+\Im \left(B\right)=0\right)$$
19		reim0b	$$⊢B\in ℂ\to \left(B\in ℝ\leftrightarrow \Im \left(B\right)=0\right)$$
20	6 19	syl	$$⊢\phi \to \left(B\in ℝ\leftrightarrow \Im \left(B\right)=0\right)$$
21	16 18 20	3bitr4d	$$⊢\phi \to \left(\Im \left(A+B\right)=0\leftrightarrow B\in ℝ\right)$$
22	9 21	bitrd	$$⊢\phi \to \left(A+B\in ℝ\leftrightarrow B\in ℝ\right)$$
23	22	notbid	$$⊢\phi \to \left(\neg A+B\in ℝ\leftrightarrow \neg B\in ℝ\right)$$
24	4 23	bitrid	$$⊢\phi \to \left(\left(A+B\right)\notin ℝ\leftrightarrow \neg B\in ℝ\right)$$
25	3 24	mpbird	$$⊢\phi \to \left(A+B\right)\notin ℝ$$