Metamath Proof Explorer

Theorem mod2addne

Description: The sums of a nonnegative integer less than the modulus and two integers whose difference is less than the modulus are not equal modulo the modulus. (Contributed by AV, 15-Nov-2025)

Ref Expression
Hypothesis mod2addne.i 
|- I = ( 0 ..^ N )
Assertion mod2addne 
|- ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( X + A ) mod N ) =/= ( ( X + B ) mod N ) )

Proof

Step Hyp Ref Expression
1 mod2addne.i 
 |-  I = ( 0 ..^ N )
2 simp1 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> N e. NN )
3 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
4 3 3adant1 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
5 4 3ad2ant2 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( A - B ) e. ZZ )
6 elfzolt2 
 |-  ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) -> ( abs ` ( A - B ) ) < N )
7 6 3ad2ant3 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( abs ` ( A - B ) ) < N )
8 modlt0b 
 |-  ( ( N e. NN /\ ( A - B ) e. ZZ /\ ( abs ` ( A - B ) ) < N ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A - B ) = 0 ) )
9 2 5 7 8 syl3anc 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A - B ) = 0 ) )
10 fveq2 
 |-  ( ( A - B ) = 0 -> ( abs ` ( A - B ) ) = ( abs ` 0 ) )
11 10 eleq1d 
 |-  ( ( A - B ) = 0 -> ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) <-> ( abs ` 0 ) e. ( 1 ..^ N ) ) )
12 11 adantl 
 |-  ( ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) /\ ( A - B ) = 0 ) -> ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) <-> ( abs ` 0 ) e. ( 1 ..^ N ) ) )
13 abs0 
 |-  ( abs ` 0 ) = 0
14 13 eleq1i 
 |-  ( ( abs ` 0 ) e. ( 1 ..^ N ) <-> 0 e. ( 1 ..^ N ) )
15 14 a1i 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( ( abs ` 0 ) e. ( 1 ..^ N ) <-> 0 e. ( 1 ..^ N ) ) )
16 elfzo1 
 |-  ( 0 e. ( 1 ..^ N ) <-> ( 0 e. NN /\ N e. NN /\ 0 < N ) )
17 0nnn 
 |-  -. 0 e. NN
18 17 pm2.21i 
 |-  ( 0 e. NN -> -. ( ( A - B ) mod N ) = 0 )
19 18 3ad2ant1 
 |-  ( ( 0 e. NN /\ N e. NN /\ 0 < N ) -> -. ( ( A - B ) mod N ) = 0 )
20 16 19 sylbi 
 |-  ( 0 e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 )
21 20 a1i 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( 0 e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 ) )
22 15 21 sylbid 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( ( abs ` 0 ) e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 ) )
23 22 adantr 
 |-  ( ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) /\ ( A - B ) = 0 ) -> ( ( abs ` 0 ) e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 ) )
24 12 23 sylbid 
 |-  ( ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) /\ ( A - B ) = 0 ) -> ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 ) )
25 24 ex 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( ( A - B ) = 0 -> ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) -> -. ( ( A - B ) mod N ) = 0 ) ) )
26 25 com23 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( ( abs ` ( A - B ) ) e. ( 1 ..^ N ) -> ( ( A - B ) = 0 -> -. ( ( A - B ) mod N ) = 0 ) ) )
27 26 3impia 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( A - B ) = 0 -> -. ( ( A - B ) mod N ) = 0 ) )
28 9 27 sylbid 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( A - B ) mod N ) = 0 -> -. ( ( A - B ) mod N ) = 0 ) )
29 28 pm2.01d 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> -. ( ( A - B ) mod N ) = 0 )
30 simp2 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
31 30 adantl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> A e. ZZ )
32 simp3 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
33 32 adantl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> B e. ZZ )
34 simpl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> N e. NN )
35 31 33 34 3jca 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( A e. ZZ /\ B e. ZZ /\ N e. NN ) )
36 35 3adant3 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( A e. ZZ /\ B e. ZZ /\ N e. NN ) )
37 difmod0 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A mod N ) = ( B mod N ) ) )
38 36 37 syl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( A - B ) mod N ) = 0 <-> ( A mod N ) = ( B mod N ) ) )
39 29 38 mtbid 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> -. ( A mod N ) = ( B mod N ) )
40 elfzoelz 
 |-  ( X e. ( 0 ..^ N ) -> X e. ZZ )
41 40 1 eleq2s 
 |-  ( X e. I -> X e. ZZ )
42 41 3ad2ant1 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> X e. ZZ )
43 42 zcnd 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> X e. CC )
44 30 zcnd 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> A e. CC )
45 43 44 addcomd 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( X + A ) = ( A + X ) )
46 45 oveq1d 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( ( X + A ) mod N ) = ( ( A + X ) mod N ) )
47 32 zcnd 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> B e. CC )
48 43 47 addcomd 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( X + B ) = ( B + X ) )
49 48 oveq1d 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( ( X + B ) mod N ) = ( ( B + X ) mod N ) )
50 46 49 eqeq12d 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( ( ( X + A ) mod N ) = ( ( X + B ) mod N ) <-> ( ( A + X ) mod N ) = ( ( B + X ) mod N ) ) )
51 50 3ad2ant2 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( X + A ) mod N ) = ( ( X + B ) mod N ) <-> ( ( A + X ) mod N ) = ( ( B + X ) mod N ) ) )
52 zre 
 |-  ( A e. ZZ -> A e. RR )
53 zre 
 |-  ( B e. ZZ -> B e. RR )
54 52 53 anim12i 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A e. RR /\ B e. RR ) )
55 54 3adant1 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> ( A e. RR /\ B e. RR ) )
56 55 adantl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( A e. RR /\ B e. RR ) )
57 nnrp 
 |-  ( N e. NN -> N e. RR+ )
58 41 zred 
 |-  ( X e. I -> X e. RR )
59 58 3ad2ant1 
 |-  ( ( X e. I /\ A e. ZZ /\ B e. ZZ ) -> X e. RR )
60 57 59 anim12ci 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( X e. RR /\ N e. RR+ ) )
61 56 60 jca 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) ) -> ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ N e. RR+ ) ) )
62 61 3adant3 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ N e. RR+ ) ) )
63 modaddb 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ N e. RR+ ) ) -> ( ( A mod N ) = ( B mod N ) <-> ( ( A + X ) mod N ) = ( ( B + X ) mod N ) ) )
64 62 63 syl 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( A mod N ) = ( B mod N ) <-> ( ( A + X ) mod N ) = ( ( B + X ) mod N ) ) )
65 51 64 bitr4d 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( X + A ) mod N ) = ( ( X + B ) mod N ) <-> ( A mod N ) = ( B mod N ) ) )
66 65 necon3abid 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( ( X + A ) mod N ) =/= ( ( X + B ) mod N ) <-> -. ( A mod N ) = ( B mod N ) ) )
67 39 66 mpbird 
 |-  ( ( N e. NN /\ ( X e. I /\ A e. ZZ /\ B e. ZZ ) /\ ( abs ` ( A - B ) ) e. ( 1 ..^ N ) ) -> ( ( X + A ) mod N ) =/= ( ( X + B ) mod N ) )