Metamath Proof Explorer

Theorem inelr

Description: The imaginary unit _i is not a real number. (Contributed by NM, 6-May-1999)

Ref Expression
Assertion inelr 
|- -. _i e. RR

Proof

Step Hyp Ref Expression
1 neg1lt0 
 |-  -u 1 < 0
2 neg1rr 
 |-  -u 1 e. RR
3 0re 
 |-  0 e. RR
4 2 3 ltnsymi 
 |-  ( -u 1 < 0 -> -. 0 < -u 1 )
5 1 4 ax-mp 
 |-  -. 0 < -u 1
6 ixi 
 |-  ( _i x. _i ) = -u 1
7 6 breq2i 
 |-  ( 0 < ( _i x. _i ) <-> 0 < -u 1 )
8 5 7 mtbir 
 |-  -. 0 < ( _i x. _i )
9 ine0 
 |-  _i =/= 0
10 msqgt0 
 |-  ( ( _i e. RR /\ _i =/= 0 ) -> 0 < ( _i x. _i ) )
11 9 10 mpan2 
 |-  ( _i e. RR -> 0 < ( _i x. _i ) )
12 8 11 mto 
 |-  -. _i e. RR