Theorem cncongrprm

Description: Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021)

	Ref	Expression
Assertion	cncongrprm	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑃 ) = ( ( 𝐵 · 𝐶 ) mod 𝑃 ) ↔ ( 𝐴 mod 𝑃 ) = ( 𝐵 mod 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2	1	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) ) → 𝑃 ∈ ℕ )
3		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐶 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐶 ↔ ( 𝑃 gcd 𝐶 ) = 1 ) )
4		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
5		gcdcom	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝑃 gcd 𝐶 ) = ( 𝐶 gcd 𝑃 ) )
6	4 5	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐶 ∈ ℤ ) → ( 𝑃 gcd 𝐶 ) = ( 𝐶 gcd 𝑃 ) )
7	6	eqeq1d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐶 ∈ ℤ ) → ( ( 𝑃 gcd 𝐶 ) = 1 ↔ ( 𝐶 gcd 𝑃 ) = 1 ) )
8	3 7	bitrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐶 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐶 ↔ ( 𝐶 gcd 𝑃 ) = 1 ) )
9	8	ancoms	⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ¬ 𝑃 ∥ 𝐶 ↔ ( 𝐶 gcd 𝑃 ) = 1 ) )
10	9	biimpd	⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ¬ 𝑃 ∥ 𝐶 → ( 𝐶 gcd 𝑃 ) = 1 ) )
11	10	expimpd	⊢ ( 𝐶 ∈ ℤ → ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) → ( 𝐶 gcd 𝑃 ) = 1 ) )
12	11	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) → ( 𝐶 gcd 𝑃 ) = 1 ) )
13	12	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) ) → ( 𝐶 gcd 𝑃 ) = 1 )
14	2 13	jca	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) ) → ( 𝑃 ∈ ℕ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) )
15		cncongrcoprm	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑃 ) = ( ( 𝐵 · 𝐶 ) mod 𝑃 ) ↔ ( 𝐴 mod 𝑃 ) = ( 𝐵 mod 𝑃 ) ) )
16	14 15	syldan	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶 ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑃 ) = ( ( 𝐵 · 𝐶 ) mod 𝑃 ) ↔ ( 𝐴 mod 𝑃 ) = ( 𝐵 mod 𝑃 ) ) )