Theorem cndivrenred

Description: The quotient of an imaginary number and a real 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 ) )
	cndivrenred.n	|- ( ph -> A =/= 0 )
Assertion	cndivrenred	|- ( ph -> ( B / A ) e/ RR )

Proof

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