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

Theorem lgseisenlem4 22576
Description: Lemma for lgseisen 22577. The function  M is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.)
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 zringbas 17731 . . . . 5  |-  ZZ  =  ( Base ` ring )
2 zring0 17735 . . . . 5  |-  0  =  ( 0g ` ring )
3 zringabl 17729 . . . . . 6  |-ring  e.  Abel
4 ablcmn 16263 . . . . . 6  |-  (ring  e.  Abel  ->ring  e. CMnd )
53, 4mp1i 12 . . . . 5  |-  ( ph  ->ring  e. CMnd
)
6 lgseisen.1 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
76eldifad 3328 . . . . . . . . 9  |-  ( ph  ->  P  e.  Prime )
8 lgseisen.7 . . . . . . . . . 10  |-  Y  =  (ℤ/n `  P )
98znfld 17835 . . . . . . . . 9  |-  ( P  e.  Prime  ->  Y  e. Field
)
107, 9syl 16 . . . . . . . 8  |-  ( ph  ->  Y  e. Field )
11 isfld 16765 . . . . . . . . 9  |-  ( Y  e. Field 
<->  ( Y  e.  DivRing  /\  Y  e.  CRing ) )
1211simprbi 461 . . . . . . . 8  |-  ( Y  e. Field  ->  Y  e.  CRing )
1310, 12syl 16 . . . . . . 7  |-  ( ph  ->  Y  e.  CRing )
14 lgseisen.8 . . . . . . . 8  |-  G  =  (mulGrp `  Y )
1514crngmgp 16589 . . . . . . 7  |-  ( Y  e.  CRing  ->  G  e. CMnd )
1613, 15syl 16 . . . . . 6  |-  ( ph  ->  G  e. CMnd )
17 cmnmnd 16272 . . . . . 6  |-  ( G  e. CMnd  ->  G  e.  Mnd )
1816, 17syl 16 . . . . 5  |-  ( ph  ->  G  e.  Mnd )
19 fzfid 11779 . . . . 5  |-  ( ph  ->  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin )
20 m1expcl 11872 . . . . . . . 8  |-  ( k  e.  ZZ  ->  ( -u 1 ^ k )  e.  ZZ )
2120adantl 463 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( -u
1 ^ k )  e.  ZZ )
22 eqidd 2434 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  =  ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) )
23 crngrng 16591 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
2413, 23syl 16 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  Ring )
25 lgseisen.9 . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Y
)
2625zrhrhm 17785 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  L  e.  (ring RingHom  Y ) )
2724, 26syl 16 . . . . . . . . 9  |-  ( ph  ->  L  e.  (ring RingHom  Y ) )
28 eqid 2433 . . . . . . . . . 10  |-  ( Base `  Y )  =  (
Base `  Y )
291, 28rhmf 16748 . . . . . . . . 9  |-  ( L  e.  (ring RingHom  Y )  ->  L : ZZ --> ( Base `  Y
) )
3027, 29syl 16 . . . . . . . 8  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
3130feqmptd 5732 . . . . . . 7  |-  ( ph  ->  L  =  ( x  e.  ZZ  |->  ( L `
 x ) ) )
32 fveq2 5679 . . . . . . 7  |-  ( x  =  ( -u 1 ^ k )  -> 
( L `  x
)  =  ( L `
 ( -u 1 ^ k ) ) )
