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 than the modulus. (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion difltmodne ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A mod N ≠ B mod N

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → N ∈ ℕ
2 zsubcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A − B ∈ ℤ
3 simpl ⊢ 1 ≤ A − B ∧ A − B < N → 1 ≤ A − B
4 2 3 anim12i ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B ∈ ℤ ∧ 1 ≤ A − B
5 4 3adant1 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B ∈ ℤ ∧ 1 ≤ A − B
6 elnnz1 ⊢ A − B ∈ ℕ ↔ A − B ∈ ℤ ∧ 1 ≤ A − B
7 5 6 sylibr ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B ∈ ℕ
8 simp3r ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B < N
9 elfzo1 ⊢ A − B ∈ 1 ..^ N ↔ A − B ∈ ℕ ∧ N ∈ ℕ ∧ A − B < N
10 7 1 8 9 syl3anbrc ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B ∈ 1 ..^ N
11 nnz ⊢ N ∈ ℕ → N ∈ ℤ
12 11 3ad2ant1 ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → N ∈ ℤ
13 fzoval ⊢ N ∈ ℤ → 1 ..^ N = 1 … N − 1
14 12 13 syl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → 1 ..^ N = 1 … N − 1
15 10 14 eleqtrd ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A − B ∈ 1 … N − 1
16 fzm1ndvds ⊢ N ∈ ℕ ∧ A − B ∈ 1 … N − 1 → ¬ N ∥ A − B
17 1 15 16 syl2anc ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → ¬ N ∥ A − B
18 3simpa ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ
19 3anass ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ↔ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ
20 18 19 sylibr ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ
21 moddvds ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → A mod N = B mod N ↔ N ∥ A − B
22 20 21 syl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A mod N = B mod N ↔ N ∥ A − B
23 17 22 mtbird ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → ¬ A mod N = B mod N
24 23 neqned ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ 1 ≤ A − B ∧ A − B < N → A mod N ≠ B mod N