Theorem zmodidfzoimp

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

	Ref	Expression
Assertion	zmodidfzoimp	⊢ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) → ( 𝑀 mod 𝑁 ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑀 < 𝑁 ) )
2		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
3	2	anim1i	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
4	3	3adant3	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑀 < 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
5	1 4	sylbi	⊢ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
6		zmodidfzo	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ 𝑀 ∈ ( 0 ..^ 𝑁 ) ) )
7	6	biimprd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∈ ( 0 ..^ 𝑁 ) → ( 𝑀 mod 𝑁 ) = 𝑀 ) )
8	5 7	mpcom	⊢ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) → ( 𝑀 mod 𝑁 ) = 𝑀 )