Metamath Proof Explorer

Theorem fermltl

Description: Fermat's little theorem. When P is prime, A ^ P == A (mod P ) for any A , see theorem 5.19 in ApostolNT p. 114. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 19-Mar-2022)

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

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 dvdsmodexp 
 |-  ( ( P e. NN /\ P e. NN /\ P || A ) -> ( ( A ^ P ) mod P ) = ( A mod P ) )
3 2 3exp 
 |-  ( P e. NN -> ( P e. NN -> ( P || A -> ( ( A ^ P ) mod P ) = ( A mod P ) ) ) )
4 1 1 3 sylc 
 |-  ( P e. Prime -> ( P || A -> ( ( A ^ P ) mod P ) = ( A mod P ) ) )
5 4 adantr 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P || A -> ( ( A ^ P ) mod P ) = ( A mod P ) ) )
6 coprm 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) )
7 prmz 
 |-  ( P e. Prime -> P e. ZZ )
8 gcdcom 
 |-  ( ( P e. ZZ /\ A e. ZZ ) -> ( P gcd A ) = ( A gcd P ) )
9 7 8 sylan 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P gcd A ) = ( A gcd P ) )
10 9 eqeq1d 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( P gcd A ) = 1 <-> ( A gcd P ) = 1 ) )
11 6 10 bitrd 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( A gcd P ) = 1 ) )
12 simp2 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> A e. ZZ )
13 1 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> P e. NN )
14 13 phicld 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( phi ` P ) e. NN )
15 14 nnnn0d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( phi ` P ) e. NN0 )
16 zexpcl 
 |-  ( ( A e. ZZ /\ ( phi ` P ) e. NN0 ) -> ( A ^ ( phi ` P ) ) e. ZZ )
17 12 15 16 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( A ^ ( phi ` P ) ) e. ZZ )
18 17 zred 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( A ^ ( phi ` P ) ) e. RR )
19 1red 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> 1 e. RR )
20 13 nnrpd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> P e. RR+ )
21 eulerth 
 |-  ( ( P e. NN /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
22 1 21 syl3an1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
23 modmul1 
 |-  ( ( ( ( A ^ ( phi ` P ) ) e. RR /\ 1 e. RR ) /\ ( A e. ZZ /\ P e. RR+ ) /\ ( ( A ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( A ^ ( phi ` P ) ) x. A ) mod P ) = ( ( 1 x. A ) mod P ) )
24 18 19 12 20 22 23 syl221anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( ( A ^ ( phi ` P ) ) x. A ) mod P ) = ( ( 1 x. A ) mod P ) )
25 phiprm 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
26 25 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( phi ` P ) = ( P - 1 ) )
27 26 oveq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( A ^ ( phi ` P ) ) = ( A ^ ( P - 1 ) ) )
28 27 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) x. A ) = ( ( A ^ ( P - 1 ) ) x. A ) )
29 12 zcnd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> A e. CC )
30 expm1t 
 |-  ( ( A e. CC /\ P e. NN ) -> ( A ^ P ) = ( ( A ^ ( P - 1 ) ) x. A ) )
31 29 13 30 syl2anc 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( A ^ P ) = ( ( A ^ ( P - 1 ) ) x. A ) )
32 28 31 eqtr4d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ ( phi ` P ) ) x. A ) = ( A ^ P ) )
33 32 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( ( A ^ ( phi ` P ) ) x. A ) mod P ) = ( ( A ^ P ) mod P ) )
34 29 mulid2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( 1 x. A ) = A )
35 34 oveq1d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( 1 x. A ) mod P ) = ( A mod P ) )
36 24 33 35 3eqtr3d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( A gcd P ) = 1 ) -> ( ( A ^ P ) mod P ) = ( A mod P ) )
37 36 3expia 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A gcd P ) = 1 -> ( ( A ^ P ) mod P ) = ( A mod P ) ) )
38 11 37 sylbid 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A -> ( ( A ^ P ) mod P ) = ( A mod P ) ) )
39 5 38 pm2.61d 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( ( A ^ P ) mod P ) = ( A mod P ) )