Metamath Proof Explorer

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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ M = N C gcd N → A ⁢ C mod N = B ⁢ C mod N ↔ A mod M = B mod M

Proof

Step Hyp Ref Expression
1 cncongr1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ M = N C gcd N → A ⁢ C mod N = B ⁢ C mod N → A mod M = B mod M
2 cncongr2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ M = N C gcd N → A mod M = B mod M → A ⁢ C mod N = B ⁢ C mod N
3 1 2 impbid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ M = N C gcd N → A ⁢ C mod N = B ⁢ C mod N ↔ A mod M = B mod M