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

Metamath Proof Explorer

Theorem ply1fermltl

Description: Fermat's little theorem for polynomials. If P is prime, Then ( X + A ) ^ P = ( ( X ^ P ) + A ) modulo P . (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses ply1fermltl.z 
|- Z = ( Z/nZ ` P )
ply1fermltl.w 
|- W = ( Poly1 ` Z )
ply1fermltl.x 
|- X = ( var1 ` Z )
ply1fermltl.l 
|- .+ = ( +g ` W )
ply1fermltl.n 
|- N = ( mulGrp ` W )
ply1fermltl.t 
|- .^ = ( .g ` N )
ply1fermltl.c 
|- C = ( algSc ` W )
ply1fermltl.a 
|- A = ( C ` ( ( ZRHom ` Z ) ` E ) )
ply1fermltl.p 
|- ( ph -> P e. Prime )
ply1fermltl.1 
|- ( ph -> E e. ZZ )
Assertion ply1fermltl 
|- ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )

Proof

Step Hyp Ref Expression
1 ply1fermltl.z 
 |-  Z = ( Z/nZ ` P )
2 ply1fermltl.w 
 |-  W = ( Poly1 ` Z )
3 ply1fermltl.x 
 |-  X = ( var1 ` Z )
4 ply1fermltl.l 
 |-  .+ = ( +g ` W )
5 ply1fermltl.n 
 |-  N = ( mulGrp ` W )
6 ply1fermltl.t 
 |-  .^ = ( .g ` N )
7 ply1fermltl.c 
 |-  C = ( algSc ` W )
8 ply1fermltl.a 
 |-  A = ( C ` ( ( ZRHom ` Z ) ` E ) )
9 ply1fermltl.p 
 |-  ( ph -> P e. Prime )
10 ply1fermltl.1 
 |-  ( ph -> E e. ZZ )
11 eqid 
 |-  ( chr ` Z ) = ( chr ` Z )
12 prmnn 
 |-  ( P e. Prime -> P e. NN )
13 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
14 1 zncrng 
 |-  ( P e. NN0 -> Z e. CRing )
15 9 12 13 14 4syl 
 |-  ( ph -> Z e. CRing )
16 1 znchr 
 |-  ( P e. NN0 -> ( chr ` Z ) = P )
17 9 12 13 16 4syl 
 |-  ( ph -> ( chr ` Z ) = P )
18 17 9 eqeltrd 
 |-  ( ph -> ( chr ` Z ) e. Prime )
19 2 3 4 5 6 7 8 11 15 18 10 ply1fermltlchr 
 |-  ( ph -> ( ( chr ` Z ) .^ ( X .+ A ) ) = ( ( ( chr ` Z ) .^ X ) .+ A ) )
20 17 oveq1d 
 |-  ( ph -> ( ( chr ` Z ) .^ ( X .+ A ) ) = ( P .^ ( X .+ A ) ) )
21 17 oveq1d 
 |-  ( ph -> ( ( chr ` Z ) .^ X ) = ( P .^ X ) )
22 21 oveq1d 
 |-  ( ph -> ( ( ( chr ` Z ) .^ X ) .+ A ) = ( ( P .^ X ) .+ A ) )
23 19 20 22 3eqtr3d 
 |-  ( ph -> ( P .^ ( X .+ A ) ) = ( ( P .^ X ) .+ A ) )