Metamath Proof Explorer

Theorem ine0

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

Ref Expression
Assertion ine0 
|- _i =/= 0

Proof

Step Hyp Ref Expression
1 ax-1ne0 
 |-  1 =/= 0
2 1 neii 
 |-  -. 1 = 0
3 oveq2 
 |-  ( _i = 0 -> ( _i x. _i ) = ( _i x. 0 ) )
4 ax-icn 
 |-  _i e. CC
5 4 mul01i 
 |-  ( _i x. 0 ) = 0
6 3 5 eqtr2di 
 |-  ( _i = 0 -> 0 = ( _i x. _i ) )
7 6 oveq1d 
 |-  ( _i = 0 -> ( 0 + 1 ) = ( ( _i x. _i ) + 1 ) )
8 ax-1cn 
 |-  1 e. CC
9 8 addid2i 
 |-  ( 0 + 1 ) = 1
10 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
11 7 9 10 3eqtr3g 
 |-  ( _i = 0 -> 1 = 0 )
12 2 11 mto 
 |-  -. _i = 0
13 12 neir 
 |-  _i =/= 0