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	|- ( ph -> A e. RR )
	recnaddnred.b	|- ( ph -> B e. ( CC \ RR ) )
Assertion	resubcnnred	|- ( 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	subcld	|- ( 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		df-neg	|- -u ( Im ` B ) = ( 0 - ( Im ` B ) )
13	11 12	eqtr4di	|- ( ph -> ( ( Im ` A ) - ( Im ` B ) ) = -u ( Im ` B ) )
14	13	eqeq1d	|- ( ph -> ( ( ( Im ` A ) - ( Im ` B ) ) = 0 <-> -u ( Im ` B ) = 0 ) )
15	5 6	imsubd	|- ( ph -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
16	15	eqeq1d	|- ( ph -> ( ( Im ` ( A - B ) ) = 0 <-> ( ( Im ` A ) - ( Im ` B ) ) = 0 ) )
17		reim0b	|- ( B e. CC -> ( B e. RR <-> ( Im ` B ) = 0 ) )
18	6 17	syl	|- ( ph -> ( B e. RR <-> ( Im ` B ) = 0 ) )
19	6	imcld	|- ( ph -> ( Im ` B ) e. RR )
20	19	recnd	|- ( ph -> ( Im ` B ) e. CC )
21	20	negeq0d	|- ( ph -> ( ( Im ` B ) = 0 <-> -u ( Im ` B ) = 0 ) )
22	18 21	bitrd	|- ( ph -> ( B e. RR <-> -u ( Im ` B ) = 0 ) )
23	14 16 22	3bitr4d	|- ( ph -> ( ( Im ` ( A - B ) ) = 0 <-> B e. RR ) )
24	9 23	bitrd	|- ( ph -> ( ( A - B ) e. RR <-> B e. RR ) )
25	24	notbid	|- ( ph -> ( -. ( A - B ) e. RR <-> -. B e. RR ) )
26	4 25	syl5bb	|- ( ph -> ( ( A - B ) e/ RR <-> -. B e. RR ) )
27	3 26	mpbird	|- ( ph -> ( A - B ) e/ RR )