Description: The imaginary unit _i is not zero. (Contributed by NM, 6-May-1999)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ine0 | ⊢ i ≠ 0 |
| 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 |