Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 . (Contributed by NM, 29-Jan-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | ax-1ne0 | ⊢ 1 ≠ 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c1 | ⊢ 1 | |
1 | cc0 | ⊢ 0 | |
2 | 0 1 | wne | ⊢ 1 ≠ 0 |