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

Theorem lgseisenlem4 22671
Description: Lemma for lgseisen 22672. 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 17869 . . . . 5  |-  ZZ  =  ( Base ` ring )
2 zring0 17873 . . . . 5  |-  0  =  ( 0g ` ring )
3 zringabl 17867 . . . . . 6  |-ring  e.  Abel
4 ablcmn 16274 . . . . . 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 3335 . . . . . . . . 9  |-  ( ph  ->  P  e.  Prime )
8 lgseisen.7 . . . . . . . . . 10  |-  Y  =  (ℤ/n `  P )
98znfld 17973 . . . . . . . . 9  |-  ( P  e.  Prime  ->  Y  e. Field
)
107, 9syl 16 . . . . . . . 8  |-  ( ph  ->  Y  e. Field )
11 isfld 16821 . . . . . . . . 9  |-  ( Y  e. Field 
<->  ( Y  e.  DivRing  /\  Y  e.  CRing ) )
1211simprbi 464 . . . . . . . 8  |-  ( Y  e. Field  ->  Y  e.  CRing )
1310, 12syl 16 . . . . . . 7  |-  ( ph  ->  Y  e.  CRing )
14 lgseisen.8 . . . . . . . 8  |-  G  =  (mulGrp `  Y )
1514crngmgp 16643 . . . . . . 7  |-  ( Y  e.  CRing  ->  G  e. CMnd )
1613, 15syl 16 . . . . . 6  |-  ( ph  ->  G  e. CMnd )
17 cmnmnd 16283 . . . . . 6  |-  ( G  e. CMnd  ->  G  e.  Mnd )
1816, 17syl 16 . . . . 5  |-  ( ph  ->  G  e.  Mnd )
19 fzfid 11787 . . . . 5  |-  ( ph  ->  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin )
20 m1expcl 11880 . . . . . . . 8  |-  ( k  e.  ZZ  ->  ( -u 1 ^ k )  e.  ZZ )
2120adantl 466 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( -u
1 ^ k )  e.  ZZ )
22 eqidd 2439 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  =  ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) )
23 crngrng 16645 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
2413, 23syl 16 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  Ring )
25 lgseisen.9 . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Y
)
2625zrhrhm 17923 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  L  e.  (ring RingHom  Y ) )
2724, 26syl 16 . . . . . . . . 9  |-  ( ph  ->  L  e.  (ring RingHom  Y ) )
28 eqid 2438 . . . . . . . . . 10  |-  ( Base `  Y )  =  (
Base `  Y )
291, 28rhmf 16804 . . . . . . . . 9  |-  ( L  e.  (ring RingHom  Y )  ->  L : ZZ --> ( Base `  Y
) )
3027, 29syl 16 . . . . . . . 8  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
3130feqmptd 5739 . . . . . . 7  |-  ( ph  ->  L  =  ( x  e.  ZZ  |->  ( L `
 x ) ) )
32 fveq2 5686 . . . . . . 7  |-  ( x  =  ( -u 1 ^ k )  -> 
( L `  x
)  =  ( L `
 ( -u 1 ^ k ) ) )
