Theorem vfermltl

Description: Variant of Fermat's little theorem if A is not a multiple of P , see theorem 5.18 in ApostolNT p. 113. (Contributed by AV, 21-Aug-2020) (Proof shortened by AV, 5-Sep-2020)

	Ref	Expression
Assertion	vfermltl	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		phiprm	|- ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
2	1	eqcomd	|- ( P e. Prime -> ( P - 1 ) = ( phi ` P ) )
3	2	3ad2ant1	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P - 1 ) = ( phi ` P ) )
4	3	oveq2d	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A ^ ( P - 1 ) ) = ( A ^ ( phi ` P ) ) )
5	4	oveq1d	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = ( ( A ^ ( phi ` P ) ) mod P ) )
6		prmnn	|- ( P e. Prime -> P e. NN )
7	6	3ad2ant1	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> P e. NN )
8		simp2	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> A e. ZZ )
9		prmz	|- ( P e. Prime -> P e. ZZ )
10	9	anim1ci	|- ( ( P e. Prime /\ A e. ZZ ) -> ( A e. ZZ /\ P e. ZZ ) )
11	10	3adant3	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A e. ZZ /\ P e. ZZ ) )
12		gcdcom	|- ( ( A e. ZZ /\ P e. ZZ ) -> ( A gcd P ) = ( P gcd A ) )
13	11 12	syl	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A gcd P ) = ( P gcd A ) )
14		coprm	|- ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
15	14	biimp3a	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P gcd A ) = 1 )
16	13 15	eqtrd	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( A gcd P ) = 1 )
17		eulerth	|- ( ( P e. NN /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
18	7 8 16 17	syl3anc	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
19	6	nnred	|- ( P e. Prime -> P e. RR )
20		prmgt1	|- ( P e. Prime -> 1 < P )
21	19 20	jca	|- ( P e. Prime -> ( P e. RR /\ 1 < P ) )
22	21	3ad2ant1	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( P e. RR /\ 1 < P ) )
23		1mod	|- ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
24	22 23	syl	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( 1 mod P ) = 1 )
25	5 18 24	3eqtrd	|- ( ( P e. Prime /\ A e. ZZ /\ -. P || A ) -> ( ( A ^ ( P - 1 ) ) mod P ) = 1 )