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