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 𝑁 ) ) )