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 PAAPmodP=AmodP

Proof

Step Hyp Ref Expression
1 prmnn PP
2 dvdsmodexp PPPAAPmodP=AmodP
3 2 3exp PPPAAPmodP=AmodP
4 1 1 3 sylc PPAAPmodP=AmodP
5 4 adantr PAPAAPmodP=AmodP
6 coprm PA¬PAPgcdA=1
7 prmz PP
8 gcdcom PAPgcdA=AgcdP
9 7 8 sylan PAPgcdA=AgcdP
10 9 eqeq1d PAPgcdA=1AgcdP=1
11 6 10 bitrd PA¬PAAgcdP=1
12 simp2 PAAgcdP=1A
13 1 3ad2ant1 PAAgcdP=1P
14 13 phicld PAAgcdP=1ϕP
15 14 nnnn0d PAAgcdP=1ϕP0
16 zexpcl AϕP0AϕP
17 12 15 16 syl2anc PAAgcdP=1AϕP
18 17 zred PAAgcdP=1AϕP
19 1red PAAgcdP=11
20 13 nnrpd PAAgcdP=1P+
21 eulerth PAAgcdP=1AϕPmodP=1modP
22 1 21 syl3an1 PAAgcdP=1AϕPmodP=1modP
23 modmul1 AϕP1AP+AϕPmodP=1modPAϕPAmodP=1AmodP
24 18 19 12 20 22 23 syl221anc PAAgcdP=1AϕPAmodP=1AmodP
25 phiprm PϕP=P1
26 25 3ad2ant1 PAAgcdP=1ϕP=P1
27 26 oveq2d PAAgcdP=1AϕP=AP1
28 27 oveq1d PAAgcdP=1AϕPA=AP1A
29 12 zcnd PAAgcdP=1A
30 expm1t APAP=AP1A
31 29 13 30 syl2anc PAAgcdP=1AP=AP1A
32 28 31 eqtr4d PAAgcdP=1AϕPA=AP
33 32 oveq1d PAAgcdP=1AϕPAmodP=APmodP
34 29 mulid2d PAAgcdP=11A=A
35 34 oveq1d PAAgcdP=11AmodP=AmodP
36 24 33 35 3eqtr3d PAAgcdP=1APmodP=AmodP
37 36 3expia PAAgcdP=1APmodP=AmodP
38 11 37 sylbid PA¬PAAPmodP=AmodP
39 5 38 pm2.61d PAAPmodP=AmodP