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⁢CmodP=B⁢CmodP↔AmodP=BmodP

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↔PgcdC=1
4 prmz ⊢P∈ℙ→P∈ℤ
5 gcdcom ⊢P∈ℤ∧C∈ℤ→PgcdC=CgcdP
6 4 5 sylan ⊢P∈ℙ∧C∈ℤ→PgcdC=CgcdP
7 6 eqeq1d ⊢P∈ℙ∧C∈ℤ→PgcdC=1↔CgcdP=1
8 3 7 bitrd ⊢P∈ℙ∧C∈ℤ→¬P∥C↔CgcdP=1
9 8 ancoms ⊢C∈ℤ∧P∈ℙ→¬P∥C↔CgcdP=1
10 9 biimpd ⊢C∈ℤ∧P∈ℙ→¬P∥C→CgcdP=1
11 10 expimpd ⊢C∈ℤ→P∈ℙ∧¬P∥C→CgcdP=1
12 11 3ad2ant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→P∈ℙ∧¬P∥C→CgcdP=1
13 12 imp ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧P∈ℙ∧¬P∥C→CgcdP=1
14 2 13 jca ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧P∈ℙ∧¬P∥C→P∈ℕ∧CgcdP=1
15 cncongrcoprm ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧P∈ℕ∧CgcdP=1→A⁢CmodP=B⁢CmodP↔AmodP=BmodP
16 14 15 syldan ⊢A∈ℤ∧B∈ℤ∧C∈ℤ∧P∈ℙ∧¬P∥C→A⁢CmodP=B⁢CmodP↔AmodP=BmodP