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∈ℕ∧CgcdN=1→A⁢CmodN=B⁢CmodN↔AmodN=BmodN

Proof

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