# 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 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({N}\in ℕ\wedge {C}\mathrm{gcd}{N}=1\right)\right)\to \left({A}{C}\mathrm{mod}{N}={B}{C}\mathrm{mod}{N}↔{A}\mathrm{mod}{N}={B}\mathrm{mod}{N}\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({N}\in ℕ\wedge {C}\mathrm{gcd}{N}=1\right)\to {N}\in ℕ$
2 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
3 2 div1d ${⊢}{N}\in ℕ\to \frac{{N}}{1}={N}$
4 oveq2 ${⊢}{C}\mathrm{gcd}{N}=1\to \frac{{N}}{{C}\mathrm{gcd}{N}}=\frac{{N}}{1}$
5 4 eqcomd ${⊢}{C}\mathrm{gcd}{N}=1\to \frac{{N}}{1}=\frac{{N}}{{C}\mathrm{gcd}{N}}$
6 3 5 sylan9req ${⊢}\left({N}\in ℕ\wedge {C}\mathrm{gcd}{N}=1\right)\to {N}=\frac{{N}}{{C}\mathrm{gcd}{N}}$
7 1 6 jca ${⊢}\left({N}\in ℕ\wedge {C}\mathrm{gcd}{N}=1\right)\to \left({N}\in ℕ\wedge {N}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)$
8 cncongr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({N}\in ℕ\wedge {N}=\frac{{N}}{{C}\mathrm{gcd}{N}}\right)\right)\to \left({A}{C}\mathrm{mod}{N}={B}{C}\mathrm{mod}{N}↔{A}\mathrm{mod}{N}={B}\mathrm{mod}{N}\right)$
9 7 8 sylan2 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℤ\right)\wedge \left({N}\in ℕ\wedge {C}\mathrm{gcd}{N}=1\right)\right)\to \left({A}{C}\mathrm{mod}{N}={B}{C}\mathrm{mod}{N}↔{A}\mathrm{mod}{N}={B}\mathrm{mod}{N}\right)$