This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )