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 e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( I mod N ) = ( J mod N ) <-> I = J ) )

Proof

Step Hyp Ref Expression
1 zmodidfzoimp 
 |-  ( I e. ( 0 ..^ N ) -> ( I mod N ) = I )
2 zmodidfzoimp 
 |-  ( J e. ( 0 ..^ N ) -> ( J mod N ) = J )
3 1 2 eqeqan12d 
 |-  ( ( I e. ( 0 ..^ N ) /\ J e. ( 0 ..^ N ) ) -> ( ( I mod N ) = ( J mod N ) <-> I = J ) )