This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 greatest 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