Metamath Proof Explorer

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 bitrid 
 |-  ( ph -> ( ( B / A ) e/ RR <-> -. B e. RR ) )
22 4 21 mpbird 
 |-  ( ph -> ( B / A ) e/ RR )