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	|- ( ph -> A e. RR )
	recnaddnred.b	|- ( ph -> B e. ( CC \ RR ) )
Assertion	readdcnnred	|- ( ph -> ( A + B ) e/ RR )

Proof

Step	Hyp	Ref	Expression
1		recnaddnred.a	|- ( ph -> A e. RR )
2		recnaddnred.b	|- ( ph -> B e. ( CC \ RR ) )
3	2	eldifbd	|- ( ph -> -. B e. RR )
4		df-nel	|- ( ( A + B ) e/ RR <-> -. ( A + B ) e. RR )
5	1	recnd	|- ( ph -> A e. CC )
6	2	eldifad	|- ( ph -> B e. CC )
7	5 6	addcld	|- ( ph -> ( A + B ) e. CC )
8		reim0b	|- ( ( A + B ) e. CC -> ( ( A + B ) e. RR <-> ( Im ` ( A + B ) ) = 0 ) )
9	7 8	syl	|- ( ph -> ( ( A + B ) e. RR <-> ( Im ` ( A + B ) ) = 0 ) )
10	1	reim0d	|- ( ph -> ( Im ` A ) = 0 )
11	10	oveq1d	|- ( ph -> ( ( Im ` A ) + ( Im ` B ) ) = ( 0 + ( Im ` B ) ) )
12	6	imcld	|- ( ph -> ( Im ` B ) e. RR )
13	12	recnd	|- ( ph -> ( Im ` B ) e. CC )
14	13	addid2d	|- ( ph -> ( 0 + ( Im ` B ) ) = ( Im ` B ) )
15	11 14	eqtrd	|- ( ph -> ( ( Im ` A ) + ( Im ` B ) ) = ( Im ` B ) )
16	15	eqeq1d	|- ( ph -> ( ( ( Im ` A ) + ( Im ` B ) ) = 0 <-> ( Im ` B ) = 0 ) )
17	5 6	imaddd	|- ( ph -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
18	17	eqeq1d	|- ( ph -> ( ( Im ` ( A + B ) ) = 0 <-> ( ( Im ` A ) + ( Im ` B ) ) = 0 ) )
19		reim0b	|- ( B e. CC -> ( B e. RR <-> ( Im ` B ) = 0 ) )
20	6 19	syl	|- ( ph -> ( B e. RR <-> ( Im ` B ) = 0 ) )
21	16 18 20	3bitr4d	|- ( ph -> ( ( Im ` ( A + B ) ) = 0 <-> B e. RR ) )
22	9 21	bitrd	|- ( ph -> ( ( A + B ) e. RR <-> B e. RR ) )
23	22	notbid	|- ( ph -> ( -. ( A + B ) e. RR <-> -. B e. RR ) )
24	4 23	syl5bb	|- ( ph -> ( ( A + B ) e/ RR <-> -. B e. RR ) )
25	3 24	mpbird	|- ( ph -> ( A + B ) e/ RR )