Theorem cncongr

Description: Cancellability of Congruences (see ProofWiki "Cancellability of Congruences, https://proofwiki.org/wiki/Cancellability_of_Congruences , 10-Jul-2021): Two products with a common factor are congruent modulo a positive integer iff the other factors are congruent modulo the integer divided by the greates common divisor of the integer and the common factor. See also Theorem 5.4 "Cancellation law" in ApostolNT p. 109. (Contributed by AV, 13-Jul-2021)

	Ref	Expression
Assertion	cncongr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cncongr1	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
2		cncongr2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )
3	1 2	impbid	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )