Theorem zmodidfzo

Description: Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018)

	Ref	Expression
Assertion	zmodidfzo	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ..^ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zmodid2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
5	4	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
6	5	eqcomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ... ( 𝑁 − 1 ) ) = ( 0 ..^ 𝑁 ) )
7	6	eleq2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ 𝑀 ∈ ( 0 ..^ 𝑁 ) ) )
8	1 7	bitrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ..^ 𝑁 ) ) )