Theorem modlteq

Description: Two nonnegative integers less than the modulus are equal iff they are equal modulo the modulus. (Contributed by AV, 14-Mar-2021)

	Ref	Expression
Assertion	modlteq	$$⊢\left(I\in \left(0..^N\right)\wedge J\in \left(0..^N\right)\right)\to \left(I\mathrm{mod}N=J\mathrm{mod}N\leftrightarrow I=J\right)$$

Proof

Step	Hyp	Ref	Expression
1		zmodidfzoimp	$$⊢I\in \left(0..^N\right)\to I\mathrm{mod}N=I$$
2		zmodidfzoimp	$$⊢J\in \left(0..^N\right)\to J\mathrm{mod}N=J$$
3	1 2	eqeqan12d	$$⊢\left(I\in \left(0..^N\right)\wedge J\in \left(0..^N\right)\right)\to \left(I\mathrm{mod}N=J\mathrm{mod}N\leftrightarrow I=J\right)$$