Metamath Proof Explorer

Theorem difmod0

Description: The difference of two integers modulo a positive integer equals zero iff the two integers are equal modulo the positive integer. (Contributed by AV, 15-Nov-2025)

Ref Expression
Assertion difmod0 
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A mod N ) = ( B mod N ) ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 zcn 
 |-  ( B e. ZZ -> B e. CC )
3 1 2 anim12i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A e. CC /\ B e. CC ) )
4 3 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A e. CC /\ B e. CC ) )
5 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
6 4 5 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A + -u B ) = ( A - B ) )
7 6 eqcomd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A - B ) = ( A + -u B ) )
8 7 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( A - B ) mod N ) = ( ( A + -u B ) mod N ) )
9 8 eqeq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A - B ) mod N ) = 0 <-> ( ( A + -u B ) mod N ) = 0 ) )
10 znegcl 
 |-  ( B e. ZZ -> -u B e. ZZ )
11 summodnegmod 
 |-  ( ( A e. ZZ /\ -u B e. ZZ /\ N e. NN ) -> ( ( ( A + -u B ) mod N ) = 0 <-> ( A mod N ) = ( -u -u B mod N ) ) )
12 10 11 syl3an2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A + -u B ) mod N ) = 0 <-> ( A mod N ) = ( -u -u B mod N ) ) )
13 2 negnegd 
 |-  ( B e. ZZ -> -u -u B = B )
14 13 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> -u -u B = B )
15 14 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( -u -u B mod N ) = ( B mod N ) )
16 15 eqeq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( A mod N ) = ( -u -u B mod N ) <-> ( A mod N ) = ( B mod N ) ) )
17 9 12 16 3bitrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A mod N ) = ( B mod N ) ) )