3321, 22, 31, 32fmptco 5871 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  =  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) ) )
34 zringmpg 17896 . . . . . . . . 9  |-  ( (mulGrp ` fld )s  ZZ )  =  (mulGrp ` ring )
3534, 14rhmmhm 16802 . . . . . . . 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 10417 . . . . . . . . . . 11  |-  -u 1  e.  CC
38 neg1ne0 10419 . . . . . . . . . . 11  |-  -u 1  =/=  0
39 eqid 2438 . . . . . . . . . . . 12  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
40 eqid 2438 . . . . . . . . . . . 12  |-  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )  =  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
4139, 40expghm 17903 . . . . . . . . . . 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 672 . . . . . . . . . 10  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
43 ghmmhm 15748 . . . . . . . . . 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 17818 . . . . . . . . . 10  |-fld  e.  Ring
46 cnfldbas 17802 . . . . . . . . . . . 12  |-  CC  =  ( Base ` fld )
47 cnfld0 17820 . . . . . . . . . . . 12  |-  0  =  ( 0g ` fld )
48 cndrng 17825 . . . . . . . . . . . 12  |-fld  e.  DivRing
4946, 47, 48drngui 16818 . . . . . . . . . . 11  |-  ( CC 
\  { 0 } )  =  (Unit ` fld )
5049, 39unitsubm 16752 . . . . . . . . . 10  |-  (fld  e.  Ring  -> 
( CC  \  {
0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )
5145, 50ax-mp 5 . . . . . . . . 9  |-  ( CC 
\  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) )
5240resmhm2 15479 . . . . . . . . 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 672 . . . . . . . 8  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring MndHom  (mulGrp ` fld ) )
54 zsubrg 17846 . . . . . . . . . 10  |-  ZZ  e.  (SubRing ` fld )
5539subrgsubm 16858 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
5654, 55ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubMnd `  (mulGrp ` fld ) )
57 eqid 2438 . . . . . . . . . . 11  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  =  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )
5821, 57fmptd 5862 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) : ZZ --> ZZ )
59 frn 5560 . . . . . . . . . 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 2438 . . . . . . . . . 10  |-  ( (mulGrp ` fld )s  ZZ )  =  (
(mulGrp ` fld )s  ZZ )
6261resmhm2b 15480 . . . . . . . . 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 663 . . . . . . . 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 15481 . . . . . . 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 661 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  (ring MndHom  G ) )
6733, 66eqeltrrd 2513 . . . . 5  |-  ( ph  ->  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) )  e.  (ring MndHom  G
) )
68 lgseisen.2 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
6968eldifad 3335 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  Prime )
70 prmnn 13758 . . . . . . . . . . 11  |-  ( Q  e.  Prime  ->  Q  e.  NN )
7169, 70syl 16 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  NN )
7271nnred 10329 . . . . . . . . 9  |-  ( ph  ->  Q  e.  RR )
73 prmnn 13758 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
747, 73syl 16 . . . . . . . . 9  |-  ( ph  ->  P  e.  NN )
7572, 74nndivred 10362 . . . . . . . 8  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
7675adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  /  P )  e.  RR )
77 2nn 10471 . . . . . . . . 9  |-  2  e.  NN
78 elfznn 11470 . . . . . . . . . 10  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
7978adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
80 nnmulcl 10337 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
8177, 79, 80sylancr 663 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
8281nnred 10329 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  RR )
8376, 82remulcld 9406 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  /  P
)  x.  ( 2  x.  x ) )  e.  RR )
8483flcld 11640 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ )
85 eqid 2438 . . . . . 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 5696 . . . . . . 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 9372 . . . . . . 7  |-  0  e.  _V
8988a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  _V )
9085, 19, 87, 89fsuppmptdm 7623 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) finSupp  0 )
91 oveq2 6094 . . . . . 6  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
9291fveq2d 5690 . . . . 5  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
93 oveq2 6094 . . . . . 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 5690 . . . . 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 16424 . . . 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 16587 . . . . . . 7  |-  ( Base `  Y )  =  (
Base `  G )
97 eqid 2438 . . . . . . . 8  |-  ( .r
`  Y )  =  ( .r `  Y
)
9814, 97mgpplusg 16585 . . . . . . 7  |-  ( .r
`  Y )  =  ( +g  `  G
)
9930adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
100 m1expcl 11880 . . . . . . . . 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 5839 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( Base `  Y
) )
103 neg1z 10673 . . . . . . . . . 10  |-  -u 1  e.  ZZ
104 lgseisen.4 . . . . . . . . . . 11  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
10569adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
106 prmz 13759 . . . . . . . . . . . . . 14  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
107105, 106syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
10881nnzd 10738 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
109107, 108zmulcld 10745 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
1107adantr 465 . . . . . . . . . . . . 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 11720 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  NN0 )
113104, 112syl5eqel 2522 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
114 zexpcl 11872 . . . . . . . . . 10  |-  ( (
-u 1  e.  ZZ  /\  R  e.  NN0 )  ->  ( -u 1 ^ R )  e.  ZZ )
115103, 113, 114sylancr 663 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
116115, 107zmulcld 10745 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )
11799, 116ffvelrnd 5839 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ R )  x.  Q ) )  e.  ( Base `  Y
) )
118 eqid 2438 . . . . . . 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 2438 . . . . . . 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 16408 . . . . . 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 2439 . . . . . . . . 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 2439 . . . . . . . . 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 6331 . . . . . . . 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 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L  e.  (ring RingHom  Y ) )
125 zringmulr 17872 . . . . . . . . . . . 12  |-  x.  =  ( .r ` ring )
1261, 125, 97rhmmul 16805 . . . . . . . . . . 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 1218 . . . . . . . . . 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 10739 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
129111nnrpd 11018 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
130 modval 11702 . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
133107zcnd 10740 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  CC )
13481nncnd 10330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  CC )
135111nncnd 10330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
136111nnne0d 10358 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  0 )
137133, 134, 135, 136div23d 10136 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )
138137fveq2d 5690 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) )  =  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )
139138oveq2d 6102 . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
142141oveq2d 6102 . . . . . . . . . . . . . . . 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 13759 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
144110, 143syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
145144, 84zmulcld 10745 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )
146145zcnd 10740 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  CC )
147109zcnd 10740 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  CC )
148146, 147pncan3d 9714 . . . . . . . . . . . . . . . 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 10386 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  CC )
15079nncnd 10330 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  CC )
151133, 149, 150mul12d 9570 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  =  ( 2  x.  ( Q  x.  x
) ) )
152142, 148, 1513eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( 2  x.  ( Q  x.  x )
) )
153152oveq2d 6102 . . . . . . . . . . . . . 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 10737 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
157 expaddz 11900 . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . 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 11902 . . . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . . . 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 9394 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  CC )
162 eldifsni 3996 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
1636, 162syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  2 )
164163necomd 2690 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  =/=  P )
165164neneqd 2619 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  2  =  P )
166165adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  =  P )
167 2z 10670 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  ZZ
168 uzid 10867 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
169167, 168ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ( ZZ>= `  2 )
170 dvdsprm 13777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
171169, 110, 170sylancr 663 . . . . . . . . . . . . . . . . . . . . 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 13587 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  NN  /\  -.  2  ||  P )  -> 
( -u 1 ^ P
)  =  -u (
1 ^ P ) )
174161, 111, 172, 173syl3anc 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u ( 1 ^ P ) )
175 1exp 11885 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
1 ^ P )  =  1 )
176144, 175syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ P )  =  1 )
177176negeqd 9596 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u (
1 ^ P )  =  -u 1 )
178174, 177eqtrd 2470 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u 1 )
179178oveq1d 6101 . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . 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 10337 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  e.  NN  /\  x  e.  NN )  ->  ( Q  x.  x
)  e.  NN )
18471, 78, 183syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN )
185184nnnn0d 10628 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN0 )
186 2nn0 10588 . . . . . . . . . . . . . . . . 17  |-  2  e.  NN0
187186a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
188154, 185, 187expmuld 12003 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( Q  x.  x ) ) )
189 neg1sqe1 11953 . . . . . . . . . . . . . . . . 17  |-  ( -u
1 ^ 2 )  =  1
190189oveq1i 6096 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  ( 1 ^ ( Q  x.  x
) )
191184nnzd 10738 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  ZZ )
192 1exp 11885 . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  1 )
195188, 194eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  1 )
196153, 182, 1953eqtr3d 2478 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) )  =  1 )
197196oveq1d 6101 . . . . . . . . . . . 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 10740 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  CC )
199115zcnd 10740 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
200198, 199, 133mulassd 9401 . . . . . . . . . . . 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 9396 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  Q )  =  Q )
202197, 200, 2013eqtr3d 2478 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) )  =  Q )
203202fveq2d 5690 . . . . . . . . . 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 2472 . . . . . . . . 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 4373 . . . . . . . 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 2470 . . . . . . 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 6102 . . . . . 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 22670 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) )  =  ( 1r `  Y
) )
212211oveq2d 6102 . . . . . 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 2479 . . . . 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 2438 . . . . . . 7  |-  ( 0g
`  G )  =  ( 0g `  G
)
215102, 118fmptd 5862 . . . . . . 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 5696 . . . . . . . . 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 5696 . . . . . . . . 9  |-  ( 0g
`  G )  e. 
_V
219218a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 0g `  G
)  e.  _V )
220118, 19, 217, 219fsuppmptdm 7623 . . . . . . 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 16388 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )
222 eqid 2438 . . . . . . 7  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
22328, 97, 222rngridm 16659 . . . . . 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 661 . . . . 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 5839 . . . . . . 7  |-  ( ph  ->  ( L `  Q
)  e.  ( Base `  Y ) )
227 eqid 2438 . . . . . . . 8  |-  (.g `  G
)  =  (.g `  G
)
22896, 227gsumconst 16417 . . . . . . 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 1218 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
230 oddprm 13874 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
2316, 230syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
232231nnnn0d 10628 . . . . . . . 8  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
233 hashfz1 12109 . . . . . . . 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 6101 . . . . . 6  |-  ( ph  ->  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
23634, 1mgpbas 16587 . . . . . . . . 9  |-  ZZ  =  ( Base `  ( (mulGrp ` fld )s  ZZ ) )
237 eqid 2438 . . . . . . . . 9  |-  (.g `  (
(mulGrp ` fld )s  ZZ ) )  =  (.g `  ( (mulGrp ` fld )s  ZZ ) )
238236, 237, 227mhmmulg 15650 . . . . . . . 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 1218 . . . . . . 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 2438 . . . . . . . . . . 11  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
242241, 61, 237submmulg 15653 . . . . . . . . . 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 1218 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )
244225zcnd 10740 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
245 cnfldexp 17829 . . . . . . . . . 10  |-  ( ( Q  e.  CC  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
246244, 232, 245syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
247243, 246eqtr3d 2472 . . . . . . . 8  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q )  =  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )
248247fveq2d 5690 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( L `
 ( Q ^
( ( P  - 
1 )  /  2
) ) ) )
249239, 248eqtr3d 2472 . . . . . 6  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  G
) ( L `  Q ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
250229, 235, 2493eqtrd 2474 . . . . 5  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
251213, 224, 2503eqtr3d 2478 . . . 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 16851 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
25354, 252ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubGrp ` fld )
254 subgsubm 15694 . . . . . . . . 9  |-  ( ZZ  e.  (SubGrp ` fld )  ->  ZZ  e.  (SubMnd ` fld ) )
255253, 254mp1i 12 . . . . . . . 8  |-  ( ph  ->  ZZ  e.  (SubMnd ` fld )
)
25684, 85fmptd 5862 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ZZ )
257 df-zring 17864 . . . . . . . 8  |-ring  =  (flds  ZZ )
25819, 255, 256, 257gsumsubm 15499 . . . . . . 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 10740 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  CC )
26019, 259gsumfsum 17859 . . . . . . 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 2472 . . . . . 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 6102 . . . . 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 5690 . . . 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 2478 . . 3  |-  ( ph  ->  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
26574nnnn0d 10628 . . . 4  |-  ( ph  ->  P  e.  NN0 )
266 zexpcl 11872 . . . . 5  |-  ( ( Q  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
267225, 232, 266syl2anc 661 . . . 4  |-  ( ph  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
26819, 84fsumzcl 13204 . . . . 5  |-  ( ph  -> 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ )
269 m1expcl 11880 . . . . 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 17962 . . . 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 1218 . . 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 13534 . . 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 1218 . 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 1369    e. wcel 1756    =/= wne 2601   _Vcvv 2967    \ cdif 3320    C_ wss 3323   {csn 3872   class class class wbr 4287    e. cmpt 4345   ran crn 4836    o. ccom 4839   -->wf 5409   ` cfv 5413  (class class class)co 6086    oFcof 6313   Fincfn 7302   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    - cmin 9587   -ucneg 9588    / cdiv 9985   NNcn 10314   2c2 10363   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   RR+crp 10983   ...cfz 11429   |_cfl 11632    mod cmo 11700   ^cexp 11857   #chash 12095   sum_csu 13155    || cdivides 13527   Primecprime 13755   Basecbs 14166   ↾s cress 14167   .rcmulr 14231   0gc0g 14370    gsumg cgsu 14371   Mndcmnd 15401  .gcmg 15406   MndHom cmhm 15454  SubMndcsubmnd 15455  SubGrpcsubg 15666    GrpHom cghm 15735  CMndccmn 16268   Abelcabel 16269  mulGrpcmgp 16581   1rcur 16593   Ringcrg 16635   CRingccrg 16636   RingHom crh 16794   DivRingcdr 16812  Fieldcfield 16813  SubRingcsubrg 16841  ℂfldccnfld 17798  ℤringzring 17863   ZRHomczrh 17911  ℤ/nczn 17914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-tpos 6740  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-ec 7095  df-qs 7099  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-rp 10984  df-fz 11430  df-fzo 11541  df-fl 11634  df-mod 11701  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-clim 12958  df-sum 13156  df-dvds 13528  df-gcd 13683  df-prm 13756  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-starv 14245  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-unif 14253  df-0g 14372  df-gsum 14373  df-imas 14438  df-divs 14439  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-grp 15536  df-minusg 15537  df-sbg 15538  df-mulg 15539  df-subg 15669  df-nsg 15670  df-eqg 15671  df-ghm 15736  df-cntz 15826  df-cmn 16270  df-abl 16271  df-mgp 16582  df-ur 16594  df-rng 16637  df-cring 16638  df-oppr 16705  df-dvdsr 16723  df-unit 16724  df-invr 16754  df-dvr 16765  df-rnghom 16796  df-drng 16814  df-field 16815  df-subrg 16843  df-lmod 16930  df-lss 16994  df-lsp 17033  df-sra 17233  df-rgmod 17234  df-lidl 17235  df-rsp 17236  df-2idl 17294  df-nzr 17320  df-rlreg 17334  df-domn 17335  df-idom 17336  df-cnfld 17799  df-zring 17864  df-zrh 17915  df-zn 17918
This theorem is referenced by:  lgseisen  22672
  Copyright terms: Public domain W3C validator