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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 1 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐴 − 𝐵 ) < 𝑁 ) ) → ( 𝐴 mod 𝑁 ) ≠ ( 𝐵 mod 𝑁 ) )

Proof

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