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 | $${\u22a2}1\ne 0$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c1 | $${class}1$$ | |
1 | cc0 | $${class}0$$ | |
2 | 0 1 | wne | $${wff}1\ne 0$$ |