3321, 22, 31, 32fmptco 5863 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  =  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) ) )
34 zringmpg 17758 . . . . . . . . 9  |-  ( (mulGrp ` fld )s  ZZ )  =  (mulGrp ` ring )
3534, 14rhmmhm 16746 . . . . . . . 8  |-  ( L  e.  (ring RingHom  Y )  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
3627, 35syl 16 . . . . . . 7  |-  ( ph  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
37 neg1cn 10413 . . . . . . . . . . 11  |-  -u 1  e.  CC
38 neg1ne0 10415 . . . . . . . . . . 11  |-  -u 1  =/=  0
39 eqid 2433 . . . . . . . . . . . 12  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
40 eqid 2433 . . . . . . . . . . . 12  |-  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )  =  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
4139, 40expghm 17765 . . . . . . . . . . 11  |-  ( (
-u 1  e.  CC  /\  -u 1  =/=  0
)  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  (ring  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) )
4237, 38, 41mp2an 665 . . . . . . . . . 10  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
43 ghmmhm 15737 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) )  e.  (ring  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )  ->  (
k  e.  ZZ  |->  (
-u 1 ^ k
) )  e.  (ring MndHom  (
(mulGrp ` fld )s  ( CC  \  { 0 } ) ) ) )
4442, 43ax-mp 5 . . . . . . . . 9  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring MndHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
45 cnrng 17682 . . . . . . . . . 10  |-fld  e.  Ring
46 cnfldbas 17666 . . . . . . . . . . . 12  |-  CC  =  ( Base ` fld )
47 cnfld0 17684 . . . . . . . . . . . 12  |-  0  =  ( 0g ` fld )
48 cndrng 17689 . . . . . . . . . . . 12  |-fld  e.  DivRing
4946, 47, 48drngui 16762 . . . . . . . . . . 11  |-  ( CC 
\  { 0 } )  =  (Unit ` fld )
5049, 39unitsubm 16696 . . . . . . . . . 10  |-  (fld  e.  Ring  -> 
( CC  \  {
0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )
5145, 50ax-mp 5 . . . . . . . . 9  |-  ( CC 
\  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) )
5240resmhm2 15470 . . . . . . . . 9  |-  ( ( ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  (ring MndHom  (
(mulGrp ` fld )s  ( CC  \  { 0 } ) ) )  /\  ( CC  \  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )  -> 
( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  (ring MndHom  (mulGrp ` fld ) ) )
5344, 51, 52mp2an 665 . . . . . . . 8  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring MndHom  (mulGrp ` fld ) )
54 zsubrg 17710 . . . . . . . . . 10  |-  ZZ  e.  (SubRing ` fld )
5539subrgsubm 16802 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
5654, 55ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubMnd `  (mulGrp ` fld ) )
57 eqid 2433 . . . . . . . . . . 11  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  =  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )
5821, 57fmptd 5855 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) : ZZ --> ZZ )
59 frn 5553 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) : ZZ --> ZZ  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
6058, 59syl 16 . . . . . . . . 9  |-  ( ph  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
61 eqid 2433 . . . . . . . . . 10  |-  ( (mulGrp ` fld )s  ZZ )  =  (
(mulGrp ` fld )s  ZZ )
6261resmhm2b 15471 . . . . . . . . 9  |-  ( ( ZZ  e.  (SubMnd `  (mulGrp ` fld ) )  /\  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  C_  ZZ )  ->  ( ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring MndHom  (mulGrp ` fld ) )  <->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  (ring MndHom  ( (mulGrp ` fld )s  ZZ ) ) ) )
6356, 60, 62sylancr 656 . . . . . . . 8  |-  ( ph  ->  ( ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  (ring MndHom  (mulGrp ` fld ) )  <->  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  (ring MndHom  ( (mulGrp ` fld )s  ZZ ) ) ) )
6453, 63mpbii 211 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  e.  (ring MndHom  (
(mulGrp ` fld )s  ZZ ) ) )
65 mhmco 15472 . . . . . . 7  |-  ( ( L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G )  /\  ( k  e.  ZZ  |->  ( -u 1 ^ k ) )  e.  (ring MndHom  ( (mulGrp ` fld )s  ZZ ) ) )  ->  ( L  o.  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) )  e.  (ring MndHom  G ) )
6636, 64, 65syl2anc 654 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  (ring MndHom  G ) )
6733, 66eqeltrrd 2508 . . . . 5  |-  ( ph  ->  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) )  e.  (ring MndHom  G
) )
68 lgseisen.2 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
6968eldifad 3328 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  Prime )
70 prmnn 13749 . . . . . . . . . . 11  |-  ( Q  e.  Prime  ->  Q  e.  NN )
7169, 70syl 16 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  NN )
7271nnred 10325 . . . . . . . . 9  |-  ( ph  ->  Q  e.  RR )
73 prmnn 13749 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
747, 73syl 16 . . . . . . . . 9  |-  ( ph  ->  P  e.  NN )
7572, 74nndivred 10358 . . . . . . . 8  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
7675adantr 462 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  /  P )  e.  RR )
77 2nn 10467 . . . . . . . . 9  |-  2  e.  NN
78 elfznn 11465 . . . . . . . . . 10  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
7978adantl 463 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
80 nnmulcl 10333 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
8177, 79, 80sylancr 656 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
8281nnred 10325 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  RR )
8376, 82remulcld 9402 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  /  P
)  x.  ( 2  x.  x ) )  e.  RR )
8483flcld 11632 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ )
85 eqid 2433 . . . . . 6  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  =  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )
86 fvex 5689 . . . . . . 7  |-  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e. 
_V
8786a1i 11 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e. 
_V )
88 c0ex 9368 . . . . . . 7  |-  0  e.  _V
8988a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  _V )
9085, 19, 87, 89fsuppmptdm 7619 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) finSupp  0 )
91 oveq2 6088 . . . . . 6  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
9291fveq2d 5683 . . . . 5  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
93 oveq2 6088 . . . . . 6  |-  ( k  =  (ring 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ (ring 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) ) ) )
9493fveq2d 5683 . . . . 5  |-  ( k  =  (ring 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ (ring  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) ) ) )
951, 2, 5, 18, 19, 67, 84, 90, 92, 94gsummhm2 16411 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  =  ( L `  ( -u 1 ^ (ring  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) ) ) )
9614, 28mgpbas 16571 . . . . . . 7  |-  ( Base `  Y )  =  (
Base `  G )
97 eqid 2433 . . . . . . . 8  |-  ( .r
`  Y )  =  ( .r `  Y
)
9814, 97mgpplusg 16569 . . . . . . 7  |-  ( .r
`  Y )  =  ( +g  `  G
)
9930adantr 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
100 m1expcl 11872 . . . . . . . . 9  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
10184, 100syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
10299, 101ffvelrnd 5832 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( Base `  Y
) )
103 neg1z 10669 . . . . . . . . . 10  |-  -u 1  e.  ZZ
104 lgseisen.4 . . . . . . . . . . 11  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
10569adantr 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
106 prmz 13750 . . . . . . . . . . . . . 14  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
107105, 106syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
10881nnzd 10734 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
109107, 108zmulcld 10741 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
1107adantr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
111110, 73syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
112109, 111zmodcld 11712 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  NN0 )
113104, 112syl5eqel 2517 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
114 zexpcl 11864 . . . . . . . . . 10  |-  ( (
-u 1  e.  ZZ  /\  R  e.  NN0 )  ->  ( -u 1 ^ R )  e.  ZZ )
115103, 113, 114sylancr 656 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
116115, 107zmulcld 10741 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )
11799, 116ffvelrnd 5832 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ R )  x.  Q ) )  e.  ( Base `  Y
) )
118 eqid 2433 . . . . . . 7  |-  ( 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 ) ) ) ) ) )
119 eqid 2433 . . . . . . 7  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) )  =  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( L `
 ( ( -u
1 ^ R )  x.  Q ) ) )
12096, 98, 16, 19, 102, 117, 118, 119gsummptfidmadd2 16397 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  oF ( .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 ) ) ) ) ) )
121 eqidd 2434 . . . . . . . . 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
) ) ) ) ) ) )
122 eqidd 2434 . . . . . . . . 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 ) ) ) )
12319, 102, 117, 121, 122offval2 6325 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  oF ( .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
) ) ) ) )
12427adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L  e.  (ring RingHom  Y ) )
125 zringmulr 17734 . . . . . . . . . . . 12  |-  x.  =  ( .r ` ring )
1261, 125, 97rhmmul 16749 . . . . . . . . . . 11  |-  ( ( L  e.  (ring 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 ) ) ) )
127124, 101, 116, 126syl3anc 1211 . . . . . . . . . 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 ) ) ) )
128109zred 10735 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
129111nnrpd 11014 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
130 modval 11694 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
131128, 129, 130syl2anc 654 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
132104, 131syl5eq 2477 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
133107zcnd 10736 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  CC )
13481nncnd 10326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  CC )
135111nncnd 10326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
136111nnne0d 10354 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  0 )
137133, 134, 135, 136div23d 10132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )
138137fveq2d 5683 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) )  =  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )
139138oveq2d 6096 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x
) )  /  P
) ) )  =  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) )
140139oveq2d 6096 . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
141132, 140eqtrd 2465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
142141oveq2d 6096 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
143 prmz 13750 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
144110, 143syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
145144, 84zmulcld 10741 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )
146145zcnd 10736 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  CC )
147109zcnd 10736 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  CC )
148146, 147pncan3d 9710 . . . . . . . . . . . . . . . 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 ) ) )
149 2cnd 10382 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  CC )
15079nncnd 10326 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  CC )
151133, 149, 150mul12d 9566 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  =  ( 2  x.  ( Q  x.  x
) ) )
152142, 148, 1513eqtrd 2469 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( 2  x.  ( Q  x.  x )
) )
153152oveq2d 6096 . . . . . . . . . . . . . 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
) ) ) )
15437a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  e.  CC )
15538a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u 1  =/=  0 )
156113nn0zd 10733 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
157 expaddz 11892 . . . . . . . . . . . . . . . 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 ) ) )
158154, 155, 145, 156, 157syl22anc 1212 . . . . . . . . . . . . . . 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 ) ) )
159 expmulz 11894 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
160154, 155, 144, 84, 159syl22anc 1212 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
161 1cnd 9390 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  CC )
162 eldifsni 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
1636, 162syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  2 )
164163necomd 2685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  =/=  P )
165164neneqd 2614 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  2  =  P )
166165adantr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  =  P )
167 2z 10666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  ZZ
168 uzid 10863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
169167, 168ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ( ZZ>= `  2 )
170 dvdsprm 13768 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
171169, 110, 170sylancr 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  P  <->  2  =  P ) )
172166, 171mtbird 301 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  ||  P )
173 oexpneg 13578 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  NN  /\  -.  2  ||  P )  -> 
( -u 1 ^ P
)  =  -u (
1 ^ P ) )
174161, 111, 172, 173syl3anc 1211 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u ( 1 ^ P ) )
175 1exp 11877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
1 ^ P )  =  1 )
176144, 175syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ P )  =  1 )
177176negeqd 9592 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u (
1 ^ P )  =  -u 1 )
178174, 177eqtrd 2465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u 1 )
179178oveq1d 6095 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
180160, 179eqtrd 2465 . . . . . . . . . . . . . . . 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 ) ) ) ) )
181180oveq1d 6095 . . . . . . . . . . . . . . 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 ) ) )
182158, 181eqtrd 2465 . . . . . . . . . . . . . 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 ) ) )
183 nnmulcl 10333 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  e.  NN  /\  x  e.  NN )  ->  ( Q  x.  x
)  e.  NN )
18471, 78, 183syl2an 474 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN )
185184nnnn0d 10624 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN0 )
186 2nn0 10584 . . . . . . . . . . . . . . . . 17  |-  2  e.  NN0
187186a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
188154, 185, 187expmuld 11995 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( Q  x.  x ) ) )
189 neg1sqe1 11945 . . . . . . . . . . . . . . . . 17  |-  ( -u
1 ^ 2 )  =  1
190189oveq1i 6090 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  ( 1 ^ ( Q  x.  x
) )
191184nnzd 10734 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  ZZ )
192 1exp 11877 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  x.  x )  e.  ZZ  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
193191, 192syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
194190, 193syl5eq 2477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  1 )
195188, 194eqtrd 2465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  1 )
196153, 182, 1953eqtr3d 2473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) )  =  1 )
197196oveq1d 6095 . . . . . . . . . . . 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 ) )
198101zcnd 10736 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  CC )
199115zcnd 10736 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
200198, 199, 133mulassd 9397 . . . . . . . . . . . 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 ) ) )
201133mulid2d 9392 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  Q )  =  Q )
202197, 200, 2013eqtr3d 2473 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) )  =  Q )
203202fveq2d 5683 . . . . . . . . . 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 ) )
204127, 203eqtr3d 2467 . . . . . . . . 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 ) )
205204mpteq2dva 4366 . . . . . . . 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 ) ) )
206123, 205eqtrd 2465 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  oF ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) )  =  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  Q ) ) )
207206oveq2d 6096 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )  oF ( .r `  Y
) ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  |->  ( L `  ( ( -u 1 ^ R )  x.  Q
) ) ) ) )  =  ( G 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( L `  Q ) ) ) )
208 lgseisen.3 . . . . . . . 8  |-  ( ph  ->  P  =/=  Q )
209 lgseisen.5 . . . . . . . 8  |-  M  =  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( ( ( (
-u 1 ^ R
)  x.  R )  mod  P )  / 
2 ) )
210 lgseisen.6 . . . . . . . 8  |-  S  =  ( ( Q  x.  ( 2  x.  y
) )  mod  P
)
2116, 68, 208, 104, 209, 210, 8, 14, 25lgseisenlem3 22575 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) )  =  ( 1r `  Y
) )
212211oveq2d 6096 . . . . . 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
) ) )
213120, 207, 2123eqtr3rd 2474 . . . . 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 ) ) ) )
214 eqid 2433 . . . . . . 7  |-  ( 0g
`  G )  =  ( 0g `  G
)
215102, 118fmptd 5855 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ( Base `  Y
) )
216 fvex 5689 . . . . . . . . 9  |-  ( L `
 ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  _V
217216a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  _V )
218 fvex 5689 . . . . . . . . 9  |-  ( 0g
`  G )  e. 
_V
219218a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 0g `  G
)  e.  _V )
220118, 19, 217, 219fsuppmptdm 7619 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) finSupp  ( 0g
`  G ) )
22196, 214, 16, 19, 215, 220gsumcl 16377 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )
222 eqid 2433 . . . . . . 7  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
22328, 97, 222rngridm 16605 . . . . . 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
) ) ) ) ) ) ) )
22424, 221, 223syl2anc 654 . . . . 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
) ) ) ) ) ) ) )
22569, 106syl 16 . . . . . . . 8  |-  ( ph  ->  Q  e.  ZZ )
22630, 225ffvelrnd 5832 . . . . . . 7  |-  ( ph  ->  ( L `  Q
)  e.  ( Base `  Y ) )
227 eqid 2433 . . . . . . . 8  |-  (.g `  G
)  =  (.g `  G
)
22896, 227gsumconst 16406 . . . . . . 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 ) ) )
22918, 19, 226, 228syl3anc 1211 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
230 oddprm 13865 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
2316, 230syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
232231nnnn0d 10624 . . . . . . . 8  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
233 hashfz1 12101 . . . . . . . 8  |-  ( ( ( P  -  1 )  /  2 )  e.  NN0  ->  ( # `  ( 1 ... (
( P  -  1 )  /  2 ) ) )  =  ( ( P  -  1 )  /  2 ) )
234232, 233syl 16 . . . . . . 7  |-  ( ph  ->  ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) )  =  ( ( P  -  1 )  / 
2 ) )
235234oveq1d 6095 . . . . . 6  |-  ( ph  ->  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
23634, 1mgpbas 16571 . . . . . . . . 9  |-  ZZ  =  ( Base `  ( (mulGrp ` fld )s  ZZ ) )
237 eqid 2433 . . . . . . . . 9  |-  (.g `  (
(mulGrp ` fld )s  ZZ ) )  =  (.g `  ( (mulGrp ` fld )s  ZZ ) )
238236, 237, 227mhmmulg 15639 . . . . . . . 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 ) ) )
23936, 232, 225, 238syl3anc 1211 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
24056a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
241 eqid 2433 . . . . . . . . . . 11  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
242241, 61, 237submmulg 15642 . . . . . . . . . 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 ) )
243240, 232, 225, 242syl3anc 1211 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )
244225zcnd 10736 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
245 cnfldexp 17693 . . . . . . . . . 10  |-  ( ( Q  e.  CC  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
246244, 232, 245syl2anc 654 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
247243, 246eqtr3d 2467 . . . . . . . 8  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q )  =  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )
248247fveq2d 5683 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( L `
 ( Q ^
( ( P  - 
1 )  /  2
) ) ) )
249239, 248eqtr3d 2467 . . . . . 6  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  G
) ( L `  Q ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
250229, 235, 2493eqtrd 2469 . . . . 5  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
251213, 224, 2503eqtr3d 2473 . . . 4  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
252 subrgsubg 16795 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
25354, 252ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubGrp ` fld )
254 subgsubm 15683 . . . . . . . . 9  |-  ( ZZ  e.  (SubGrp ` fld )  ->  ZZ  e.  (SubMnd ` fld ) )
255253, 254mp1i 12 . . . . . . . 8  |-  ( ph  ->  ZZ  e.  (SubMnd ` fld )
)
25684, 85fmptd 5855 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ZZ )
257 df-zring 17726 . . . . . . . 8  |-ring  =  (flds  ZZ )
25819, 255, 256, 257gsumsubm 15488 . . . . . . 7  |-  ( ph  ->  (fld 
gsumg  ( x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) )  |->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) ) )  =  (ring  gsumg  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  |->  ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
25984zcnd 10736 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  CC )
26019, 259gsumfsum 17723 . . . . . . 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
) ) ) )
261258, 260eqtr3d 2467 . . . . . 6  |-  ( ph  ->  (ring 
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
) ) ) )
262261oveq2d 6096 . . . . 5  |-  ( ph  ->  ( -u 1 ^ (ring 
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 ) ) ) ) )
263262fveq2d 5683 . . . 4  |-  ( ph  ->  ( L `  ( -u 1 ^ (ring  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 ) ) ) ) ) )
26495, 251, 2633eqtr3d 2473 . . 3  |-  ( ph  ->  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
26574nnnn0d 10624 . . . 4  |-  ( ph  ->  P  e.  NN0 )
266 zexpcl 11864 . . . . 5  |-  ( ( Q  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
267225, 232, 266syl2anc 654 . . . 4  |-  ( ph  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
26819, 84fsumzcl 13196 . . . . 5  |-  ( ph  -> 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ )
269 m1expcl 11872 . . . . 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 )
270268, 269syl 16 . . . 4  |-  ( ph  ->  ( -u 1 ^
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  e.  ZZ )
2718, 25zndvds 17824 . . . 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 ) ) ) ) ) ) )
272265, 267, 270, 271syl3anc 1211 . . 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 ) ) ) ) ) ) )
273264, 272mpbid 210 . 2  |-  ( ph  ->  P  ||  ( ( Q ^ ( ( P  -  1 )  /  2 ) )  -  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) ) )
274 moddvds 13525 . . 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 ) ) ) ) ) ) )
27574, 267, 270, 274syl3anc 1211 . 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
) ) ) ) ) ) )
276273, 275mpbird 232 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362    e. wcel 1755    =/= wne 2596   _Vcvv 2962    \ cdif 3313    C_ wss 3316   {csn 3865   class class class wbr 4280    e. cmpt 4338   ran crn 4828    o. ccom 4831   -->wf 5402   ` cfv 5406  (class class class)co 6080    oFcof 6307   Fincfn 7298   CCcc 9268   RRcr 9269   0cc0 9270   1c1 9271    + caddc 9273    x. cmul 9275    - cmin 9583   -ucneg 9584    / cdiv 9981   NNcn 10310   2c2 10359   NN0cn0 10567   ZZcz 10634   ZZ>=cuz 10849   RR+crp 10979   ...cfz 11424   |_cfl 11624    mod cmo 11692   ^cexp 11849   #chash 12087   sum_csu 13147    || cdivides 13518   Primecprime 13746   Basecbs 14157   ↾s cress 14158   .rcmulr 14222   0gc0g 14361    gsumg cgsu 14362   Mndcmnd 15392  .gcmg 15397   MndHom cmhm 15445  SubMndcsubmnd 15446  SubGrpcsubg 15655    GrpHom cghm 15724  CMndccmn 16257   Abelcabel 16258  mulGrpcmgp 16565   Ringcrg 16577   CRingccrg 16578   1rcur 16579   RingHom crh 16738   DivRingcdr 16756  Fieldcfield 16757  SubRingcsubrg 16785  ℂfldccnfld 17662  ℤringzring 17725   ZRHomczrh 17773  ℤ/nczn 17776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349  ax-mulf 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-tpos 6734  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-ec 7091  df-qs 7095  df-map 7204  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-sup 7679  df-oi 7712  df-card 8097  df-cda 8325  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-rp 10980  df-fz 11425  df-fzo 11533  df-fl 11626  df-mod 11693  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-clim 12950  df-sum 13148  df-dvds 13519  df-gcd 13674  df-prm 13747  df-struct 14159  df-ndx 14160  df-slot 14161  df-base 14162  df-sets 14163  df-ress 14164  df-plusg 14234  df-mulr 14235  df-starv 14236  df-sca 14237  df-vsca 14238  df-ip 14239  df-tset 14240  df-ple 14241  df-ds 14243  df-unif 14244  df-0g 14363  df-gsum 14364  df-imas 14429  df-divs 14430  df-mnd 15398  df-mhm 15447  df-submnd 15448  df-grp 15525  df-minusg 15526  df-sbg 15527  df-mulg 15528  df-subg 15658  df-nsg 15659  df-eqg 15660  df-ghm 15725  df-cntz 15815  df-cmn 16259  df-abl 16260  df-mgp 16566  df-rng 16580  df-cring 16581  df-ur 16582  df-oppr 16649  df-dvdsr 16667  df-unit 16668  df-invr 16698  df-dvr 16709  df-rnghom 16740  df-drng 16758  df-field 16759  df-subrg 16787  df-lmod 16874  df-lss 16936  df-lsp 16975  df-sra 17175  df-rgmod 17176  df-lidl 17177  df-rsp 17178  df-2idl 17236  df-nzr 17262  df-rlreg 17276  df-domn 17277  df-idom 17278  df-cnfld 17663  df-zring 17726  df-zrh 17777  df-zn 17780
This theorem is referenced by:  lgseisen  22577
  Copyright terms: Public domain W3C validator