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 
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> ( ( ( A x. C ) mod P ) = ( ( B x. C ) mod P ) <-> ( A mod P ) = ( B mod P ) ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 1 ad2antrl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> P e. NN )
3 coprm 
 |-  ( ( P e. Prime /\ C e. ZZ ) -> ( -. P || C <-> ( P gcd C ) = 1 ) )
4 prmz 
 |-  ( P e. Prime -> P e. ZZ )
5 gcdcom 
 |-  ( ( P e. ZZ /\ C e. ZZ ) -> ( P gcd C ) = ( C gcd P ) )
6 4 5 sylan 
 |-  ( ( P e. Prime /\ C e. ZZ ) -> ( P gcd C ) = ( C gcd P ) )
7 6 eqeq1d 
 |-  ( ( P e. Prime /\ C e. ZZ ) -> ( ( P gcd C ) = 1 <-> ( C gcd P ) = 1 ) )
8 3 7 bitrd 
 |-  ( ( P e. Prime /\ C e. ZZ ) -> ( -. P || C <-> ( C gcd P ) = 1 ) )
9 8 ancoms 
 |-  ( ( C e. ZZ /\ P e. Prime ) -> ( -. P || C <-> ( C gcd P ) = 1 ) )
10 9 biimpd 
 |-  ( ( C e. ZZ /\ P e. Prime ) -> ( -. P || C -> ( C gcd P ) = 1 ) )
11 10 expimpd 
 |-  ( C e. ZZ -> ( ( P e. Prime /\ -. P || C ) -> ( C gcd P ) = 1 ) )
12 11 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( P e. Prime /\ -. P || C ) -> ( C gcd P ) = 1 ) )
13 12 imp 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> ( C gcd P ) = 1 )
14 2 13 jca 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> ( P e. NN /\ ( C gcd P ) = 1 ) )
15 cncongrcoprm 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. NN /\ ( C gcd P ) = 1 ) ) -> ( ( ( A x. C ) mod P ) = ( ( B x. C ) mod P ) <-> ( A mod P ) = ( B mod P ) ) )
16 14 15 syldan 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( P e. Prime /\ -. P || C ) ) -> ( ( ( A x. C ) mod P ) = ( ( B x. C ) mod P ) <-> ( A mod P ) = ( B mod P ) ) )