congr

Description: Definition of congruence by integer multiple (see ProofWiki "Congruence (Number Theory)", 11-Jul-2021, https://proofwiki.org/wiki/Definition:Congruence_(Number_Theory) ): An integer A is congruent to an integer B modulo M if their difference is a multiple of M . See also the definition in ApostolNT p. 104: "... a is congruent to b modulo m , and we write a == b (mod m ) if m divides the difference a - b ", or Wikipedia "Modular arithmetic - Congruence", https://en.wikipedia.org/wiki/Modular_arithmetic#Congruence , 11-Jul-2021,: "Given an integer n > 1, called a modulus, two integers are said to be congruent modulo n, if n is a divisor of their difference (i.e., if there is an integer k such that a-b = kn)". (Contributed by AV, 11-Jul-2021)

		Ref	Expression
	Assertion	congr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		moddvds	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 − 𝐵 ) ) )
2	1	3coml	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 − 𝐵 ) ) )
3		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
4	3	nnzd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℤ )
5		zsubcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
6	5	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
7		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = ( 𝐴 − 𝐵 ) ) )
8	4 6 7	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = ( 𝐴 − 𝐵 ) ) )
9	2 8	bitrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = ( 𝐴 − 𝐵 ) ) )

Metamath Proof Explorer

Theorem congr

Proof