Metamath Proof Explorer

Theorem cncongrcoprm

Description: Corollary 1 of Cancellability of Congruences: Two products with a common factor are congruent modulo an integer being coprime to the common factor iff the other factors are congruent modulo the integer. (Contributed by AV, 13-Jul-2021)

Ref Expression
Assertion cncongrcoprm ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ C gcd N = 1 → A ⁢ C mod N = B ⁢ C mod N ↔ A mod N = B mod N

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℕ ∧ C gcd N = 1 → N ∈ ℕ
2 nncn ⊢ N ∈ ℕ → N ∈ ℂ
3 2 div1d ⊢ N ∈ ℕ → N 1 = N
4 oveq2 ⊢ C gcd N = 1 → N C gcd N = N 1
5 4 eqcomd ⊢ C gcd N = 1 → N 1 = N C gcd N
6 3 5 sylan9req ⊢ N ∈ ℕ ∧ C gcd N = 1 → N = N C gcd N
7 1 6 jca ⊢ N ∈ ℕ ∧ C gcd N = 1 → N ∈ ℕ ∧ N = N C gcd N
8 cncongr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ N = N C gcd N → A ⁢ C mod N = B ⁢ C mod N ↔ A mod N = B mod N
9 7 8 sylan2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ N ∈ ℕ ∧ C gcd N = 1 → A ⁢ C mod N = B ⁢ C mod N ↔ A mod N = B mod N