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

Theorem lgseisenlem4 23900
Description: Lemma for lgseisen 23901. 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 18706 . . . . 5  |-  ZZ  =  ( Base ` ring )
2 zring0 18710 . . . . 5  |-  0  =  ( 0g ` ring )
3 zringabl 18704 . . . . . 6  |-ring  e.  Abel
4 ablcmn 17020 . . . . . 6  |-  (ring  e.  Abel  ->ring  e. CMnd )
53, 4mp1i 13 . . . . 5  |-  ( ph  ->ring  e. CMnd
)
6 lgseisen.1 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
76eldifad 3425 . . . . . . . . 9  |-  ( ph  ->  P  e.  Prime )
8 lgseisen.7 . . . . . . . . . 10  |-  Y  =  (ℤ/n `  P )
98znfld 18789 . . . . . . . . 9  |-  ( P  e.  Prime  ->  Y  e. Field
)
107, 9syl 17 . . . . . . . 8  |-  ( ph  ->  Y  e. Field )
11 isfld 17617 . . . . . . . . 9  |-  ( Y  e. Field 
<->  ( Y  e.  DivRing  /\  Y  e.  CRing ) )
1211simprbi 462 . . . . . . . 8  |-  ( Y  e. Field  ->  Y  e.  CRing )
1310, 12syl 17 . . . . . . 7  |-  ( ph  ->  Y  e.  CRing )
14 lgseisen.8 . . . . . . . 8  |-  G  =  (mulGrp `  Y )
1514crngmgp 17418 . . . . . . 7  |-  ( Y  e.  CRing  ->  G  e. CMnd )
1613, 15syl 17 . . . . . 6  |-  ( ph  ->  G  e. CMnd )
17 cmnmnd 17029 . . . . . 6  |-  ( G  e. CMnd  ->  G  e.  Mnd )
1816, 17syl 17 . . . . 5  |-  ( ph  ->  G  e.  Mnd )
19 fzfid 12037 . . . . 5  |-  ( ph  ->  ( 1 ... (
( P  -  1 )  /  2 ) )  e.  Fin )
20 m1expcl 12143 . . . . . . . 8  |-  ( k  e.  ZZ  ->  ( -u 1 ^ k )  e.  ZZ )
2120adantl 464 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( -u
1 ^ k )  e.  ZZ )
22 eqidd 2403 . . . . . . 7  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) )  =  ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) )
23 crngring 17421 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
2413, 23syl 17 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  Ring )
25 lgseisen.9 . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Y
)
2625zrhrhm 18741 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  L  e.  (ring RingHom  Y ) )
2724, 26syl 17 . . . . . . . . 9  |-  ( ph  ->  L  e.  (ring RingHom  Y ) )
28 eqid 2402 . . . . . . . . . 10  |-  ( Base `  Y )  =  (
Base `  Y )
291, 28rhmf 17587 . . . . . . . . 9  |-  ( L  e.  (ring RingHom  Y )  ->  L : ZZ --> ( Base `  Y
) )
3027, 29syl 17 . . . . . . . 8  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
3130feqmptd 5858 . . . . . . 7  |-  ( ph  ->  L  =  ( x  e.  ZZ  |->  ( L `
 x ) ) )
32 fveq2 5805 . . . . . . 7  |-  ( x  =  ( -u 1 ^ k )  -> 
( L `  x
)  =  ( L `
 ( -u 1 ^ k ) ) )
