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	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 mod 𝑁 ) = ( 𝐽 mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		zmodidfzoimp	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 mod 𝑁 ) = 𝐼 )
2		zmodidfzoimp	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 mod 𝑁 ) = 𝐽 )
3	1 2	eqeqan12d	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 mod 𝑁 ) = ( 𝐽 mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )