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	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	Assertion	zntos	⊢ ( 𝑁 ∈ ℕ₀ → 𝑌 ∈ Toset )

Proof

Step	Hyp	Ref	Expression
1		zntos.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		eqid	⊢ ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
3		eqid	⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
4		eqid	⊢ ( le ‘ 𝑌 ) = ( le ‘ 𝑌 )
5		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6	1 2 3 4 5	zntoslem	⊢ ( 𝑁 ∈ ℕ₀ → 𝑌 ∈ Toset )