Theorem recnmulnred

Description: The product 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 ) )
	cndivrenred.n	|- ( ph -> A =/= 0 )
Assertion	recnmulnred	|- ( ph -> ( A x. B ) 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	|- ( ( A x. B ) e/ RR <-> -. ( A x. B ) e. RR )
6	2	eldifad	|- ( ph -> B e. CC )
7		mulre	|- ( ( B e. CC /\ A e. RR /\ A =/= 0 ) -> ( B e. RR <-> ( A x. B ) e. RR ) )
8	6 1 3 7	syl3anc	|- ( ph -> ( B e. RR <-> ( A x. B ) e. RR ) )
9	8	bicomd	|- ( ph -> ( ( A x. B ) e. RR <-> B e. RR ) )
10	9	notbid	|- ( ph -> ( -. ( A x. B ) e. RR <-> -. B e. RR ) )
11	5 10	bitrid	|- ( ph -> ( ( A x. B ) e/ RR <-> -. B e. RR ) )
12	4 11	mpbird	|- ( ph -> ( A x. B ) e/ RR )