Description: The Z/nZ structure is a totally ordered set. (The order is not respected by the operations, except in the case N = 0 when it coincides with the ordering on ZZ .) (Contributed by Mario Carneiro, 15-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | zntos.y | |- Y = ( Z/nZ ` N ) |
|
| Assertion | zntos | |- ( N e. NN0 -> Y e. Toset ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zntos.y | |- Y = ( Z/nZ ` N ) |
|
| 2 | eqid | |- ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) |
|
| 3 | eqid | |- if ( N = 0 , ZZ , ( 0 ..^ N ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) ) |
|
| 4 | eqid | |- ( le ` Y ) = ( le ` Y ) |
|
| 5 | eqid | |- ( Base ` Y ) = ( Base ` Y ) |
|
| 6 | 1 2 3 4 5 | zntoslem | |- ( N e. NN0 -> Y e. Toset ) |