zmodidfzoimp

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

		Ref	Expression
	Assertion	zmodidfzoimp	$⊢ M \in (0 ..^N) \to M \mod N = M$

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ M \in (0 ..^N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ \land M < N)$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3	2	anim1i	$⊢ (M \in ℕ_{0} \land N \in ℕ) \to (M \in ℤ \land N \in ℕ)$
4	3	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ \land M < N) \to (M \in ℤ \land N \in ℕ)$
5	1 4	sylbi	$⊢ M \in (0 ..^N) \to (M \in ℤ \land N \in ℕ)$
6		zmodidfzo	$⊢ (M \in ℤ \land N \in ℕ) \to (M \mod N = M \leftrightarrow M \in (0 ..^N))$
7	6	biimprd	$⊢ (M \in ℤ \land N \in ℕ) \to (M \in (0 ..^N) \to M \mod N = M)$
8	5 7	mpcom	$⊢ M \in (0 ..^N) \to M \mod N = M$

Metamath Proof Explorer