Metamath Proof Explorer


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 syl5bb
 |-  ( ph -> ( ( A x. B ) e/ RR <-> -. B e. RR ) )
12 4 11 mpbird
 |-  ( ph -> ( A x. B ) e/ RR )