MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgseisenlem4 Unicode version

Theorem lgseisenlem4 20607
Description: Lemma for lgseisen 20608. The function  M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
lgseisen.2  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
lgseisen.3  |-  ( ph  ->  P  =/=  Q )
lgseisen.4  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
lgseisen.5  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
lgseisen.6  |-  S  =  ( ( Q  x.  ( 2  x.  y
) )  mod  P
)
lgseisen.7  |-  Y  =  (ℤ/n `  P )
lgseisen.8  |-  G  =  (mulGrp `  Y )
lgseisen.9  |-  L  =  ( ZRHom `  Y
)
Assertion
Ref Expression
lgseisenlem4  |-  ( ph  ->  ( ( Q ^
( ( P  - 
1 )  /  2
) )  mod  P
)  =  ( (
-u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  mod  P ) )
Distinct variable groups:    x, G    x, L    x, y, P    ph, x, y    y, M   
x, Q, y    x, Y    x, S
Allowed substitution hints:    R( x, y)    S( y)    G( y)    L( y)    M( x)    Y( y)

Proof of Theorem lgseisenlem4
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 zsubrg 16441 . . . . . 6  |-  ZZ  e.  (SubRing ` fld )
2 eqid 2296 . . . . . . 7  |-  (flds  ZZ )  =  (flds  ZZ )
32subrgbas 15570 . . . . . 6  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  =  ( Base `  (flds  ZZ ) ) )
41, 3ax-mp 8 . . . . 5  |-  ZZ  =  ( Base `  (flds  ZZ ) )
5 cnfld0 16414 . . . . . . 7  |-  0  =  ( 0g ` fld )
62, 5subrg0 15568 . . . . . 6  |-  ( ZZ  e.  (SubRing ` fld )  ->  0  =  ( 0g `  (flds  ZZ )
) )
71, 6ax-mp 8 . . . . 5  |-  0  =  ( 0g `  (flds  ZZ ) )
82subrgrng 15564 . . . . . . 7  |-  ( ZZ  e.  (SubRing ` fld )  ->  (flds  ZZ )  e.  Ring )
9 rngabl 15386 . . . . . . 7  |-  ( (flds  ZZ )  e.  Ring  ->  (flds  ZZ )  e.  Abel )
101, 8, 9mp2b 9 . . . . . 6  |-  (flds  ZZ )  e.  Abel
11 ablcmn 15111 . . . . . 6  |-  ( (flds  ZZ )  e.  Abel  ->  (flds  ZZ )  e. CMnd )
1210, 11mp1i 11 . . . . 5  |-  ( ph  ->  (flds  ZZ )  e. CMnd )
13 lgseisen.1 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
14 eldifi 3311 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
1513, 14syl 15 . . . . . . . . 9  |-  ( ph  ->  P  e.  Prime )
16 lgseisen.7 . . . . . . . . . 10  |-  Y  =  (ℤ/n `  P )
1716znfld 16530 . . . . . . . . 9  |-  ( P  e.  Prime  ->  Y  e. Field
)
1815, 17syl 15 . . . . . . . 8  |-  ( ph  ->  Y  e. Field )
19 isfld 15537 . . . . . . . . 9  |-  ( Y  e. Field 
<->  ( Y  e.  DivRing  /\  Y  e.  CRing ) )
2019simprbi 450 . . . . . . . 8  |-  ( Y  e. Field  ->  Y  e.  CRing )
2118, 20syl 15 . . . . . . 7  |-  ( ph  ->  Y  e.  CRing )
22 lgseisen.8 . . . . . . . 8  |-  G  =  (mulGrp `  Y )
2322crngmgp 15365 . . . . . . 7  |-  ( Y  e.  CRing  ->  G  e. CMnd )
2421, 23syl 15 . . . . . 6  |-  ( ph  ->  G  e. CMnd )
25 cmnmnd 15120 . . . . . 6  |-  ( G  e. CMnd  ->  G  e.  Mnd )
2624, 25syl 15 . . . . 5  |-  ( ph  ->  G  e.  Mnd )
27 fzfid 11051 . . . . 5  |-  ( ph  ->  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin )
28 m1expcl 11142 . . . . . . . 8  |-  ( k  e.  ZZ  ->  ( -u 1 ^ k )  e.  ZZ )
2928adantl 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( -u
1 ^ k )  e.  ZZ )
30 eqidd 2297 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  =  ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) )
31 crngrng 15367 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
3221, 31syl 15 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  Ring )
33 lgseisen.9 . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Y
)
342, 33zrhrhm 16482 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
3532, 34syl 15 . . . . . . . . 9  |-  ( ph  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
36 eqid 2296 . . . . . . . . . 10  |-  ( Base `  Y )  =  (
Base `  Y )
374, 36rhmf 15520 . . . . . . . . 9  |-  ( L  e.  ( (flds  ZZ ) RingHom  Y )  ->  L : ZZ --> ( Base `  Y )
)
3835, 37syl 15 . . . . . . . 8  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
3938feqmptd 5591 . . . . . . 7  |-  ( ph  ->  L  =  ( x  e.  ZZ  |->  ( L `
 x ) ) )
40 fveq2 5541 . . . . . . 7  |-  ( x  =  ( -u 1 ^ k )  -> 
( L `  x
)  =  ( L `
 ( -u 1 ^ k ) ) )
4129, 30, 39, 40fmptco 5707 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  =  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) ) )
42 cnrng 16412 . . . . . . . . . 10  |-fld  e.  Ring
43 eqid 2296 . . . . . . . . . . 11  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
442, 43mgpress 15352 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  ZZ  e.  (SubRing ` fld ) )  ->  (
(mulGrp ` fld )s  ZZ )  =  (mulGrp `  (flds  ZZ ) ) )
4542, 1, 44mp2an 653 . . . . . . . . 9  |-  ( (mulGrp ` fld )s  ZZ )  =  (mulGrp `  (flds  ZZ ) )
4645, 22rhmmhm 15518 . . . . . . . 8  |-  ( L  e.  ( (flds  ZZ ) RingHom  Y )  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
4735, 46syl 15 . . . . . . 7  |-  ( ph  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
48 neg1cn 9829 . . . . . . . . . . 11  |-  -u 1  e.  CC
49 ax-1cn 8811 . . . . . . . . . . . 12  |-  1  e.  CC
50 ax-1ne0 8822 . . . . . . . . . . . 12  |-  1  =/=  0
5149, 50negne0i 9137 . . . . . . . . . . 11  |-  -u 1  =/=  0
52 eqid 2296 . . . . . . . . . . . 12  |-  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )  =  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
532, 43, 52expghm 16466 . . . . . . . . . . 11  |-  ( (
-u 1  e.  CC  /\  -u 1  =/=  0
)  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ )  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) )
5448, 51, 53mp2an 653 . . . . . . . . . 10  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) 
GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
55 ghmmhm 14709 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) )  e.  ( (flds  ZZ )  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )  -> 
( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) )
5654, 55ax-mp 8 . . . . . . . . 9  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) MndHom 
( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
57 cnfldbas 16399 . . . . . . . . . . . 12  |-  CC  =  ( Base ` fld )
58 cndrng 16419 . . . . . . . . . . . 12  |-fld  e.  DivRing
5957, 5, 58drngui 15534 . . . . . . . . . . 11  |-  ( CC 
\  { 0 } )  =  (Unit ` fld )
6059, 43unitsubm 15468 . . . . . . . . . 10  |-  (fld  e.  Ring  -> 
( CC  \  {
0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )
6142, 60ax-mp 8 . . . . . . . . 9  |-  ( CC 
\  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) )
6252resmhm2 14453 . . . . . . . . 9  |-  ( ( ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )  /\  ( CC  \  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )  -> 
( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  ( (flds  ZZ ) MndHom  (mulGrp ` fld ) ) )
6356, 61, 62mp2an 653 . . . . . . . 8  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) MndHom 
(mulGrp ` fld ) )
6443subrgsubm 15574 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
651, 64ax-mp 8 . . . . . . . . 9  |-  ZZ  e.  (SubMnd `  (mulGrp ` fld ) )
66 eqid 2296 . . . . . . . . . . 11  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  =  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )
6729, 66fmptd 5700 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) : ZZ --> ZZ )
68 frn 5411 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) : ZZ --> ZZ  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
6967, 68syl 15 . . . . . . . . 9  |-  ( ph  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
70 eqid 2296 . . . . . . . . . 10  |-  ( (mulGrp ` fld )s  ZZ )  =  (
(mulGrp ` fld )s  ZZ )
7170resmhm2b 14454 . . . . . . . . 9  |-  ( ( ZZ  e.  (SubMnd `  (mulGrp ` fld ) )  /\  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  C_  ZZ )  ->  ( ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) MndHom 
(mulGrp ` fld ) )  <->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ZZ ) ) ) )
7265, 69, 71sylancr 644 . . . . . . . 8  |-  ( ph  ->  ( ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ ) MndHom  (mulGrp ` fld )
)  <->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ZZ ) ) ) )
7363, 72mpbii 202 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ZZ ) ) )
74 mhmco 14455 . . . . . . 7  |-  ( ( L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G )  /\  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ZZ ) ) )  -> 
( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  ( (flds  ZZ ) MndHom  G ) )
7547, 73, 74syl2anc 642 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  ( (flds  ZZ ) MndHom  G ) )
7641, 75eqeltrrd 2371 . . . . 5  |-  ( ph  ->  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) )  e.  ( (flds  ZZ ) MndHom  G ) )
77 lgseisen.2 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
78 eldifi 3311 . . . . . . . . . . . 12  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
7977, 78syl 15 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  Prime )
80 prmnn 12777 . . . . . . . . . . 11  |-  ( Q  e.  Prime  ->  Q  e.  NN )
8179, 80syl 15 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  NN )
8281nnred 9777 . . . . . . . . 9  |-  ( ph  ->  Q  e.  RR )
83 prmnn 12777 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
8415, 83syl 15 . . . . . . . . 9  |-  ( ph  ->  P  e.  NN )
8582, 84nndivred 9810 . . . . . . . 8  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
8685adantr 451 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  /  P )  e.  RR )
87 2nn 9893 . . . . . . . . 9  |-  2  e.  NN
88 elfznn 10835 . . . . . . . . . 10  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
8988adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
90 nnmulcl 9785 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
9187, 89, 90sylancr 644 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
9291nnred 9777 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  RR )
9386, 92remulcld 8879 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  /  P
)  x.  ( 2  x.  x ) )  e.  RR )
9493flcld 10946 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ )
95 eqid 2296 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  =  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )
9695mptpreima 5182 . . . . . . 7  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) " ( _V  \  { 0 } ) )  =  {
x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) )  e.  ( _V 
\  { 0 } ) }
97 ssrab2 3271 . . . . . . 7  |-  { x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ( _V  \  {
0 } ) } 
C_  ( 1 ... ( ( P  - 
1 )  /  2
) )
9896, 97eqsstri 3221 . . . . . 6  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) " ( _V  \  { 0 } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
99 ssfi 7099 . . . . . 6  |-  ( ( ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin  /\  ( `' ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) "
( _V  \  {
0 } ) ) 
C_  ( 1 ... ( ( P  - 
1 )  /  2
) ) )  -> 
( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )
" ( _V  \  { 0 } ) )  e.  Fin )
10027, 98, 99sylancl 643 . . . . 5  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )
" ( _V  \  { 0 } ) )  e.  Fin )
101 oveq2 5882 . . . . . 6  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
102101fveq2d 5545 . . . . 5  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
103 oveq2 5882 . . . . . 6  |-  ( k  =  ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) )  -> 
( -u 1 ^ k
)  =  ( -u
1 ^ ( (flds  ZZ ) 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) ) ) )
104103fveq2d 5545 . . . . 5  |-  ( k  =  ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) )  -> 
( L `  ( -u 1 ^ k ) )  =  ( L `
 ( -u 1 ^ ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) ) ) )
1054, 7, 12, 26, 27, 76, 94, 100, 102, 104gsummhm2 15228 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  =  ( L `  ( -u 1 ^ ( (flds  ZZ ) 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) ) ) ) )
10622, 36mgpbas 15347 . . . . . . 7  |-  ( Base `  Y )  =  (
Base `  G )
107 eqid 2296 . . . . . . 7  |-  ( 0g
`  G )  =  ( 0g `  G
)
108 eqid 2296 . . . . . . . 8  |-  ( .r
`  Y )  =  ( .r `  Y
)
10922, 108mgpplusg 15345 . . . . . . 7  |-  ( .r
`  Y )  =  ( +g  `  G
)
11038adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
111 m1expcl 11142 . . . . . . . . . 10  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
11294, 111syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
113 ffvelrn 5679 . . . . . . . . 9  |-  ( ( L : ZZ --> ( Base `  Y )  /\  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )  -> 
( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )  e.  ( Base `  Y ) )
114110, 112, 113syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( Base `  Y
) )
115 eqid 2296 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) )  =  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) )
116114, 115fmptd 5700 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ( Base `  Y
) )
117 1z 10069 . . . . . . . . . . . 12  |-  1  e.  ZZ
118 znegcl 10071 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  -u 1  e.  ZZ )
119117, 118ax-mp 8 . . . . . . . . . . 11  |-  -u 1  e.  ZZ
120 lgseisen.4 . . . . . . . . . . . 12  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
12179adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
122 prmz 12778 . . . . . . . . . . . . . . 15  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
123121, 122syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
12491nnzd 10132 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
125123, 124zmulcld 10139 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
12615adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
127126, 83syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
128125, 127zmodcld 11006 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  NN0 )
129120, 128syl5eqel 2380 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
130 zexpcl 11134 . . . . . . . . . . 11  |-  ( (
-u 1  e.  ZZ  /\  R  e.  NN0 )  ->  ( -u 1 ^ R )  e.  ZZ )
131119, 129, 130sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
132131, 123zmulcld 10139 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )
133 ffvelrn 5679 . . . . . . . . 9  |-  ( ( L : ZZ --> ( Base `  Y )  /\  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )  -> 
( L `  (
( -u 1 ^ R
)  x.  Q ) )  e.  ( Base `  Y ) )
134110, 132, 133syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ R )  x.  Q ) )  e.  ( Base `  Y
) )
135 eqid 2296 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) )
136134, 135fmptd 5700 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ( Base `  Y
) )
137115mptpreima 5182 . . . . . . . . 9  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  =  {
x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )  e.  ( _V 
\  { ( 0g
`  G ) } ) }
138 ssrab2 3271 . . . . . . . . 9  |-  { x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( _V  \  { ( 0g `  G ) } ) }  C_  ( 1 ... ( ( P  -  1 )  / 
2 ) )
139137, 138eqsstri 3221 . . . . . . . 8  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
140 ssfi 7099 . . . . . . . 8  |-  ( ( ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin  /\  ( `' ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) ) )  ->  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  e.  Fin )
14127, 139, 140sylancl 643 . . . . . . 7  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) " ( _V 
\  { ( 0g
`  G ) } ) )  e.  Fin )
142135mptpreima 5182 . . . . . . . . 9  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  =  {
x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |  ( L `  (
( -u 1 ^ R
)  x.  Q ) )  e.  ( _V 
\  { ( 0g
`  G ) } ) }
143 ssrab2 3271 . . . . . . . . 9  |-  { x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |  ( L `
 ( ( -u
1 ^ R )  x.  Q ) )  e.  ( _V  \  { ( 0g `  G ) } ) }  C_  ( 1 ... ( ( P  -  1 )  / 
2 ) )
144142, 143eqsstri 3221 . . . . . . . 8  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
145 ssfi 7099 . . . . . . . 8  |-  ( ( ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin  /\  ( `' ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) "
( _V  \  {
( 0g `  G
) } ) ) 
C_  ( 1 ... ( ( P  - 
1 )  /  2
) ) )  -> 
( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) " ( _V 
\  { ( 0g
`  G ) } ) )  e.  Fin )
14627, 144, 145sylancl 643 . . . . . . 7  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) " ( _V 
\  { ( 0g
`  G ) } ) )  e.  Fin )
147106, 107, 109, 24, 27, 116, 136, 141, 146gsumadd 15221 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  o F ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) ) )  =  ( ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) ) ( .r `  Y ) ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) ) ) )
148 eqidd 2297 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  =  ( x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )
149 eqidd 2297 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) )  =  ( x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  ( (
-u 1 ^ R
)  x.  Q ) ) ) )
15027, 114, 134, 148, 149offval2 6111 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  o F ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) )  =  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ( .r `  Y
) ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) ) )
15135adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
152 cnfldmul 16401 . . . . . . . . . . . . . 14  |-  x.  =  ( .r ` fld )
1532, 152ressmulr 13277 . . . . . . . . . . . . 13  |-  ( ZZ  e.  (SubRing ` fld )  ->  x.  =  ( .r `  (flds  ZZ ) ) )
1541, 153ax-mp 8 . . . . . . . . . . . 12  |-  x.  =  ( .r `  (flds  ZZ ) )
1554, 154, 108rhmmul 15521 . . . . . . . . . . 11  |-  ( ( L  e.  ( (flds  ZZ ) RingHom  Y )  /\  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ  /\  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )  -> 
( L `  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ( .r `  Y ) ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) )
156151, 112, 132, 155syl3anc 1182 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ( .r `  Y ) ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) )
157125zred 10133 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
158127nnrpd 10405 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
159 modval 10991 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( Q  x.  (
2  x.  x ) )  e.  RR  /\  P  e.  RR+ )  -> 
( ( Q  x.  ( 2  x.  x
) )  mod  P
)  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
160157, 158, 159syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
161120, 160syl5eq 2340 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
162123zcnd 10134 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  CC )
16391nncnd 9778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  CC )
164127nncnd 9778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
165127nnne0d 9806 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  0 )
166162, 163, 164, 165div23d 9589 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )
167166fveq2d 5545 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) )  =  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )
168167oveq2d 5890 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x
) )  /  P
) ) )  =  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )
169168oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x
) )  /  P
) ) ) )  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
170161, 169eqtrd 2328 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
171170oveq2d 5890 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  +  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) ) ) )
172 prmz 12778 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
173126, 172syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
174173, 94zmulcld 10139 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )
175174zcnd 10134 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  CC )
176125zcnd 10134 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  CC )
177175, 176pncan3d 9176 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  =  ( Q  x.  ( 2  x.  x ) ) )
178 2cn 9832 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
179178a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  CC )
18089nncnd 9778 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  CC )
181162, 179, 180mul12d 9037 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  =  ( 2  x.  ( Q  x.  x
) ) )
182171, 177, 1813eqtrd 2332 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( 2  x.  ( Q  x.  x )
) )
183182oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( ( P  x.  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R ) )  =  ( -u 1 ^ ( 2  x.  ( Q  x.  x
) ) ) )
18448a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  e.  CC )
18551a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  =/=  0 )
186129nn0zd 10131 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
187 expaddz 11162 . . . . . . . . . . . . . . . 16  |-  ( ( ( -u 1  e.  CC  /\  -u 1  =/=  0 )  /\  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ  /\  R  e.  ZZ ) )  -> 
( -u 1 ^ (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R ) )  =  ( ( -u
1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  x.  ( -u 1 ^ R ) ) )
188184, 185, 174, 186, 187syl22anc 1183 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( ( P  x.  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R ) )  =  ( ( -u
1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  x.  ( -u 1 ^ R ) ) )
189 expmulz 11164 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u 1  e.  CC  /\  -u 1  =/=  0 )  /\  ( P  e.  ZZ  /\  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ ) )  -> 
( -u 1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  =  ( ( -u
1 ^ P ) ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
190184, 185, 173, 94, 189syl22anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  =  ( ( -u
1 ^ P ) ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
19149a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  CC )
192 eldifsni 3763 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
19313, 192syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  2 )
194193necomd 2542 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  =/=  P )
195194neneqd 2475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  2  =  P )
196195adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  =  P )
197 2z 10070 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  ZZ
198 uzid 10258 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
199197, 198ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ( ZZ>= `  2 )
200 dvdsprm 12794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
201199, 126, 200sylancr 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  P  <->  2  =  P ) )
202196, 201mtbird 292 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  ||  P )
203 oexpneg 12606 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  NN  /\  -.  2  ||  P )  -> 
( -u 1 ^ P
)  =  -u (
1 ^ P ) )
204191, 127, 202, 203syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u ( 1 ^ P ) )
205 1exp 11147 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
1 ^ P )  =  1 )
206173, 205syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ P )  =  1 )
207206negeqd 9062 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u (
1 ^ P )  =  -u 1 )
208204, 207eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u 1 )
209208oveq1d 5889 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ P
) ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
210190, 209eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
211210oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  x.  ( -u 1 ^ R ) )  =  ( ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  x.  ( -u 1 ^ R ) ) )
212188, 211eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( ( P  x.  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R ) )  =  ( ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) ) )
213 nnmulcl 9785 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  e.  NN  /\  x  e.  NN )  ->  ( Q  x.  x
)  e.  NN )
21481, 88, 213syl2an 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN )
215214nnnn0d 10034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN0 )
216 2nn0 9998 . . . . . . . . . . . . . . . . 17  |-  2  e.  NN0
217216a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
218184, 215, 217expmuld 11264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( Q  x.  x ) ) )
219 sqneg 11180 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
22049, 219ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
221 sq1 11214 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ^ 2 )  =  1
222220, 221eqtri 2316 . . . . . . . . . . . . . . . . 17  |-  ( -u
1 ^ 2 )  =  1
223222oveq1i 5884 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  ( 1 ^ ( Q  x.  x
) )
224214nnzd 10132 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  ZZ )
225 1exp 11147 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  x.  x )  e.  ZZ  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
226224, 225syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
227223, 226syl5eq 2340 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  1 )
228218, 227eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  1 )
229183, 212, 2283eqtr3d 2336 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) )  =  1 )
230229oveq1d 5889 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  x.  ( -u 1 ^ R ) )  x.  Q )  =  ( 1  x.  Q ) )
231112zcnd 10134 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  CC )
232131zcnd 10134 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
233231, 232, 162mulassd 8874 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  x.  ( -u 1 ^ R ) )  x.  Q )  =  ( ( -u 1 ^ ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )  x.  (
( -u 1 ^ R
)  x.  Q ) ) )
234162mulid2d 8869 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  Q )  =  Q )
235230, 233, 2343eqtr3d 2336 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) )  =  Q )
236235fveq2d 5545 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( L `
 Q ) )
