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 𝑁 ) ) )