3321, 22, 31, 32fmptco 5999 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  =  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) ) )
34 zringmpg 18721 . . . . . . . . 9  |-  ( (mulGrp ` fld )s  ZZ )  =  (mulGrp ` ring )
3534, 14rhmmhm 17583 . . . . . . . 8  |-  ( L  e.  (ring RingHom  Y )  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
3627, 35syl 17 . . . . . . 7  |-  ( ph  ->  L  e.  ( ( (mulGrp ` fld )s  ZZ ) MndHom  G ) )
37 neg1cn 10600 . . . . . . . . . . 11  |-  -u 1  e.  CC
38 neg1ne0 10602 . . . . . . . . . . 11  |-  -u 1  =/=  0
39 eqid 2402 . . . . . . . . . . . 12  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
40 eqid 2402 . . . . . . . . . . . 12  |-  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )  =  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) )
4139, 40expghm 18725 . . . . . . . . . . 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 670 . . . . . . . . . 10  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring  GrpHom  ( (mulGrp ` fld )s  ( CC  \  { 0 } ) ) )
43 ghmmhm 16493 . . . . . . . . . 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 cnring 18652 . . . . . . . . . 10  |-fld  e.  Ring
46 cnfldbas 18636 . . . . . . . . . . . 12  |-  CC  =  ( Base ` fld )
47 cnfld0 18654 . . . . . . . . . . . 12  |-  0  =  ( 0g ` fld )
48 cndrng 18659 . . . . . . . . . . . 12  |-fld  e.  DivRing
4946, 47, 48drngui 17614 . . . . . . . . . . 11  |-  ( CC 
\  { 0 } )  =  (Unit ` fld )
5049, 39unitsubm 17531 . . . . . . . . . 10  |-  (fld  e.  Ring  -> 
( CC  \  {
0 } )  e.  (SubMnd `  (mulGrp ` fld ) ) )
5145, 50ax-mp 5 . . . . . . . . 9  |-  ( CC 
\  { 0 } )  e.  (SubMnd `  (mulGrp ` fld ) )
5240resmhm2 16207 . . . . . . . . 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 670 . . . . . . . 8  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  e.  (ring MndHom  (mulGrp ` fld ) )
54 zsubrg 18683 . . . . . . . . . 10  |-  ZZ  e.  (SubRing ` fld )
5539subrgsubm 17654 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  (mulGrp ` fld ) ) )
5654, 55ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubMnd `  (mulGrp ` fld ) )
57 eqid 2402 . . . . . . . . . . 11  |-  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )  =  ( k  e.  ZZ  |->  ( -u
1 ^ k ) )
5821, 57fmptd 5989 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  ZZ  |->  ( -u 1 ^ k
) ) : ZZ --> ZZ )
59 frn 5676 . . . . . . . . . 10  |-  ( ( k  e.  ZZ  |->  (
-u 1 ^ k
) ) : ZZ --> ZZ  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
6058, 59syl 17 . . . . . . . . 9  |-  ( ph  ->  ran  ( k  e.  ZZ  |->  ( -u 1 ^ k ) ) 
C_  ZZ )
61 eqid 2402 . . . . . . . . . 10  |-  ( (mulGrp ` fld )s  ZZ )  =  (
(mulGrp ` fld )s  ZZ )
6261resmhm2b 16208 . . . . . . . . 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 661 . . . . . . . 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 16209 . . . . . . 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 659 . . . . . 6  |-  ( ph  ->  ( L  o.  (
k  e.  ZZ  |->  (
-u 1 ^ k
) ) )  e.  (ring MndHom  G ) )
6733, 66eqeltrrd 2491 . . . . 5  |-  ( ph  ->  ( k  e.  ZZ  |->  ( L `  ( -u
1 ^ k ) ) )  e.  (ring MndHom  G
) )
68 lgseisen.2 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
6968eldifad 3425 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  Prime )
70 prmnn 14321 . . . . . . . . . . 11  |-  ( Q  e.  Prime  ->  Q  e.  NN )
7169, 70syl 17 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  NN )
7271nnred 10511 . . . . . . . . 9  |-  ( ph  ->  Q  e.  RR )
73 prmnn 14321 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
747, 73syl 17 . . . . . . . . 9  |-  ( ph  ->  P  e.  NN )
7572, 74nndivred 10545 . . . . . . . 8  |-  ( ph  ->  ( Q  /  P
)  e.  RR )
7675adantr 463 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  /  P )  e.  RR )
77 2nn 10654 . . . . . . . . 9  |-  2  e.  NN
78 elfznn 11685 . . . . . . . . . 10  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
7978adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  NN )
80 nnmulcl 10519 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  x  e.  NN )  ->  ( 2  x.  x
)  e.  NN )
8177, 79, 80sylancr 661 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  NN )
8281nnred 10511 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  RR )
8376, 82remulcld 9574 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  /  P
)  x.  ( 2  x.  x ) )  e.  RR )
8483flcld 11885 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  ZZ )
85 eqid 2402 . . . . . 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 5815 . . . . . . 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 9540 . . . . . . 7  |-  0  e.  _V
8988a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  _V )
9085, 19, 87, 89fsuppmptdm 7794 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) finSupp  0 )
91 oveq2 6242 . . . . . 6  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( -u 1 ^ k )  =  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )
9291fveq2d 5809 . . . . 5  |-  ( k  =  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) )  ->  ( L `  ( -u 1 ^ k ) )  =  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
93 oveq2 6242 . . . . . 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 5809 . . . . 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 17176 . . . 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 17359 . . . . . . 7  |-  ( Base `  Y )  =  (
Base `  G )
97 eqid 2402 . . . . . . . 8  |-  ( .r
`  Y )  =  ( .r `  Y
)
9814, 97mgpplusg 17357 . . . . . . 7  |-  ( .r
`  Y )  =  ( +g  `  G
)
9930adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
100 m1expcl 12143 . . . . . . . . 9  |-  ( ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
10184, 100syl 17 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  ZZ )
10299, 101ffvelrnd 5966 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) ) )  e.  ( Base `  Y
) )
103 neg1z 10861 . . . . . . . . . 10  |-  -u 1  e.  ZZ
104 lgseisen.4 . . . . . . . . . . 11  |-  R  =  ( ( Q  x.  ( 2  x.  x
) )  mod  P
)
10569adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  Prime )
106 prmz 14322 . . . . . . . . . . . . . 14  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
107105, 106syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  ZZ )
10881nnzd 10927 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  ZZ )
109107, 108zmulcld 10934 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  ZZ )
1107adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
111110, 73syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
112109, 111zmodcld 11968 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  mod  P )  e.  NN0 )
113104, 112syl5eqel 2494 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  NN0 )
114 zexpcl 12135 . . . . . . . . . 10  |-  ( (
-u 1  e.  ZZ  /\  R  e.  NN0 )  ->  ( -u 1 ^ R )  e.  ZZ )
115103, 113, 114sylancr 661 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  ZZ )
116115, 107zmulcld 10934 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ R
)  x.  Q )  e.  ZZ )
11799, 116ffvelrnd 5966 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( ( -u 1 ^ R )  x.  Q ) )  e.  ( Base `  Y
) )
118 eqid 2402 . . . . . . 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 2402 . . . . . . 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 17159 . . . . . 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 2403 . . . . . . . . 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 2403 . . . . . . . . 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 6494 . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L  e.  (ring RingHom  Y ) )
125 zringmulr 18709 . . . . . . . . . . . 12  |-  x.  =  ( .r ` ring )
1261, 125, 97rhmmul 17588 . . . . . . . . . . 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 1230 . . . . . . . . . 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 10928 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  RR )
129111nnrpd 11220 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR+ )
130 modval 11949 . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . 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 2455 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) ) ) ) )
133107zcnd 10929 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  Q  e.  CC )
13481nncnd 10512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  x )  e.  CC )
135111nncnd 10512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  CC )
136111nnne0d 10541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  =/=  0 )
137133, 134, 135, 136div23d 10318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( Q  x.  (
2  x.  x ) )  /  P )  =  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )
138137fveq2d 5809 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  x.  ( 2  x.  x ) )  /  P ) )  =  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) )
139138oveq2d 6250 . . . . . . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  =  ( ( Q  x.  ( 2  x.  x ) )  -  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
142141oveq2d 6250 . . . . . . . . . . . . . . . 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 14322 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
144110, 143syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
145144, 84zmulcld 10934 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  ZZ )
146145zcnd 10929 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  x.  ( |_ `  ( ( Q  /  P )  x.  (
2  x.  x ) ) ) )  e.  CC )
147109zcnd 10929 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  e.  CC )
148146, 147pncan3d 9890 . . . . . . . . . . . . . . . 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 10569 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  CC )
15079nncnd 10512 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  x  e.  CC )
151133, 149, 150mul12d 9743 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  ( 2  x.  x ) )  =  ( 2  x.  ( Q  x.  x
) ) )
152142, 148, 1513eqtrd 2447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  x.  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  +  R )  =  ( 2  x.  ( Q  x.  x )
) )
153152oveq2d 6250 . . . . . . . . . . . . . 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 10926 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  R  e.  ZZ )
157 expaddz 12164 . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . 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 12166 . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . 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 9562 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  1  e.  CC )
162 eldifsni 4097 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  =/=  2 )
1636, 162syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  P  =/=  2 )
164163necomd 2674 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  2  =/=  P )
165164neneqd 2605 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  2  =  P )
166165adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  =  P )
167 2z 10857 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  ZZ
168 uzid 11059 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
169167, 168ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ( ZZ>= `  2 )
170 dvdsprm 14341 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  P  e.  Prime )  ->  (
2  ||  P  <->  2  =  P ) )
171169, 110, 170sylancr 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  ||  P  <->  2  =  P ) )
172166, 171mtbird 299 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  2  ||  P )
173 oexpneg 14150 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  P  e.  NN  /\  -.  2  ||  P )  -> 
( -u 1 ^ P
)  =  -u (
1 ^ P ) )
174161, 111, 172, 173syl3anc 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u ( 1 ^ P ) )
175 1exp 12149 . . . . . . . . . . . . . . . . . . . . 21  |-  ( P  e.  ZZ  ->  (
1 ^ P )  =  1 )
176144, 175syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ P )  =  1 )
177176negeqd 9770 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -u (
1 ^ P )  =  -u 1 )
178174, 177eqtrd 2443 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ P )  =  -u 1 )
179178oveq1d 6249 . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 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 6249 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . 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 10519 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  e.  NN  /\  x  e.  NN )  ->  ( Q  x.  x
)  e.  NN )
18471, 78, 183syl2an 475 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN )
185184nnnn0d 10813 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  NN0 )
186 2nn0 10773 . . . . . . . . . . . . . . . . 17  |-  2  e.  NN0
187186a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
188154, 185, 187expmuld 12267 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  ( ( -u
1 ^ 2 ) ^ ( Q  x.  x ) ) )
189 neg1sqe1 12218 . . . . . . . . . . . . . . . . 17  |-  ( -u
1 ^ 2 )  =  1
190189oveq1i 6244 . . . . . . . . . . . . . . . 16  |-  ( (
-u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  ( 1 ^ ( Q  x.  x
) )
191184nnzd 10927 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( Q  x.  x )  e.  ZZ )
192 1exp 12149 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  x.  x )  e.  ZZ  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
193191, 192syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1 ^ ( Q  x.  x ) )  =  1 )
194190, 193syl5eq 2455 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ 2 ) ^ ( Q  x.  x ) )  =  1 )
195188, 194eqtrd 2443 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( 2  x.  ( Q  x.  x ) ) )  =  1 )
196153, 182, 1953eqtr3d 2451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( -u 1 ^ R ) )  =  1 )
197196oveq1d 6249 . . . . . . . . . . . 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 10929 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  e.  CC )
199115zcnd 10929 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -u 1 ^ R )  e.  CC )
200198, 199, 133mulassd 9569 . . . . . . . . . . . 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 9564 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
1  x.  Q )  =  Q )
202197, 200, 2013eqtr3d 2451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( -u 1 ^ ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) )  x.  ( ( -u
1 ^ R )  x.  Q ) )  =  Q )
203202fveq2d 5809 . . . . . . . . . 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 2445 . . . . . . . . 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 4480 . . . . . . . 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 2443 . . . . . . 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 6250 . . . . . 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 23899 . . . . . . 7  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
( -u 1 ^ R
)  x.  Q ) ) ) )  =  ( 1r `  Y
) )
212211oveq2d 6250 . . . . . 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 2452 . . . . 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 2402 . . . . . . 7  |-  ( 0g
`  G )  =  ( 0g `  G
)
215102, 118fmptd 5989 . . . . . . 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 5815 . . . . . . . . 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 5815 . . . . . . . . 9  |-  ( 0g
`  G )  e. 
_V
219218a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 0g `  G
)  e.  _V )
220118, 19, 217, 219fsuppmptdm 7794 . . . . . . 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 17139 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  ( -u 1 ^ ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) ) )  e.  ( Base `  Y
) )
222 eqid 2402 . . . . . . 7  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
22328, 97, 222ringridm 17435 . . . . . 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 659 . . . . 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 17 . . . . . . . 8  |-  ( ph  ->  Q  e.  ZZ )
22630, 225ffvelrnd 5966 . . . . . . 7  |-  ( ph  ->  ( L `  Q
)  e.  ( Base `  Y ) )
227 eqid 2402 . . . . . . . 8  |-  (.g `  G
)  =  (.g `  G
)
22896, 227gsumconst 17169 . . . . . . 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 1230 . . . . . 6  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) ) )
230 oddprm 14440 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
2316, 230syl 17 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
232231nnnn0d 10813 . . . . . . . 8  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
233 hashfz1 12373 . . . . . . . 8  |-  ( ( ( P  -  1 )  /  2 )  e.  NN0  ->  ( # `  ( 1 ... (
( P  -  1 )  /  2 ) ) )  =  ( ( P  -  1 )  /  2 ) )
234232, 233syl 17 . . . . . . 7  |-  ( ph  ->  ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) )  =  ( ( P  -  1 )  / 
2 ) )
235234oveq1d 6249 . . . . . 6  |-  ( ph  ->  ( ( # `  (
1 ... ( ( P  -  1 )  / 
2 ) ) ) (.g `  G ) ( L `  Q ) )  =  ( ( ( P  -  1 )  /  2 ) (.g `  G ) ( L `  Q ) ) )
23634, 1mgpbas 17359 . . . . . . . . 9  |-  ZZ  =  ( Base `  ( (mulGrp ` fld )s  ZZ ) )
237 eqid 2402 . . . . . . . . 9  |-  (.g `  (
(mulGrp ` fld )s  ZZ ) )  =  (.g `  ( (mulGrp ` fld )s  ZZ ) )
238236, 237, 227mhmmulg 16390 . . . . . . . 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 1230 . . . . . . 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 2402 . . . . . . . . . . 11  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
242241, 61, 237submmulg 16393 . . . . . . . . . 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 1230 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q ) )
244225zcnd 10929 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
245 cnfldexp 18663 . . . . . . . . . 10  |-  ( ( Q  e.  CC  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
246244, 232, 245syl2anc 659 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (mulGrp ` fld ) ) Q )  =  ( Q ^ (
( P  -  1 )  /  2 ) ) )
247243, 246eqtr3d 2445 . . . . . . . 8  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  (
(mulGrp ` fld )s  ZZ ) ) Q )  =  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )
248247fveq2d 5809 . . . . . . 7  |-  ( ph  ->  ( L `  (
( ( P  - 
1 )  /  2
) (.g `  ( (mulGrp ` fld )s  ZZ ) ) Q ) )  =  ( L `
 ( Q ^
( ( P  - 
1 )  /  2
) ) ) )
249239, 248eqtr3d 2445 . . . . . 6  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 ) (.g `  G
) ( L `  Q ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
250229, 235, 2493eqtrd 2447 . . . . 5  |-  ( ph  ->  ( G  gsumg  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  Q
) ) )  =  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) ) )
251213, 224, 2503eqtr3d 2451 . . . 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 17647 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubGrp ` fld ) )
25354, 252ax-mp 5 . . . . . . . . 9  |-  ZZ  e.  (SubGrp ` fld )
254 subgsubm 16439 . . . . . . . . 9  |-  ( ZZ  e.  (SubGrp ` fld )  ->  ZZ  e.  (SubMnd ` fld ) )
255253, 254mp1i 13 . . . . . . . 8  |-  ( ph  ->  ZZ  e.  (SubMnd ` fld )
)
25684, 85fmptd 5989 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( |_ `  (
( Q  /  P
)  x.  ( 2  x.  x ) ) ) ) : ( 1 ... ( ( P  -  1 )  /  2 ) ) --> ZZ )
257 df-zring 18701 . . . . . . . 8  |-ring  =  (flds  ZZ )
25819, 255, 256, 257gsumsubm 16220 . . . . . . 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 10929 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x
) ) )  e.  CC )
26019, 259gsumfsum 18696 . . . . . . 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 2445 . . . . . 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 6250 . . . . 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 5809 . . . 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 2451 . . 3  |-  ( ph  ->  ( L `  ( Q ^ ( ( P  -  1 )  / 
2 ) ) )  =  ( L `  ( -u 1 ^ sum_ x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) ) ( |_
`  ( ( Q  /  P )  x.  ( 2  x.  x
) ) ) ) ) )
26574nnnn0d 10813 . . . 4  |-  ( ph  ->  P  e.  NN0 )
266 zexpcl 12135 . . . . 5  |-  ( ( Q  e.  ZZ  /\  ( ( P  - 
1 )  /  2
)  e.  NN0 )  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
267225, 232, 266syl2anc 659 . . . 4  |-  ( ph  ->  ( Q ^ (
( P  -  1 )  /  2 ) )  e.  ZZ )
26819, 84fsumzcl 13613 . . . . 5  |-  ( ph  -> 
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) )  e.  ZZ )
269 m1expcl 12143 . . . . 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 17 . . . 4  |-  ( ph  ->  ( -u 1 ^
sum_ x  e.  (
1 ... ( ( P  -  1 )  / 
2 ) ) ( |_ `  ( ( Q  /  P )  x.  ( 2  x.  x ) ) ) )  e.  ZZ )
2718, 25zndvds 18778 . . . 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 1230 . . 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 14094 . . 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 1230 . 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 367    = wceq 1405    e. wcel 1842    =/= wne 2598   _Vcvv 3058    \ cdif 3410    C_ wss 3413   {csn 3971   class class class wbr 4394    |-> cmpt 4452   ran crn 4943    o. ccom 4946   -->wf 5521   ` cfv 5525  (class class class)co 6234    oFcof 6475   Fincfn 7474   CCcc 9440   RRcr 9441   0cc0 9442   1c1 9443    + caddc 9445    x. cmul 9447    - cmin 9761   -ucneg 9762    / cdiv 10167   NNcn 10496   2c2 10546   NN0cn0 10756   ZZcz 10825   ZZ>=cuz 11045   RR+crp 11183   ...cfz 11643   |_cfl 11877    mod cmo 11947   ^cexp 12120   #chash 12359   sum_csu 13564    || cdvds 14087   Primecprime 14318   Basecbs 14733   ↾s cress 14734   .rcmulr 14802   0gc0g 14946    gsumg cgsu 14947   Mndcmnd 16135   MndHom cmhm 16180  SubMndcsubmnd 16181  .gcmg 16272  SubGrpcsubg 16411    GrpHom cghm 16480  CMndccmn 17014   Abelcabl 17015  mulGrpcmgp 17353   1rcur 17365   Ringcrg 17410   CRingccrg 17411   RingHom crh 17573   DivRingcdr 17608  Fieldcfield 17609  SubRingcsubrg 17637  ℂfldccnfld 18632  ℤringzring 18700   ZRHomczrh 18729  ℤ/nczn 18732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-inf2 8011  ax-cnex 9498  ax-resscn 9499  ax-1cn 9500  ax-icn 9501  ax-addcl 9502  ax-addrcl 9503  ax-mulcl 9504  ax-mulrcl 9505  ax-mulcom 9506  ax-addass 9507  ax-mulass 9508  ax-distr 9509  ax-i2m1 9510  ax-1ne0 9511  ax-1rid 9512  ax-rnegex 9513  ax-rrecex 9514  ax-cnre 9515  ax-pre-lttri 9516  ax-pre-lttrn 9517  ax-pre-ltadd 9518  ax-pre-mulgt0 9519  ax-pre-sup 9520  ax-addf 9521  ax-mulf 9522
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-of 6477  df-om 6639  df-1st 6738  df-2nd 6739  df-supp 6857  df-tpos 6912  df-recs 6999  df-rdg 7033  df-1o 7087  df-2o 7088  df-oadd 7091  df-er 7268  df-ec 7270  df-qs 7274  df-map 7379  df-en 7475  df-dom 7476  df-sdom 7477  df-fin 7478  df-fsupp 7784  df-sup 7855  df-oi 7889  df-card 8272  df-cda 8500  df-pnf 9580  df-mnf 9581  df-xr 9582  df-ltxr 9583  df-le 9584  df-sub 9763  df-neg 9764  df-div 10168  df-nn 10497  df-2 10555  df-3 10556  df-4 10557  df-5 10558  df-6 10559  df-7 10560  df-8 10561  df-9 10562  df-10 10563  df-n0 10757  df-z 10826  df-dec 10940  df-uz 11046  df-rp 11184  df-fz 11644  df-fzo 11768  df-fl 11879  df-mod 11948  df-seq 12062  df-exp 12121  df-hash 12360  df-cj 12988  df-re 12989  df-im 12990  df-sqrt 13124  df-abs 13125  df-clim 13367  df-sum 13565  df-dvds 14088  df-gcd 14246  df-prm 14319  df-struct 14735  df-ndx 14736  df-slot 14737  df-base 14738  df-sets 14739  df-ress 14740  df-plusg 14814  df-mulr 14815  df-starv 14816  df-sca 14817  df-vsca 14818  df-ip 14819  df-tset 14820  df-ple 14821  df-ds 14823  df-unif 14824  df-0g 14948  df-gsum 14949  df-imas 15014  df-qus 15015  df-mgm 16088  df-sgrp 16127  df-mnd 16137  df-mhm 16182  df-submnd 16183  df-grp 16273  df-minusg 16274  df-sbg 16275  df-mulg 16276  df-subg 16414  df-nsg 16415  df-eqg 16416  df-ghm 16481  df-cntz 16571  df-cmn 17016  df-abl 17017  df-mgp 17354  df-ur 17366  df-ring 17412  df-cring 17413  df-oppr 17484  df-dvdsr 17502  df-unit 17503  df-invr 17533  df-dvr 17544  df-rnghom 17576  df-drng 17610  df-field 17611  df-subrg 17639  df-lmod 17726  df-lss 17791  df-lsp 17830  df-sra 18030  df-rgmod 18031  df-lidl 18032  df-rsp 18033  df-2idl 18092  df-nzr 18118  df-rlreg 18143  df-domn 18144  df-idom 18145  df-cnfld 18633  df-zring 18701  df-zrh 18733  df-zn 18736
This theorem is referenced by:  lgseisen  23901
  Copyright terms: Public domain W3C validator