Metamath Proof Explorer

Theorem znfermltl

Description: Fermat's little theorem in Z/nZ . (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses znfermltl.z 
|- Z = ( Z/nZ ` P )
znfermltl.b 
|- B = ( Base ` Z )
znfermltl.p 
|- .^ = ( .g ` ( mulGrp ` Z ) )
Assertion znfermltl 
|- ( ( P e. Prime /\ A e. B ) -> ( P .^ A ) = A )

Proof

Step Hyp Ref Expression
1 znfermltl.z 
 |-  Z = ( Z/nZ ` P )
2 znfermltl.b 
 |-  B = ( Base ` Z )
3 znfermltl.p 
 |-  .^ = ( .g ` ( mulGrp ` Z ) )
4 prmnn 
 |-  ( P e. Prime -> P e. NN )
5 4 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
6 5 ad3antrrr 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> P e. NN0 )
7 simplr 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> a e. ZZ )
8 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( ( mulGrp ` CCfld ) |`s ZZ )
9 zsscn 
 |-  ZZ C_ CC
10 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
11 cnfldbas 
 |-  CC = ( Base ` CCfld )
12 10 11 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
13 9 12 sseqtri 
 |-  ZZ C_ ( Base ` ( mulGrp ` CCfld ) )
14 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
15 eqid 
 |-  ( invg ` ( mulGrp ` CCfld ) ) = ( invg ` ( mulGrp ` CCfld ) )
16 cnring 
 |-  CCfld e. Ring
17 10 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
18 16 17 ax-mp 
 |-  ( mulGrp ` CCfld ) e. Mnd
19 cnfld1 
 |-  1 = ( 1r ` CCfld )
20 10 19 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
21 1z 
 |-  1 e. ZZ
22 20 21 eqeltrri 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) e. ZZ
23 eqid 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( mulGrp ` CCfld ) )
24 8 12 23 ress0g 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ ( 0g ` ( mulGrp ` CCfld ) ) e. ZZ /\ ZZ C_ CC ) -> ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) )
25 18 22 9 24 mp3an 
 |-  ( 0g ` ( mulGrp ` CCfld ) ) = ( 0g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
26 8 13 14 15 25 ressmulgnn0 
 |-  ( ( P e. NN0 /\ a e. ZZ ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) = ( P ( .g ` ( mulGrp ` CCfld ) ) a ) )
27 6 7 26 syl2anc 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) = ( P ( .g ` ( mulGrp ` CCfld ) ) a ) )
28 7 zcnd 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> a e. CC )
29 cnfldexp 
 |-  ( ( a e. CC /\ P e. NN0 ) -> ( P ( .g ` ( mulGrp ` CCfld ) ) a ) = ( a ^ P ) )
30 28 6 29 syl2anc 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P ( .g ` ( mulGrp ` CCfld ) ) a ) = ( a ^ P ) )
31 27 30 eqtrd 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) = ( a ^ P ) )
32 31 fveq2d 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( ( ZRHom ` Z ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) ) = ( ( ZRHom ` Z ) ` ( a ^ P ) ) )
33 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
34 1 zncrng 
 |-  ( P e. NN0 -> Z e. CRing )
35 34 crngringd 
 |-  ( P e. NN0 -> Z e. Ring )
36 eqid 
 |-  ( ZRHom ` Z ) = ( ZRHom ` Z )
37 36 zrhrhm 
 |-  ( Z e. Ring -> ( ZRHom ` Z ) e. ( ZZring RingHom Z ) )
38 35 37 syl 
 |-  ( P e. NN0 -> ( ZRHom ` Z ) e. ( ZZring RingHom Z ) )
39 zringmpg 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )
40 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
41 39 40 rhmmhm 
 |-  ( ( ZRHom ` Z ) e. ( ZZring RingHom Z ) -> ( ZRHom ` Z ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Z ) ) )
42 4 33 38 41 4syl 
 |-  ( P e. Prime -> ( ZRHom ` Z ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Z ) ) )
43 42 ad3antrrr 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( ZRHom ` Z ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Z ) ) )
44 8 12 ressbas2 
 |-  ( ZZ C_ CC -> ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) )
45 9 44 ax-mp 
 |-  ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
46 eqid 
 |-  ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) )
47 45 46 3 mhmmulg 
 |-  ( ( ( ZRHom ` Z ) e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom ( mulGrp ` Z ) ) /\ P e. NN0 /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) ) = ( P .^ ( ( ZRHom ` Z ) ` a ) ) )
48 43 6 7 47 syl3anc 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( ( ZRHom ` Z ) ` ( P ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) a ) ) = ( P .^ ( ( ZRHom ` Z ) ` a ) ) )
49 simpr 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> a e. ZZ )
50 4 adantr 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> P e. NN )
51 50 nnnn0d 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> P e. NN0 )
52 zexpcl 
 |-  ( ( a e. ZZ /\ P e. NN0 ) -> ( a ^ P ) e. ZZ )
53 49 51 52 syl2anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( a ^ P ) e. ZZ )
54 eqid 
 |-  ( -g ` ZZring ) = ( -g ` ZZring )
55 54 zringsubgval 
 |-  ( ( ( a ^ P ) e. ZZ /\ a e. ZZ ) -> ( ( a ^ P ) - a ) = ( ( a ^ P ) ( -g ` ZZring ) a ) )
56 53 49 55 syl2anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( a ^ P ) - a ) = ( ( a ^ P ) ( -g ` ZZring ) a ) )
57 56 fveq2d 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( ( a ^ P ) - a ) ) = ( ( ZRHom ` Z ) ` ( ( a ^ P ) ( -g ` ZZring ) a ) ) )
58 53 zred 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( a ^ P ) e. RR )
59 zre 
 |-  ( a e. ZZ -> a e. RR )
60 59 adantl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> a e. RR )
61 50 nnrpd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> P e. RR+ )
62 fermltl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( a ^ P ) mod P ) = ( a mod P ) )
63 eqidd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( a mod P ) = ( a mod P ) )
64 58 60 60 60 61 62 63 modsub12d 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ( a ^ P ) - a ) mod P ) = ( ( a - a ) mod P ) )
65 zcn 
 |-  ( a e. ZZ -> a e. CC )
66 65 subidd 
 |-  ( a e. ZZ -> ( a - a ) = 0 )
67 66 adantl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( a - a ) = 0 )
68 67 oveq1d 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( a - a ) mod P ) = ( 0 mod P ) )
69 0mod 
 |-  ( P e. RR+ -> ( 0 mod P ) = 0 )
70 61 69 syl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( 0 mod P ) = 0 )
71 64 68 70 3eqtrd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ( a ^ P ) - a ) mod P ) = 0 )
72 53 49 zsubcld 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( a ^ P ) - a ) e. ZZ )
73 dvdsval3 
 |-  ( ( P e. NN /\ ( ( a ^ P ) - a ) e. ZZ ) -> ( P || ( ( a ^ P ) - a ) <-> ( ( ( a ^ P ) - a ) mod P ) = 0 ) )
74 50 72 73 syl2anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( P || ( ( a ^ P ) - a ) <-> ( ( ( a ^ P ) - a ) mod P ) = 0 ) )
75 71 74 mpbird 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> P || ( ( a ^ P ) - a ) )
76 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
77 1 36 76 zndvds0 
 |-  ( ( P e. NN0 /\ ( ( a ^ P ) - a ) e. ZZ ) -> ( ( ( ZRHom ` Z ) ` ( ( a ^ P ) - a ) ) = ( 0g ` Z ) <-> P || ( ( a ^ P ) - a ) ) )
78 51 72 77 syl2anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ( ZRHom ` Z ) ` ( ( a ^ P ) - a ) ) = ( 0g ` Z ) <-> P || ( ( a ^ P ) - a ) ) )
79 75 78 mpbird 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( ( a ^ P ) - a ) ) = ( 0g ` Z ) )
80 rhmghm 
 |-  ( ( ZRHom ` Z ) e. ( ZZring RingHom Z ) -> ( ZRHom ` Z ) e. ( ZZring GrpHom Z ) )
81 51 38 80 3syl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ZRHom ` Z ) e. ( ZZring GrpHom Z ) )
82 zringbas 
 |-  ZZ = ( Base ` ZZring )
83 eqid 
 |-  ( -g ` Z ) = ( -g ` Z )
84 82 54 83 ghmsub 
 |-  ( ( ( ZRHom ` Z ) e. ( ZZring GrpHom Z ) /\ ( a ^ P ) e. ZZ /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( ( a ^ P ) ( -g ` ZZring ) a ) ) = ( ( ( ZRHom ` Z ) ` ( a ^ P ) ) ( -g ` Z ) ( ( ZRHom ` Z ) ` a ) ) )
85 81 53 49 84 syl3anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( ( a ^ P ) ( -g ` ZZring ) a ) ) = ( ( ( ZRHom ` Z ) ` ( a ^ P ) ) ( -g ` Z ) ( ( ZRHom ` Z ) ` a ) ) )
86 57 79 85 3eqtr3rd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ( ZRHom ` Z ) ` ( a ^ P ) ) ( -g ` Z ) ( ( ZRHom ` Z ) ` a ) ) = ( 0g ` Z ) )
87 4 33 35 3syl 
 |-  ( P e. Prime -> Z e. Ring )
88 87 ringgrpd 
 |-  ( P e. Prime -> Z e. Grp )
89 88 adantr 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> Z e. Grp )
90 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
91 82 90 rhmf 
 |-  ( ( ZRHom ` Z ) e. ( ZZring RingHom Z ) -> ( ZRHom ` Z ) : ZZ --> ( Base ` Z ) )
92 51 38 91 3syl 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ZRHom ` Z ) : ZZ --> ( Base ` Z ) )
93 92 53 ffvelrnd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( a ^ P ) ) e. ( Base ` Z ) )
94 92 49 ffvelrnd 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` a ) e. ( Base ` Z ) )
95 90 76 83 grpsubeq0 
 |-  ( ( Z e. Grp /\ ( ( ZRHom ` Z ) ` ( a ^ P ) ) e. ( Base ` Z ) /\ ( ( ZRHom ` Z ) ` a ) e. ( Base ` Z ) ) -> ( ( ( ( ZRHom ` Z ) ` ( a ^ P ) ) ( -g ` Z ) ( ( ZRHom ` Z ) ` a ) ) = ( 0g ` Z ) <-> ( ( ZRHom ` Z ) ` ( a ^ P ) ) = ( ( ZRHom ` Z ) ` a ) ) )
96 89 93 94 95 syl3anc 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ( ( ZRHom ` Z ) ` ( a ^ P ) ) ( -g ` Z ) ( ( ZRHom ` Z ) ` a ) ) = ( 0g ` Z ) <-> ( ( ZRHom ` Z ) ` ( a ^ P ) ) = ( ( ZRHom ` Z ) ` a ) ) )
97 86 96 mpbid 
 |-  ( ( P e. Prime /\ a e. ZZ ) -> ( ( ZRHom ` Z ) ` ( a ^ P ) ) = ( ( ZRHom ` Z ) ` a ) )
98 97 ad4ant13 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( ( ZRHom ` Z ) ` ( a ^ P ) ) = ( ( ZRHom ` Z ) ` a ) )
99 32 48 98 3eqtr3d 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P .^ ( ( ZRHom ` Z ) ` a ) ) = ( ( ZRHom ` Z ) ` a ) )
100 oveq2 
 |-  ( A = ( ( ZRHom ` Z ) ` a ) -> ( P .^ A ) = ( P .^ ( ( ZRHom ` Z ) ` a ) ) )
101 100 adantl 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P .^ A ) = ( P .^ ( ( ZRHom ` Z ) ` a ) ) )
102 simpr 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> A = ( ( ZRHom ` Z ) ` a ) )
103 99 101 102 3eqtr4d 
 |-  ( ( ( ( P e. Prime /\ A e. B ) /\ a e. ZZ ) /\ A = ( ( ZRHom ` Z ) ` a ) ) -> ( P .^ A ) = A )
104 1 2 36 znzrhfo 
 |-  ( P e. NN0 -> ( ZRHom ` Z ) : ZZ -onto-> B )
105 4 33 104 3syl 
 |-  ( P e. Prime -> ( ZRHom ` Z ) : ZZ -onto-> B )
106 foelrn 
 |-  ( ( ( ZRHom ` Z ) : ZZ -onto-> B /\ A e. B ) -> E. a e. ZZ A = ( ( ZRHom ` Z ) ` a ) )
107 105 106 sylan 
 |-  ( ( P e. Prime /\ A e. B ) -> E. a e. ZZ A = ( ( ZRHom ` Z ) ` a ) )
108 103 107 r19.29a 
 |-  ( ( P e. Prime /\ A e. B ) -> ( P .^ A ) = A )