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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )

Proof

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