Theorem zntos

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=\mathbb{Z}/N\mathbb{Z}$$
Assertion	zntos	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Toset}$$

Proof

Step	Hyp	Ref	Expression
1		zntos.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		eqid	$$⊢{\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}$$
3		eqid	$$⊢if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
4		eqid	$$⊢{\le }_Y={\le }_Y$$
5		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
6	1 2 3 4 5	zntoslem	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Toset}$$