This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ℤ/Nℤ
Assertion zntos ⊢ N ∈ ℕ 0 → Y ∈ Toset

Proof

Step Hyp Ref Expression
1 zntos.y ⊢ Y = ℤ/Nℤ
2 eqid ⊢ ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N = ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N
3 eqid ⊢ if N = 0 ℤ 0 ..^ N = if N = 0 ℤ 0 ..^ N
4 eqid ⊢ ≤ Y = ≤ Y
5 eqid ⊢ Base Y = Base Y
6 1 2 3 4 5 zntoslem ⊢ N ∈ ℕ 0 → Y ∈ Toset