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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmnn | |
|
2 | dvdsmodexp | |
|
3 | 2 | 3exp | |
4 | 1 1 3 | sylc | |
5 | 4 | adantr | |
6 | coprm | |
|
7 | prmz | |
|
8 | gcdcom | |
|
9 | 7 8 | sylan | |
10 | 9 | eqeq1d | |
11 | 6 10 | bitrd | |
12 | simp2 | |
|
13 | 1 | 3ad2ant1 | |
14 | 13 | phicld | |
15 | 14 | nnnn0d | |
16 | zexpcl | |
|
17 | 12 15 16 | syl2anc | |
18 | 17 | zred | |
19 | 1red | |
|
20 | 13 | nnrpd | |
21 | eulerth | |
|
22 | 1 21 | syl3an1 | |
23 | modmul1 | |
|
24 | 18 19 12 20 22 23 | syl221anc | |
25 | phiprm | |
|
26 | 25 | 3ad2ant1 | |
27 | 26 | oveq2d | |
28 | 27 | oveq1d | |
29 | 12 | zcnd | |
30 | expm1t | |
|
31 | 29 13 30 | syl2anc | |
32 | 28 31 | eqtr4d | |
33 | 32 | oveq1d | |
34 | 29 | mulid2d | |
35 | 34 | oveq1d | |
36 | 24 33 35 | 3eqtr3d | |
37 | 36 | 3expia | |
38 | 11 37 | sylbid | |
39 | 5 38 | pm2.61d | |