237156, 236eqtr3d 2330 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ( .r `  Y ) ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( L `
 Q ) )
238237mpteq2dva 4122 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ( .r `  Y ) ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) )  =  ( x  e.  ( 1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  Q ) ) )
239150, 238eqtrd 2328 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  o F ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) )  =  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  Q ) ) )
240239oveq2d 5890 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  o F ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) ) )  =  ( G 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  Q ) ) ) )
241 lgseisen.3 . . . . . . . 8  |-  ( ph  ->  P  =/=  Q )
242 lgseisen.5 . . . . . . . 8  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
243 lgseisen.6 . . . . . . . 8  |-  S  =  ( ( Q  x.  ( 2  x.  y
) )  mod  P
)
24413, 77, 241, 120, 242, 243, 16, 22, 33lgseisenlem3 20606 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) )  =  ( 1r `  Y
) )
245244oveq2d 5890 . . . . . 6  |-  ( ph  ->  ( ( G  gsumg  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) ) ( .r
`  Y ) ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) ) )  =  ( ( G 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) ) ( .r `  Y ) ( 1r `  Y
) ) )
246147, 240, 2453eqtr3rd 2337 . . . . 5  |-  ( ph  ->  ( ( G  gsumg  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) ) ( .r
`  Y ) ( 1r `  Y ) )  =  ( G 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  Q ) ) ) )
247106, 107, 24, 27, 116, 141gsumcl 15214 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )
248 eqid 2296 . . . . . . 7  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
24936, 108, 248rngridm 15381 . . . . . 6  |-  ( ( Y  e.  Ring  /\  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )  ->  (
( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) ) ( .r `  Y ) ( 1r `  Y
) )  =  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) ) )
25032, 247, 249syl2anc 642 . . . . 5  |-  ( ph  ->  ( ( G  gsumg  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) ) ( .r
`  Y ) ( 1r `  Y ) )  =  ( G 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  ( -u
1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) ) )
25179, 122syl 15 . . . . . . . 8  |-  ( ph  ->  Q  e.  ZZ )
252 ffvelrn 5679 . . . . . . . 8  |-  ( ( L : ZZ --> ( Base `  Y )  /\  Q  e.  ZZ )  ->  ( L `  Q )  e.  ( Base `  Y
) )
25338, 251, 252syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( L `  Q
)  e.  ( Base `  Y ) )
254 eqid 2296 . . . . . . . 8  |-  (.g `  G
)  =  (.g `  G
)
255106, 254gsumconst 15225 . . . . . . 7  |-  ( ( G  e.  Mnd  /\  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin  /\  ( L `  Q )  e.  ( Base `  Y
) )  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
25626, 27, 253, 255syl3anc 1182 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
257 oddprm 12884 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
25813, 257syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
259258nnnn0d 10034 . . . . . . . 8  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
260 hashfz1 11361 . . . . . . . 8  |-  ( ( ( P  -  1 )  /  2 )  e.  NN0  ->  ( # `  ( 1 ... (
( P  -  1 )  /  2 ) ) )  =  ( ( P  -  1 )  /  2 ) )
261259, 260syl 15 . . . . . . 7  |-  ( ph  ->  ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) )  =  ( ( P  -  1 )  / 
2 ) )
262261oveq1d 5889 . . . . . 6  |-  ( ph  ->  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
26345, 4mgpbas 15347 . . . . . . . . 9  |-  ZZ  =  ( Base `  ( (mulGrp ` fld )s  ZZ ) )
264 eqid 2296 . . . . . . . . 9  |-  (.g `  (
(mulGrp ` fld )s  ZZ ) )  =  (.g `  ( (mulGrp ` fld )s  ZZ ) )
265263, 264, 254mhmmulg 14615 . . . . . . . 8  |-  ( ( L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G )  /\  ( ( P  -  1 )  / 
2 )  e.  NN0  /\  Q  e.  ZZ )  ->  ( L `  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( ( ( P  - 
1 )  /  2
) (.g `  G ) ( L `  Q ) ) )
26647, 259, 251, 265syl3anc 1182 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
26765a1i 10 . . . . . . . . . 10  |-  ( ph  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
268 eqid 2296 . . . . . . . . . . 11  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
269268, 70, 264submmulg 14618 . . . . . . . . . 10  |-  ( ( ZZ  e.  (SubMnd `  (mulGrp ` fld ) )  /\  (
( P  -  1 )  /  2 )  e.  NN0  /\  Q  e.  ZZ )  ->  (
( ( P  - 
1 )  /  2
) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  /  2 ) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )
270267, 259, 251, 269syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )
271251zcnd 10134 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
272 cnfldexp 16423 . . . . . . . . . 10  |-  ( ( Q  e.  CC  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
273271, 259, 272syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
274270, 273eqtr3d 2330 . . . . . . . 8  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q )  =  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )
275274fveq2d 5545 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( L `
 ( Q ^
( ( P  - 
1 )  /  2
) ) ) )
276266, 275eqtr3d 2330 . . . . . 6  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  G
) ( L `  Q ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
277256, 262, 2763eqtrd 2332 . . . . 5  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
278246, 250, 2773eqtr3d 2336 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
279 subrgsubg 15567 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
2801, 279ax-mp 8 . . . . . . . . 9  |-  ZZ  e.  (SubGrp ` fld )
281 subgsubm 14655 . . . . . . . . 9  |-  ( ZZ  e.  (SubGrp ` fld )  ->  ZZ  e.  (SubMnd ` fld ) )
282280, 281mp1i 11 . . . . . . . 8  |-  ( ph  ->  ZZ  e.  (SubMnd ` fld )
)
28394, 95fmptd 5700 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ZZ )
28427, 282, 283, 2gsumsubm 14471 . . . . . . 7  |-  ( ph  ->  (fld 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) )  =  ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) )
28594zcnd 10134 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  CC )
28627, 285gsumfsum 16455 . . . . . . 7  |-  ( ph  ->  (fld 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) )  =  sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )
287284, 286eqtr3d 2330 . . . . . 6  |-  ( ph  ->  ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) )  = 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )
288287oveq2d 5890 . . . . 5  |-  ( ph  ->  ( -u 1 ^ ( (flds  ZZ )  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) )  =  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) )
289288fveq2d 5545 . . . 4  |-  ( ph  ->  ( L `  ( -u 1 ^ ( (flds  ZZ ) 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
290105, 278, 2893eqtr3d 2336 . . 3  |-  ( ph  ->  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
29184nnnn0d 10034 . . . 4  |-  ( ph  ->  P  e.  NN0 )
292 zexpcl 11134 . . . . 5  |-  ( ( Q  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
293251, 259, 292syl2anc 642 . . . 4  |-  ( ph  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
29427, 94fsumzcl 12224 . . . . 5  |-  ( ph  -> 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ )
295 m1expcl 11142 . . . . 5  |-  ( sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ  ->  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )  e.  ZZ )
296294, 295syl 15 . . . 4  |-  ( ph  ->  ( -u 1 ^
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  e.  ZZ )
29716, 33zndvds 16519 . . . 4  |-  ( ( P  e.  NN0  /\  ( Q ^ ( ( P  -  1 )  /  2 ) )  e.  ZZ  /\  ( -u 1 ^ sum_ x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )  ->  (
( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )  <->  P  ||  ( ( Q ^ ( ( P  -  1 )  /  2 ) )  -  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) ) )
298291, 293, 296, 297syl3anc 1182 . . 3  |-  ( ph  ->  ( ( L `  ( Q ^ ( ( P  -  1 )  /  2 ) ) )  =  ( L `
 ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) )  <->  P  ||  (
( Q ^ (
( P  -  1 )  /  2 ) )  -  ( -u
1 ^ sum_ x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) )
299290, 298mpbid 201 . 2  |-  ( ph  ->  P  ||  ( ( Q ^ ( ( P  -  1 )  /  2 ) )  -  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) )
300 moddvds 12554 . . 3  |-  ( ( P  e.  NN  /\  ( Q ^ ( ( P  -  1 )  /  2 ) )  e.  ZZ  /\  ( -u 1 ^ sum_ x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )  ->  (
( ( Q ^
( ( P  - 
1 )  /  2
) )  mod  P
)  =  ( (
-u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  mod  P )  <->  P  ||  (
( Q ^ (
( P  -  1 )  /  2 ) )  -  ( -u
1 ^ sum_ x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) )
30184, 293, 296, 300syl3anc 1182 . 2  |-  ( ph  ->  ( ( ( Q ^ ( ( P  -  1 )  / 
2 ) )  mod 
P )  =  ( ( -u 1 ^
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  mod  P )  <-> 
P  ||  ( ( Q ^ ( ( P  -  1 )  / 
2 ) )  -  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )
302299, 301mpbird 223 1  |-  ( ph  ->  ( ( Q ^
( ( P  - 
1 )  /  2
) )  mod  P
)  =  ( (
-u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  mod  P ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   {crab 2560   _Vcvv 2801    \ cdif 3162    C_ wss 3165   {csn 3653   class class class wbr 4039    e. cmpt 4093   `'ccnv 4704   ran crn 4706   "cima 4708    o. ccom 4709   -->wf 5267   ` cfv 5271  (class class class)co 5874    o Fcof 6092   Fincfn 6879   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    - cmin 9053   -ucneg 9054    / cdiv 9439   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   RR+crp 10370   ...cfz 10798   |_cfl 10940    mod cmo 10989   ^cexp 11120   #chash 11353   sum_csu 12174    || cdivides 12547   Primecprime 12774   Basecbs 13164   ↾s cress 13165   .rcmulr 13225   0gc0g 13416    gsumg cgsu 13417   Mndcmnd 14377  .gcmg 14382   MndHom cmhm 14429  SubMndcsubmnd 14430  SubGrpcsubg 14631    GrpHom cghm 14696  CMndccmn 15105   Abelcabel 15106  mulGrpcmgp 15341   Ringcrg 15353   CRingccrg 15354   1rcur 15355   RingHom crh 15510   DivRingcdr 15528  Fieldcfield 15529  SubRingcsubrg 15557  ℂfldccnfld 16393   ZRHomczrh 16467  ℤ/nczn 16470
This theorem is referenced by:  lgseisen  20608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831  ax-addf 8832  ax-mulf 8833
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-1st 6138  df-2nd 6139  df-tpos 6250  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-er 6676  df-ec 6678  df-qs 6682  df-map 6790  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-sup 7210  df-oi 7241  df-card 7588  df-cda 7810  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-10 9828  df-n0 9982  df-z 10041  df-dec 10141  df-uz 10247  df-rp 10371  df-fz 10799  df-fzo 10887  df-fl 10941  df-mod 10990  df-seq 11063  df-exp 11121  df-hash 11354  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-clim 11978  df-sum 12175  df-dvds 12548  df-gcd 12702  df-prm 12775  df-struct 13166  df-ndx 13167  df-slot 13168  df-base 13169  df-sets 13170  df-ress 13171  df-plusg 13237  df-mulr 13238  df-starv 13239  df-sca 13240  df-vsca 13241  df-tset 13243  df-ple 13244  df-ds 13246  df-0g 13420  df-gsum 13421  df-imas 13427  df-divs 13428  df-mnd 14383  df-mhm 14431  df-submnd 14432  df-grp 14505  df-minusg 14506  df-sbg 14507  df-mulg 14508  df-subg 14634  df-nsg 14635  df-eqg 14636  df-ghm 14697  df-cntz 14809  df-cmn 15107  df-abl 15108  df-mgp 15342  df-rng 15356  df-cring 15357  df-ur 15358  df-oppr 15421  df-dvdsr 15439  df-unit 15440  df-invr 15470  df-dvr 15481  df-rnghom 15512  df-drng 15530  df-field 15531  df-subrg 15559  df-lmod 15645  df-lss 15706  df-lsp 15745  df-sra 15941  df-rgmod 15942  df-lidl 15943  df-rsp 15944  df-2idl 16000  df-nzr 16026  df-rlreg 16040  df-domn 16041  df-idom 16042  df-cnfld 16394  df-zrh 16471  df-zn 16474
  Copyright terms: Public domain W3C validator