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 ine0
 |-  _i =/= 0
2 1 neii
 |-  -. _i = 0
3 0lt1
 |-  0 < 1
4 0re
 |-  0 e. RR
5 1re
 |-  1 e. RR
6 4 5 ltnsymi
 |-  ( 0 < 1 -> -. 1 < 0 )
7 3 6 ax-mp
 |-  -. 1 < 0
8 ixi
 |-  ( _i x. _i ) = -u 1
9 5 renegcli
 |-  -u 1 e. RR
10 8 9 eqeltri
 |-  ( _i x. _i ) e. RR
11 4 10 5 ltadd1i
 |-  ( 0 < ( _i x. _i ) <-> ( 0 + 1 ) < ( ( _i x. _i ) + 1 ) )
12 ax-1cn
 |-  1 e. CC
13 12 addid2i
 |-  ( 0 + 1 ) = 1
14 ax-i2m1
 |-  ( ( _i x. _i ) + 1 ) = 0
15 13 14 breq12i
 |-  ( ( 0 + 1 ) < ( ( _i x. _i ) + 1 ) <-> 1 < 0 )
16 11 15 bitri
 |-  ( 0 < ( _i x. _i ) <-> 1 < 0 )
17 7 16 mtbir
 |-  -. 0 < ( _i x. _i )
18 msqgt0
 |-  ( ( _i e. RR /\ _i =/= 0 ) -> 0 < ( _i x. _i ) )
19 18 ex
 |-  ( _i e. RR -> ( _i =/= 0 -> 0 < ( _i x. _i ) ) )
20 19 necon1bd
 |-  ( _i e. RR -> ( -. 0 < ( _i x. _i ) -> _i = 0 ) )
21 17 20 mpi
 |-  ( _i e. RR -> _i = 0 )
22 2 21 mto
 |-  -. _i e. RR