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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ P ∈ ℙ ∧ ¬ P ∥ C → A ⁢ C mod P = B ⁢ C mod P ↔ A mod P = B mod P

Proof

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