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

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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐶 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ )
2 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
3 2 div1d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 1 ) = 𝑁 )
4 oveq2 ⊢ ( ( 𝐶 gcd 𝑁 ) = 1 → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = ( 𝑁 / 1 ) )
5 4 eqcomd ⊢ ( ( 𝐶 gcd 𝑁 ) = 1 → ( 𝑁 / 1 ) = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) )
6 3 5 sylan9req ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 gcd 𝑁 ) = 1 ) → 𝑁 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) )
7 1 6 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 gcd 𝑁 ) = 1 ) → ( 𝑁 ∈ ℕ ∧ 𝑁 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) )
8 cncongr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑁 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
9 7 8 sylan2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐶 gcd 𝑁 ) = 1 ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )