Theorem zmodid2

Description: Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	zmodid2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
3		modid2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
5		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
6		0z	⊢ 0 ∈ ℤ
7		elfzm11	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
8	6 7	mpan	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
9		3anass	⊢ ( ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
10	8 9	bitrdi	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) ) )
11	5 10	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) ) )
12		ibar	⊢ ( 𝑀 ∈ ℤ → ( ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) ) )
13	12	bicomd	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) ↔ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
14	11 13	sylan9bbr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑀 ∧ 𝑀 < 𝑁 ) ) )
15	4 14	bitr4d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )