Metamath Proof Explorer

Theorem difltmodne

Description: Two nonnegative integers are not equal modulo a positive modulus if their difference is greater than 0 and less then the modulus. (Contributed by AV, 6-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> N e. NN )
2 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
3 simpl 
 |-  ( ( 1 <_ ( A - B ) /\ ( A - B ) < N ) -> 1 <_ ( A - B ) )
4 2 3 anim12i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( ( A - B ) e. ZZ /\ 1 <_ ( A - B ) ) )
5 4 3adant1 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( ( A - B ) e. ZZ /\ 1 <_ ( A - B ) ) )
6 elnnz1 
 |-  ( ( A - B ) e. NN <-> ( ( A - B ) e. ZZ /\ 1 <_ ( A - B ) ) )
7 5 6 sylibr 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( A - B ) e. NN )
8 simp3r 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( A - B ) < N )
9 elfzo1 
 |-  ( ( A - B ) e. ( 1 ..^ N ) <-> ( ( A - B ) e. NN /\ N e. NN /\ ( A - B ) < N ) )
10 7 1 8 9 syl3anbrc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( A - B ) e. ( 1 ..^ N ) )
11 nnz 
 |-  ( N e. NN -> N e. ZZ )
12 11 3ad2ant1 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> N e. ZZ )
13 fzoval 
 |-  ( N e. ZZ -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
14 12 13 syl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
15 10 14 eleqtrd 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( A - B ) e. ( 1 ... ( N - 1 ) ) )
16 fzm1ndvds 
 |-  ( ( N e. NN /\ ( A - B ) e. ( 1 ... ( N - 1 ) ) ) -> -. N || ( A - B ) )
17 1 15 16 syl2anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> -. N || ( A - B ) )
18 3simpa 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) )
19 3anass 
 |-  ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) <-> ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) ) )
20 18 19 sylibr 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( N e. NN /\ A e. ZZ /\ B e. ZZ ) )
21 moddvds 
 |-  ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )
22 20 21 syl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )
23 17 22 mtbird 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> -. ( A mod N ) = ( B mod N ) )
24 23 neqned 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ ) /\ ( 1 <_ ( A - B ) /\ ( A - B ) < N ) ) -> ( A mod N ) =/= ( B mod N ) )