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

Metamath Proof Explorer

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	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (I \mod N = J \mod N \leftrightarrow I = J)$

Step	Hyp	Ref	Expression
1		zmodidfzoimp	$⊢ I \in (0 ..^N) \to I \mod N = I$
2		zmodidfzoimp	$⊢ J \in (0 ..^N) \to J \mod N = J$
3	1 2	eqeqan12d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (I \mod N = J \mod N \leftrightarrow I = J)$