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 ⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion mod2addne ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑋 + 𝐴 ) mod 𝑁 ) ≠ ( ( 𝑋 + 𝐵 ) mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mod2addne.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
2 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ )
3 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
4 3 3adant1 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
5 4 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
6 elfzolt2 ⊢ ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝑁 )
7 6 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝑁 )
8 modlt0b ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝑁 ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 − 𝐵 ) = 0 ) )
9 2 5 7 8 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 − 𝐵 ) = 0 ) )
10 fveq2 ⊢ ( ( 𝐴 − 𝐵 ) = 0 → ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ 0 ) )
11 10 eleq1d ⊢ ( ( 𝐴 − 𝐵 ) = 0 → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ↔ ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) ) )
12 11 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( 𝐴 − 𝐵 ) = 0 ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ↔ ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) ) )
13 abs0 ⊢ ( abs ‘ 0 ) = 0
14 13 eleq1i ⊢ ( ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) ↔ 0 ∈ ( 1 ..^ 𝑁 ) )
15 14 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) ↔ 0 ∈ ( 1 ..^ 𝑁 ) ) )
16 elfzo1 ⊢ ( 0 ∈ ( 1 ..^ 𝑁 ) ↔ ( 0 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 0 < 𝑁 ) )
17 0nnn ⊢ ¬ 0 ∈ ℕ
18 17 pm2.21i ⊢ ( 0 ∈ ℕ → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 )
19 18 3ad2ant1 ⊢ ( ( 0 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 0 < 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 )
20 16 19 sylbi ⊢ ( 0 ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 )
21 20 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 0 ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
22 15 21 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
23 22 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( 𝐴 − 𝐵 ) = 0 ) → ( ( abs ‘ 0 ) ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
24 12 23 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) ∧ ( 𝐴 − 𝐵 ) = 0 ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
25 24 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 − 𝐵 ) = 0 → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) ) )
26 25 com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) → ( ( 𝐴 − 𝐵 ) = 0 → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) ) )
27 26 3impia ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 − 𝐵 ) = 0 → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
28 9 27 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
29 28 pm2.01d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ¬ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 )
30 simp2 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
31 30 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
32 simp3 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
33 32 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
34 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝑁 ∈ ℕ )
35 31 33 34 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
36 35 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
37 difmod0 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
38 36 37 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
39 29 38 mtbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ¬ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) )
40 elfzoelz ⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ℤ )
41 40 1 eleq2s ⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ )
42 41 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑋 ∈ ℤ )
43 42 zcnd ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑋 ∈ ℂ )
44 30 zcnd ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℂ )
45 43 44 addcomd ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑋 + 𝐴 ) = ( 𝐴 + 𝑋 ) )
46 45 oveq1d ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑋 + 𝐴 ) mod 𝑁 ) = ( ( 𝐴 + 𝑋 ) mod 𝑁 ) )
47 32 zcnd ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
48 43 47 addcomd ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑋 + 𝐵 ) = ( 𝐵 + 𝑋 ) )
49 48 oveq1d ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑋 + 𝐵 ) mod 𝑁 ) = ( ( 𝐵 + 𝑋 ) mod 𝑁 ) )
50 46 49 eqeq12d ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝑋 + 𝐴 ) mod 𝑁 ) = ( ( 𝑋 + 𝐵 ) mod 𝑁 ) ↔ ( ( 𝐴 + 𝑋 ) mod 𝑁 ) = ( ( 𝐵 + 𝑋 ) mod 𝑁 ) ) )
51 50 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑋 + 𝐴 ) mod 𝑁 ) = ( ( 𝑋 + 𝐵 ) mod 𝑁 ) ↔ ( ( 𝐴 + 𝑋 ) mod 𝑁 ) = ( ( 𝐵 + 𝑋 ) mod 𝑁 ) ) )
52 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
53 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
54 52 53 anim12i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
55 54 3adant1 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
56 55 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
57 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
58 41 zred ⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ℝ )
59 58 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑋 ∈ ℝ )
60 57 59 anim12ci ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝑋 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
61 56 60 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) )
62 61 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) )
63 modaddb ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ ( ( 𝐴 + 𝑋 ) mod 𝑁 ) = ( ( 𝐵 + 𝑋 ) mod 𝑁 ) ) )
64 62 63 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ ( ( 𝐴 + 𝑋 ) mod 𝑁 ) = ( ( 𝐵 + 𝑋 ) mod 𝑁 ) ) )
65 51 64 bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑋 + 𝐴 ) mod 𝑁 ) = ( ( 𝑋 + 𝐵 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
66 65 necon3abid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑋 + 𝐴 ) mod 𝑁 ) ≠ ( ( 𝑋 + 𝐵 ) mod 𝑁 ) ↔ ¬ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
67 39 66 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑋 + 𝐴 ) mod 𝑁 ) ≠ ( ( 𝑋 + 𝐵 ) mod 𝑁 ) )