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

Theorem lgseisenlem4 21128
Description: Lemma for lgseisen 21129. 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 16744 . . . . . 6  |-  ZZ  e.  (SubRing ` fld )
2 eqid 2435 . . . . . . 7  |-  (flds  ZZ )  =  (flds  ZZ )
32subrgbas 15869 . . . . . 6  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  =  ( Base `  (flds  ZZ ) ) )
41, 3ax-mp 8 . . . . 5  |-  ZZ  =  ( Base `  (flds  ZZ ) )
5 cnfld0 16717 . . . . . . 7  |-  0  =  ( 0g ` fld )
62, 5subrg0 15867 . . . . . 6  |-  ( ZZ  e.  (SubRing ` fld )  ->  0  =  ( 0g `  (flds  ZZ )
) )
71, 6ax-mp 8 . . . . 5  |-  0  =  ( 0g `  (flds  ZZ ) )
82subrgrng 15863 . . . . . . 7  |-  ( ZZ  e.  (SubRing ` fld )  ->  (flds  ZZ )  e.  Ring )
9 rngabl 15685 . . . . . . 7  |-  ( (flds  ZZ )  e.  Ring  ->  (flds  ZZ )  e.  Abel )
101, 8, 9mp2b 10 . . . . . 6  |-  (flds  ZZ )  e.  Abel
11 ablcmn 15410 . . . . . 6  |-  ( (flds  ZZ )  e.  Abel  ->  (flds  ZZ )  e. CMnd )
1210, 11mp1i 12 . . . . 5  |-  ( ph  ->  (flds  ZZ )  e. CMnd )
13 lgseisen.1 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
1413eldifad 3324 . . . . . . . . 9  |-  ( ph  ->  P  e.  Prime )
15 lgseisen.7 . . . . . . . . . 10  |-  Y  =  (ℤ/n `  P )
1615znfld 16833 . . . . . . . . 9  |-  ( P  e.  Prime  ->  Y  e. Field
)
1714, 16syl 16 . . . . . . . 8  |-  ( ph  ->  Y  e. Field )
18 isfld 15836 . . . . . . . . 9  |-  ( Y  e. Field 
<->  ( Y  e.  DivRing  /\  Y  e.  CRing ) )
1918simprbi 451 . . . . . . . 8  |-  ( Y  e. Field  ->  Y  e.  CRing )
2017, 19syl 16 . . . . . . 7  |-  ( ph  ->  Y  e.  CRing )
21 lgseisen.8 . . . . . . . 8  |-  G  =  (mulGrp `  Y )
2221crngmgp 15664 . . . . . . 7  |-  ( Y  e.  CRing  ->  G  e. CMnd )
2320, 22syl 16 . . . . . 6  |-  ( ph  ->  G  e. CMnd )
24 cmnmnd 15419 . . . . . 6  |-  ( G  e. CMnd  ->  G  e.  Mnd )
2523, 24syl 16 . . . . 5  |-  ( ph  ->  G  e.  Mnd )
26 fzfid 11304 . . . . 5  |-  ( ph  ->  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin )
27 m1expcl 11396 . . . . . . . 8  |-  ( k  e.  ZZ  ->  ( -u 1 ^ k )  e.  ZZ )
2827adantl 453 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( -u
1 ^ k )  e.  ZZ )
29 eqidd 2436 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  =  ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) )
30 crngrng 15666 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
3120, 30syl 16 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  Ring )
32 lgseisen.9 . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Y
)
332, 32zrhrhm 16785 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
3431, 33syl 16 . . . . . . . . 9  |-  ( ph  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
35 eqid 2435 . . . . . . . . . 10  |-  ( Base `  Y )  =  (
Base `  Y )
364, 35rhmf 15819 . . . . . . . . 9  |-  ( L  e.  ( (flds  ZZ ) RingHom  Y )  ->  L : ZZ --> ( Base `  Y )
)
3734, 36syl 16 . . . . . . . 8  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
3837feqmptd 5771 . . . . . . 7  |-  ( ph  ->  L  =  ( x  e.  ZZ  |->  ( L `
 x ) ) )
