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 syl6req 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