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

Metamath Proof Explorer

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