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 · i ) = ( i · 0 ) )
4 ax-icn i ∈ ℂ
5 4 mul01i ( i · 0 ) = 0
6 3 5 eqtr2di ( i = 0 → 0 = ( i · i ) )
7 6 oveq1d ( i = 0 → ( 0 + 1 ) = ( ( i · i ) + 1 ) )
8 ax-1cn 1 ∈ ℂ
9 8 addid2i ( 0 + 1 ) = 1
10 ax-i2m1 ( ( i · i ) + 1 ) = 0
11 7 9 10 3eqtr3g ( i = 0 → 1 = 0 )
12 2 11 mto ¬ i = 0
13 12 neir i ≠ 0