39 fveq2 5720 . . . . . . 7  |-  ( x  =  ( -u 1 ^ k )  -> 
( L `  x
)  =  ( L `
 ( -u 1 ^ k ) ) )
4028, 29, 38, 39fmptco 5893 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  =  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) ) )
41 cnrng 16715 . . . . . . . . . 10  |-fld  e.  Ring
42 eqid 2435 . . . . . . . . . . 11  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
432, 42mgpress 15651 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  ZZ  e.  (SubRing ` fld ) )  ->  (
(mulGrp ` fld )s  ZZ )  =  (mulGrp `  (flds  ZZ ) ) )
4441, 1, 43mp2an 654 . . . . . . . . 9  |-  ( (mulGrp ` fld )s  ZZ )  =  (mulGrp `  (flds  ZZ ) )
4544, 21rhmmhm 15817 . . . . . . . 8  |-  ( L  e.  ( (flds  ZZ ) RingHom  Y )  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
4634, 45syl 16 . . . . . . 7  |-  ( ph  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
47 neg1cn 10059 . . . . . . . . . . 11  |-  -u 1  e.  CC
48 ax-1cn 9040 . . . . . . . . . . . 12  |-  1  e.  CC
49 ax-1ne0 9051 . . . . . . . . . . . 12  |-  1  =/=  0
5048, 49negne0i 9367 . . . . . . . . . . 11  |-  -u 1  =/=  0
51 eqid 2435 . . . . . . . . . . . 12  |-  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )  =  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
522, 42, 51expghm 16769 . . . . . . . . . . 11  |-  ( (
-u 1  e.  CC  /\  -u 1  =/=  0
)  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  ( (flds  ZZ )  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) )
5347, 50, 52mp2an 654 . . . . . . . . . 10  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) 
GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
54 ghmmhm 15008 . . . . . . . . . 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 } ) ) ) )
5553, 54ax-mp 8 . . . . . . . . 9  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) MndHom 
( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
56 cnfldbas 16699 . . . . . . . . . . . 12  |-  CC  =  ( Base ` fld )
57 cndrng 16722 . . . . . . . . . . . 12  |-fld  e.  DivRing
5856, 5, 57drngui 15833 . . . . . . . . . . 11  |-  ( CC 
\  { 0 } )  =  (Unit ` fld )
5958, 42unitsubm 15767 . . . . . . . . . 10  |-  (fld  e.  Ring  -> 
( CC  \  {
0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )
6041, 59ax-mp 8 . . . . . . . . 9  |-  ( CC 
\  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) )
6151resmhm2 14752 . . . . . . . . 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 ) ) )
6255, 60, 61mp2an 654 . . . . . . . 8  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  ( (flds  ZZ ) MndHom 
(mulGrp ` fld ) )
6342subrgsubm 15873 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
641, 63ax-mp 8 . . . . . . . . 9  |-  ZZ  e.  (SubMnd `  (mulGrp ` fld ) )
65 eqid 2435 . . . . . . . . . . 11  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  =  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )
6628, 65fmptd 5885 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) : ZZ --> ZZ )
67 frn 5589 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) : ZZ --> ZZ  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
6866, 67syl 16 . . . . . . . . 9  |-  ( ph  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
69 eqid 2435 . . . . . . . . . 10  |-  ( (mulGrp ` fld )s  ZZ )  =  (
(mulGrp ` fld )s  ZZ )
7069resmhm2b 14753 . . . . . . . . 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 ) ) ) )
7164, 68, 70sylancr 645 . . . . . . . 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 ) ) ) )
7262, 71mpbii 203 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  ( (flds  ZZ ) MndHom  ( (mulGrp ` fld )s  ZZ ) ) )
73 mhmco 14754 . . . . . . 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 ) )
7446, 72, 73syl2anc 643 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  ( (flds  ZZ ) MndHom  G ) )
7540, 74eqeltrrd 2510 . . . . 5  |-  ( ph  ->  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) )  e.  ( (flds  ZZ ) MndHom  G ) )
76 lgseisen.2 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
7776eldifad 3324 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  Prime )
78 prmnn 13074 . . . . . . . . . . 11  |-  ( Q  e.  Prime  ->  Q  e.  NN )
7977, 78syl 16 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  NN )
8079nnred 10007 . . . . . . . . 9  |-  ( ph  ->  Q  e.  RR )
81 prmnn 13074 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
8214, 81syl 16 . . . . . . . . 9  |-  ( ph  ->  P  e.  NN )
8380, 82nndivred 10040 . . . . . . . 8  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
8483adantr 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  /  P )  e.  RR )
85 2nn 10125 . . . . . . . . 9  |-  2  e.  NN
86 elfznn 11072 . . . . . . . . . 10  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
8786adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
88 nnmulcl 10015 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
8985, 87, 88sylancr 645 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
9089nnred 10007 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  RR )
9184, 90remulcld 9108 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  /  P
)  x.  ( 2  x.  x ) )  e.  RR )
9291flcld 11199 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ )
93 eqid 2435 . . . . . . . 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 ) ) ) )
9493mptpreima 5355 . . . . . . 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 } ) }
95 ssrab2 3420 . . . . . . 7  |-  { x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ( _V  \  {
0 } ) } 
C_  ( 1 ... ( ( P  - 
1 )  /  2
) )
9694, 95eqsstri 3370 . . . . . 6  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) " ( _V  \  { 0 } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
97 ssfi 7321 . . . . . 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 )
9826, 96, 97sylancl 644 . . . . 5  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )
" ( _V  \  { 0 } ) )  e.  Fin )
99 oveq2 6081 . . . . . 6  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
10099fveq2d 5724 . . . . 5  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
101 oveq2 6081 . . . . . 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 ) ) ) ) ) ) )
102101fveq2d 5724 . . . . 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 ) ) ) ) ) ) ) )
1034, 7, 12, 25, 26, 75, 92, 98, 100, 102gsummhm2 15527 . . . 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 ) ) ) ) ) ) ) )
10421, 35mgpbas 15646 . . . . . . 7  |-  ( Base `  Y )  =  (
Base `  G )
105 eqid 2435 . . . . . . 7  |-  ( 0g
`  G )  =  ( 0g `  G
)
106 eqid 2435 . . . . . . . 8  |-  ( .r
`  Y )  =  ( .r `  Y
)
10721, 106mgpplusg 15644 . . . . . . 7  |-  ( .r
`  Y )  =  ( +g  `  G
)
10837adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
109 m1expcl 11396 . . . . . . . . . 10  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
11092, 109syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
111108, 110ffvelrnd 5863 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( Base `  Y
) )
112 eqid 2435 . . . . . . . 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 ) ) ) ) ) )
113111, 112fmptd 5885 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ( Base `  Y
) )
114 1z 10303 . . . . . . . . . . . 12  |-  1  e.  ZZ
115 znegcl 10305 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  -u 1  e.  ZZ )
116114, 115ax-mp 8 . . . . . . . . . . 11  |-  -u 1  e.  ZZ
117 lgseisen.4 . . . . . . . . . . . 12  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
11877adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
119 prmz 13075 . . . . . . . . . . . . . . 15  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
120118, 119syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
12189nnzd 10366 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
122120, 121zmulcld 10373 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
12314adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
124123, 81syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
125122, 124zmodcld 11259 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  NN0 )
126117, 125syl5eqel 2519 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
127 zexpcl 11388 . . . . . . . . . . 11  |-  ( (
-u 1  e.  ZZ  /\  R  e.  NN0 )  ->  ( -u 1 ^ R )  e.  ZZ )
128116, 126, 127sylancr 645 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
129128, 120zmulcld 10373 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )
130108, 129ffvelrnd 5863 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ R )  x.  Q ) )  e.  ( Base `  Y
) )
131 eqid 2435 . . . . . . . 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 ) ) )
132130, 131fmptd 5885 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ( Base `  Y
) )
133112mptpreima 5355 . . . . . . . . 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 ) } ) }
134 ssrab2 3420 . . . . . . . . 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 ) )
135133, 134eqsstri 3370 . . . . . . . 8  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
136 ssfi 7321 . . . . . . . 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 )
13726, 135, 136sylancl 644 . . . . . . 7  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) ) ) " ( _V 
\  { ( 0g
`  G ) } ) )  e.  Fin )
138131mptpreima 5355 . . . . . . . . 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 ) } ) }
139 ssrab2 3420 . . . . . . . . 9  |-  { x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |  ( L `
 ( ( -u
1 ^ R )  x.  Q ) )  e.  ( _V  \  { ( 0g `  G ) } ) }  C_  ( 1 ... ( ( P  -  1 )  / 
2 ) )
140138, 139eqsstri 3370 . . . . . . . 8  |-  ( `' ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) " ( _V  \  { ( 0g
`  G ) } ) )  C_  (
1 ... ( ( P  -  1 )  / 
2 ) )
141 ssfi 7321 . . . . . . . 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 )
14226, 140, 141sylancl 644 . . . . . . 7  |-  ( ph  ->  ( `' ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) ) " ( _V 
\  { ( 0g
`  G ) } ) )  e.  Fin )
143104, 105, 107, 23, 26, 113, 132, 137, 142gsumadd 15520 . . . . . 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 ) ) ) ) ) )
144 eqidd 2436 . . . . . . . . 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
) ) ) ) ) ) )
145 eqidd 2436 . . . . . . . . 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 ) ) ) )
14626, 111, 130, 144, 145offval2 6314 . . . . . . . 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
) ) ) ) )
14734adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L  e.  ( (flds  ZZ ) RingHom  Y ) )
148 cnfldmul 16701 . . . . . . . . . . . . . 14  |-  x.  =  ( .r ` fld )
1492, 148ressmulr 13574 . . . . . . . . . . . . 13  |-  ( ZZ  e.  (SubRing ` fld )  ->  x.  =  ( .r `  (flds  ZZ ) ) )
1501, 149ax-mp 8 . . . . . . . . . . . 12  |-  x.  =  ( .r `  (flds  ZZ ) )
1514, 150, 106rhmmul 15820 . . . . . . . . . . 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 ) ) ) )
152147, 110, 129, 151syl3anc 1184 . . . . . . . . . 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 ) ) ) )
153122zred 10367 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
154124nnrpd 10639 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
155 modval 11244 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
156153, 154, 155syl2anc 643 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
157117, 156syl5eq 2479 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
158120zcnd 10368 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  CC )
15989nncnd 10008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  CC )
160124nncnd 10008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
161124nnne0d 10036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  0 )
162158, 159, 160, 161div23d 9819 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )
163162fveq2d 5724 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) )  =  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )
164163oveq2d 6089 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x
) )  /  P
) ) )  =  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )
165164oveq2d 6089 . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
166157, 165eqtrd 2467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
167166oveq2d 6089 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
168 prmz 13075 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
169123, 168syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
170169, 92zmulcld 10373 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )
171170zcnd 10368 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  CC )
172122zcnd 10368 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  CC )
173171, 172pncan3d 9406 . . . . . . . . . . . . . . . 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 ) ) )
174 2cn 10062 . . . . . . . . . . . . . . . . . 18  |-  2  e.  CC
175174a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  CC )
17687nncnd 10008 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  CC )
177158, 175, 176mul12d 9267 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  =  ( 2  x.  ( Q  x.  x
) ) )
178167, 173, 1773eqtrd 2471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( 2  x.  ( Q  x.  x )
) )
179178oveq2d 6089 . . . . . . . . . . . . . 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
) ) ) )
18047a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  e.  CC )
18150a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  =/=  0 )
182126nn0zd 10365 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
183 expaddz 11416 . . . . . . . . . . . . . . . 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 ) ) )
184180, 181, 170, 182, 183syl22anc 1185 . . . . . . . . . . . . . . 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 ) ) )
185 expmulz 11418 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
186180, 181, 169, 92, 185syl22anc 1185 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
18748a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  CC )
188 eldifsni 3920 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
18913, 188syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  2 )
190189necomd 2681 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  =/=  P )
191190neneqd 2614 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  2  =  P )
192191adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  =  P )
193 2z 10304 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  ZZ
194 uzid 10492 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
195193, 194ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ( ZZ>= `  2 )
196 dvdsprm 13091 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
197195, 123, 196sylancr 645 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  P  <->  2  =  P ) )
198192, 197mtbird 293 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  ||  P )
199 oexpneg 12903 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  NN  /\  -.  2  ||  P )  -> 
( -u 1 ^ P
)  =  -u (
1 ^ P ) )
200187, 124, 198, 199syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u ( 1 ^ P ) )
201 1exp 11401 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
1 ^ P )  =  1 )
202169, 201syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ P )  =  1 )
203202negeqd 9292 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u (
1 ^ P )  =  -u 1 )
204200, 203eqtrd 2467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u 1 )
205204oveq1d 6088 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
206186, 205eqtrd 2467 . . . . . . . . . . . . . . . 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 ) ) ) ) )
207206oveq1d 6088 . . . . . . . . . . . . . . 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 ) ) )
208184, 207eqtrd 2467 . . . . . . . . . . . . . 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 ) ) )
209 nnmulcl 10015 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  e.  NN  /\  x  e.  NN )  ->  ( Q  x.  x
)  e.  NN )
21079, 86, 209syl2an 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN )
211210nnnn0d 10266 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN0 )
212 2nn0 10230 . . . . . . . . . . . . . . . . 17  |-  2  e.  NN0
213212a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
214180, 211, 213expmuld 11518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( Q  x.  x ) ) )
215 sqneg 11434 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
21648, 215ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
217 sq1 11468 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ^ 2 )  =  1
218216, 217eqtri 2455 . . . . . . . . . . . . . . . . 17  |-  ( -u
1 ^ 2 )  =  1
219218oveq1i 6083 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  ( 1 ^ ( Q  x.  x
) )
220210nnzd 10366 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  ZZ )
221 1exp 11401 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  x.  x )  e.  ZZ  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
222220, 221syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
223219, 222syl5eq 2479 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  1 )
224214, 223eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  1 )
225179, 208, 2243eqtr3d 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) )  =  1 )
226225oveq1d 6088 . . . . . . . . . . . 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 ) )
227110zcnd 10368 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  CC )
228128zcnd 10368 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
229227, 228, 158mulassd 9103 . . . . . . . . . . . 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 ) ) )
230158mulid2d 9098 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  Q )  =  Q )
231226, 229, 2303eqtr3d 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) )  =  Q )
232231fveq2d 5724 . . . . . . . . . 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 ) )
233152, 232eqtr3d 2469 . . . . . . . . 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 ) )
234233mpteq2dva 4287 . . . . . . . 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 ) ) )
235146, 234eqtrd 2467 . . . . . . 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 ) ) )
236235oveq2d 6089 . . . . . 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 ) ) ) )
237 lgseisen.3 . . . . . . . 8  |-  ( ph  ->  P  =/=  Q )
238 lgseisen.5 . . . . . . . 8  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
239 lgseisen.6 . . . . . . . 8  |-  S  =  ( ( Q  x.  ( 2  x.  y
) )  mod  P
)
24013, 76, 237, 117, 238, 239, 15, 21, 32lgseisenlem3 21127 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) )  =  ( 1r `  Y
) )
241240oveq2d 6089 . . . . . 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
) ) )
242143, 236, 2413eqtr3rd 2476 . . . . 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 ) ) ) )
243104, 105, 23, 26, 113, 137gsumcl 15513 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )
244 eqid 2435 . . . . . . 7  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
24535, 106, 244rngridm 15680 . . . . . 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
) ) ) ) ) ) ) )
24631, 243, 245syl2anc 643 . . . . 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
) ) ) ) ) ) ) )
24777, 119syl 16 . . . . . . . 8  |-  ( ph  ->  Q  e.  ZZ )
24837, 247ffvelrnd 5863 . . . . . . 7  |-  ( ph  ->  ( L `  Q
)  e.  ( Base `  Y ) )
249 eqid 2435 . . . . . . . 8  |-  (.g `  G
)  =  (.g `  G
)
250104, 249gsumconst 15524 . . . . . . 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 ) ) )
25125, 26, 248, 250syl3anc 1184 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
252 oddprm 13181 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
25313, 252syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
254253nnnn0d 10266 . . . . . . . 8  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
255 hashfz1 11622 . . . . . . . 8  |-  ( ( ( P  -  1 )  /  2 )  e.  NN0  ->  ( # `  ( 1 ... (
( P  -  1 )  /  2 ) ) )  =  ( ( P  -  1 )  /  2 ) )
256254, 255syl 16 . . . . . . 7  |-  ( ph  ->  ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) )  =  ( ( P  -  1 )  / 
2 ) )
257256oveq1d 6088 . . . . . 6  |-  ( ph  ->  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
25844, 4mgpbas 15646 . . . . . . . . 9  |-  ZZ  =  ( Base `  ( (mulGrp ` fld )s  ZZ ) )
259 eqid 2435 . . . . . . . . 9  |-  (.g `  (
(mulGrp ` fld )s  ZZ ) )  =  (.g `  ( (mulGrp ` fld )s  ZZ ) )
260258, 259, 249mhmmulg 14914 . . . . . . . 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 ) ) )
26146, 254, 247, 260syl3anc 1184 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
26264a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
263 eqid 2435 . . . . . . . . . . 11  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
264263, 69, 259submmulg 14917 . . . . . . . . . 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 ) )
265262, 254, 247, 264syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )
266247zcnd 10368 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
267 cnfldexp 16726 . . . . . . . . . 10  |-  ( ( Q  e.  CC  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
268266, 254, 267syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
269265, 268eqtr3d 2469 . . . . . . . 8  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q )  =  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )
270269fveq2d 5724 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( L `
 ( Q ^
( ( P  - 
1 )  /  2
) ) ) )
271261, 270eqtr3d 2469 . . . . . 6  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  G
) ( L `  Q ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
272251, 257, 2713eqtrd 2471 . . . . 5  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
273242, 246, 2723eqtr3d 2475 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
274 subrgsubg 15866 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
2751, 274ax-mp 8 . . . . . . . . 9  |-  ZZ  e.  (SubGrp ` fld )
276 subgsubm 14954 . . . . . . . . 9  |-  ( ZZ  e.  (SubGrp ` fld )  ->  ZZ  e.  (SubMnd ` fld ) )
277275, 276mp1i 12 . . . . . . . 8  |-  ( ph  ->  ZZ  e.  (SubMnd ` fld )
)
27892, 93fmptd 5885 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ZZ )
27926, 277, 278, 2gsumsubm 14770 . . . . . . 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 ) ) ) ) ) )
28092zcnd 10368 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  CC )
28126, 280gsumfsum 16758 . . . . . . 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
) ) ) )
282279, 281eqtr3d 2469 . . . . . 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 ) ) ) )
283282oveq2d 6089 . . . . 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 ) ) ) ) )
284283fveq2d 5724 . . . 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
) ) ) ) ) )
285103, 273, 2843eqtr3d 2475 . . 3  |-  ( ph  ->  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
28682nnnn0d 10266 . . . 4  |-  ( ph  ->  P  e.  NN0 )
287 zexpcl 11388 . . . . 5  |-  ( ( Q  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
288247, 254, 287syl2anc 643 . . . 4  |-  ( ph  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
28926, 92fsumzcl 12521 . . . . 5  |-  ( ph  -> 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ )
290 m1expcl 11396 . . . . 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 )
291289, 290syl 16 . . . 4  |-  ( ph  ->  ( -u 1 ^
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  e.  ZZ )
29215, 32zndvds 16822 . . . 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 ) ) ) ) ) ) )
293286, 288, 291, 292syl3anc 1184 . . 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 ) ) ) ) ) ) )
294285, 293mpbid 202 . 2  |-  ( ph  ->  P  ||  ( ( Q ^ ( ( P  -  1 )  /  2 ) )  -  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) )
295 moddvds 12851 . . 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 ) ) ) ) ) ) )
29682, 288, 291, 295syl3anc 1184 . 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
) ) ) ) ) ) )
297294, 296mpbird 224 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 177    /\ wa 359    = wceq 1652    e. wcel 1725    =/= wne 2598   {crab 2701   _Vcvv 2948    \ cdif 3309    C_ wss 3312   {csn 3806   class class class wbr 4204    e. cmpt 4258   `'ccnv 4869   ran crn 4871   "cima 4873    o. ccom 4874   -->wf 5442   ` cfv 5446  (class class class)co 6073    o Fcof 6295   Fincfn 7101   CCcc 8980   RRcr 8981   0cc0 8982   1c1 8983    + caddc 8985    x. cmul 8987    - cmin 9283   -ucneg 9284    / cdiv 9669   NNcn 9992   2c2 10041   NN0cn0 10213   ZZcz 10274   ZZ>=cuz 10480   RR+crp 10604   ...cfz 11035   |_cfl 11193    mod cmo 11242   ^cexp 11374   #chash 11610   sum_csu 12471    || cdivides 12844   Primecprime 13071   Basecbs 13461   ↾s cress 13462   .rcmulr 13522   0gc0g 13715    gsumg cgsu 13716   Mndcmnd 14676  .gcmg 14681   MndHom cmhm 14728  SubMndcsubmnd 14729  SubGrpcsubg 14930    GrpHom cghm 14995  CMndccmn 15404   Abelcabel 15405  mulGrpcmgp 15640   Ringcrg 15652   CRingccrg 15653   1rcur 15654   RingHom crh 15809   DivRingcdr 15827  Fieldcfield 15828  SubRingcsubrg 15856  ℂfldccnfld 16695   ZRHomczrh 16770  ℤ/nczn 16773
This theorem is referenced by:  lgseisen  21129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7588  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059  ax-pre-sup 9060  ax-addf 9061  ax-mulf 9062
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-1st 6341  df-2nd 6342  df-tpos 6471  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-ec 6899  df-qs 6903  df-map 7012  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-sup 7438  df-oi 7471  df-card 7818  df-cda 8040  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-div 9670  df-nn 9993  df-2 10050  df-3 10051  df-4 10052  df-5 10053  df-6 10054  df-7 10055  df-8 10056  df-9 10057  df-10 10058  df-n0 10214  df-z 10275  df-dec 10375  df-uz 10481  df-rp 10605  df-fz 11036  df-fzo 11128  df-fl 11194  df-mod 11243  df-seq 11316  df-exp 11375  df-hash 11611  df-cj 11896  df-re 11897  df-im 11898  df-sqr 12032  df-abs 12033  df-clim 12274  df-sum 12472  df-dvds 12845  df-gcd 12999  df-prm 13072  df-struct 13463  df-ndx 13464  df-slot 13465  df-base 13466  df-sets 13467  df-ress 13468  df-plusg 13534  df-mulr 13535  df-starv 13536  df-sca 13537  df-vsca 13538  df-tset 13540  df-ple 13541  df-ds 13543  df-unif 13544  df-0g 13719  df-gsum 13720  df-imas 13726  df-divs 13727  df-mnd 14682  df-mhm 14730  df-submnd 14731  df-grp 14804  df-minusg 14805  df-sbg 14806  df-mulg 14807  df-subg 14933  df-nsg 14934  df-eqg 14935  df-ghm 14996  df-cntz 15108  df-cmn 15406  df-abl 15407  df-mgp 15641  df-rng 15655  df-cring 15656  df-ur 15657  df-oppr 15720  df-dvdsr 15738  df-unit 15739  df-invr 15769  df-dvr 15780  df-rnghom 15811  df-drng 15829  df-field 15830  df-subrg 15858  df-lmod 15944  df-lss 16001  df-lsp 16040  df-sra 16236  df-rgmod 16237  df-lidl 16238  df-rsp 16239  df-2idl 16295  df-nzr 16321  df-rlreg 16335  df-domn 16336  df-idom 16337  df-cnfld 16696  df-zrh 16774  df-zn 16777
  Copyright terms: Public domain W3C validator