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

Metamath Proof Explorer

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 ..^ 𝑁 ) ) )