This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difmod0

Description: The difference of two integers modulo a positive integer equals zero iff the two integers are equal modulo the positive integer. (Contributed by AV, 15-Nov-2025)

Ref Expression
Assertion difmod0 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A − B mod N = 0 ↔ A mod N = B mod N

Proof

Step Hyp Ref Expression
1 zcn ⊢ A ∈ ℤ → A ∈ ℂ
2 zcn ⊢ B ∈ ℤ → B ∈ ℂ
3 1 2 anim12i ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℂ ∧ B ∈ ℂ
4 3 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∈ ℂ ∧ B ∈ ℂ
5 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 4 5 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A + − B = A − B
7 6 eqcomd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A − B = A + − B
8 7 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A − B mod N = A + − B mod N
9 8 eqeq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A − B mod N = 0 ↔ A + − B mod N = 0
10 znegcl ⊢ B ∈ ℤ → − B ∈ ℤ
11 summodnegmod ⊢ A ∈ ℤ ∧ − B ∈ ℤ ∧ N ∈ ℕ → A + − B mod N = 0 ↔ A mod N = − − B mod N
12 10 11 syl3an2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A + − B mod N = 0 ↔ A mod N = − − B mod N
13 2 negnegd ⊢ B ∈ ℤ → − − B = B
14 13 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → − − B = B
15 14 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → − − B mod N = B mod N
16 15 eqeq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A mod N = − − B mod N ↔ A mod N = B mod N
17 9 12 16 3bitrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A − B mod N = 0 ↔ A mod N = B mod N