Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 . (Contributed by NM, 19-Mar-1996) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax1ne0 | |- 1 =/= 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1ne0sr | |- -. 1R = 0R |
|
| 2 | 1sr | |- 1R e. R. |
|
| 3 | 2 | elexi | |- 1R e. _V |
| 4 | 3 | eqresr | |- ( <. 1R , 0R >. = <. 0R , 0R >. <-> 1R = 0R ) |
| 5 | 1 4 | mtbir | |- -. <. 1R , 0R >. = <. 0R , 0R >. |
| 6 | df-1 | |- 1 = <. 1R , 0R >. |
|
| 7 | df-0 | |- 0 = <. 0R , 0R >. |
|
| 8 | 6 7 | eqeq12i | |- ( 1 = 0 <-> <. 1R , 0R >. = <. 0R , 0R >. ) |
| 9 | 5 8 | mtbir | |- -. 1 = 0 |
| 10 | 9 | neir | |- 1 =/= 0 |