Metamath Proof Explorer

Theorem rimul

Description: A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion rimul 
|- ( ( A e. RR /\ ( _i x. A ) e. RR ) -> A = 0 )

Proof

Step Hyp Ref Expression
1 inelr 
 |-  -. _i e. RR
2 ax-icn 
 |-  _i e. CC
3 2 a1i 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> _i e. CC )
4 simpll 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> A e. RR )
5 4 recnd 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> A e. CC )
6 simpr 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> A =/= 0 )
7 3 5 6 divcan4d 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> ( ( _i x. A ) / A ) = _i )
8 simplr 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> ( _i x. A ) e. RR )
9 8 4 6 redivcld 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> ( ( _i x. A ) / A ) e. RR )
10 7 9 eqeltrrd 
 |-  ( ( ( A e. RR /\ ( _i x. A ) e. RR ) /\ A =/= 0 ) -> _i e. RR )
11 10 ex 
 |-  ( ( A e. RR /\ ( _i x. A ) e. RR ) -> ( A =/= 0 -> _i e. RR ) )
12 11 necon1bd 
 |-  ( ( A e. RR /\ ( _i x. A ) e. RR ) -> ( -. _i e. RR -> A = 0 ) )
13 1 12 mpi 
 |-  ( ( A e. RR /\ ( _i x. A ) e. RR ) -> A = 0 )