Step |
Hyp |
Ref |
Expression |
1 |
|
lgseisen.1 |
|- ( ph -> P e. ( Prime \ { 2 } ) ) |
2 |
|
lgseisen.2 |
|- ( ph -> Q e. ( Prime \ { 2 } ) ) |
3 |
|
lgseisen.3 |
|- ( ph -> P =/= Q ) |
4 |
|
lgseisen.4 |
|- R = ( ( Q x. ( 2 x. x ) ) mod P ) |
5 |
|
lgseisen.5 |
|- M = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ( ( -u 1 ^ R ) x. R ) mod P ) / 2 ) ) |
6 |
|
lgseisen.6 |
|- S = ( ( Q x. ( 2 x. y ) ) mod P ) |
7 |
|
lgseisen.7 |
|- Y = ( Z/nZ ` P ) |
8 |
|
lgseisen.8 |
|- G = ( mulGrp ` Y ) |
9 |
|
lgseisen.9 |
|- L = ( ZRHom ` Y ) |
10 |
|
zringbas |
|- ZZ = ( Base ` ZZring ) |
11 |
|
zring0 |
|- 0 = ( 0g ` ZZring ) |
12 |
|
zringabl |
|- ZZring e. Abel |
13 |
|
ablcmn |
|- ( ZZring e. Abel -> ZZring e. CMnd ) |
14 |
12 13
|
mp1i |
|- ( ph -> ZZring e. CMnd ) |
15 |
1
|
eldifad |
|- ( ph -> P e. Prime ) |
16 |
7
|
znfld |
|- ( P e. Prime -> Y e. Field ) |
17 |
15 16
|
syl |
|- ( ph -> Y e. Field ) |
18 |
|
isfld |
|- ( Y e. Field <-> ( Y e. DivRing /\ Y e. CRing ) ) |
19 |
18
|
simprbi |
|- ( Y e. Field -> Y e. CRing ) |
20 |
17 19
|
syl |
|- ( ph -> Y e. CRing ) |
21 |
8
|
crngmgp |
|- ( Y e. CRing -> G e. CMnd ) |
22 |
20 21
|
syl |
|- ( ph -> G e. CMnd ) |
23 |
|
cmnmnd |
|- ( G e. CMnd -> G e. Mnd ) |
24 |
22 23
|
syl |
|- ( ph -> G e. Mnd ) |
25 |
|
fzfid |
|- ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin ) |
26 |
|
crngring |
|- ( Y e. CRing -> Y e. Ring ) |
27 |
20 26
|
syl |
|- ( ph -> Y e. Ring ) |
28 |
9
|
zrhrhm |
|- ( Y e. Ring -> L e. ( ZZring RingHom Y ) ) |
29 |
27 28
|
syl |
|- ( ph -> L e. ( ZZring RingHom Y ) ) |
30 |
|
eqid |
|- ( Base ` Y ) = ( Base ` Y ) |
31 |
10 30
|
rhmf |
|- ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) ) |
32 |
29 31
|
syl |
|- ( ph -> L : ZZ --> ( Base ` Y ) ) |
33 |
|
m1expcl |
|- ( k e. ZZ -> ( -u 1 ^ k ) e. ZZ ) |
34 |
33
|
adantl |
|- ( ( ph /\ k e. ZZ ) -> ( -u 1 ^ k ) e. ZZ ) |
35 |
32 34
|
cofmpt |
|- ( ph -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) = ( k e. ZZ |-> ( L ` ( -u 1 ^ k ) ) ) ) |
36 |
|
zringmpg |
|- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring ) |
37 |
36 8
|
rhmmhm |
|- ( L e. ( ZZring RingHom Y ) -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) ) |
38 |
29 37
|
syl |
|- ( ph -> L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) ) |
39 |
|
neg1cn |
|- -u 1 e. CC |
40 |
|
neg1ne0 |
|- -u 1 =/= 0 |
41 |
|
eqid |
|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld ) |
42 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
43 |
41 42
|
expghm |
|- ( ( -u 1 e. CC /\ -u 1 =/= 0 ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ) |
44 |
39 40 43
|
mp2an |
|- ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) |
45 |
|
ghmmhm |
|- ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ) |
46 |
44 45
|
ax-mp |
|- ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) |
47 |
|
cnring |
|- CCfld e. Ring |
48 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
49 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
50 |
|
cndrng |
|- CCfld e. DivRing |
51 |
48 49 50
|
drngui |
|- ( CC \ { 0 } ) = ( Unit ` CCfld ) |
52 |
51 41
|
unitsubm |
|- ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
53 |
47 52
|
ax-mp |
|- ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) |
54 |
42
|
resmhm2 |
|- ( ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) ) |
55 |
46 53 54
|
mp2an |
|- ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) |
56 |
|
zsubrg |
|- ZZ e. ( SubRing ` CCfld ) |
57 |
41
|
subrgsubm |
|- ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
58 |
56 57
|
ax-mp |
|- ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) |
59 |
34
|
fmpttd |
|- ( ph -> ( k e. ZZ |-> ( -u 1 ^ k ) ) : ZZ --> ZZ ) |
60 |
59
|
frnd |
|- ( ph -> ran ( k e. ZZ |-> ( -u 1 ^ k ) ) C_ ZZ ) |
61 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( ( mulGrp ` CCfld ) |`s ZZ ) |
62 |
61
|
resmhm2b |
|- ( ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ran ( k e. ZZ |-> ( -u 1 ^ k ) ) C_ ZZ ) -> ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) <-> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) ) |
63 |
58 60 62
|
sylancr |
|- ( ph -> ( ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( mulGrp ` CCfld ) ) <-> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) ) |
64 |
55 63
|
mpbii |
|- ( ph -> ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) |
65 |
|
mhmco |
|- ( ( L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) /\ ( k e. ZZ |-> ( -u 1 ^ k ) ) e. ( ZZring MndHom ( ( mulGrp ` CCfld ) |`s ZZ ) ) ) -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) ) |
66 |
38 64 65
|
syl2anc |
|- ( ph -> ( L o. ( k e. ZZ |-> ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) ) |
67 |
35 66
|
eqeltrrd |
|- ( ph -> ( k e. ZZ |-> ( L ` ( -u 1 ^ k ) ) ) e. ( ZZring MndHom G ) ) |
68 |
2
|
gausslemma2dlem0a |
|- ( ph -> Q e. NN ) |
69 |
68
|
nnred |
|- ( ph -> Q e. RR ) |
70 |
1
|
gausslemma2dlem0a |
|- ( ph -> P e. NN ) |
71 |
69 70
|
nndivred |
|- ( ph -> ( Q / P ) e. RR ) |
72 |
71
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q / P ) e. RR ) |
73 |
|
2nn |
|- 2 e. NN |
74 |
|
elfznn |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN ) |
75 |
74
|
adantl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. NN ) |
76 |
|
nnmulcl |
|- ( ( 2 e. NN /\ x e. NN ) -> ( 2 x. x ) e. NN ) |
77 |
73 75 76
|
sylancr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. NN ) |
78 |
77
|
nnred |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. RR ) |
79 |
72 78
|
remulcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q / P ) x. ( 2 x. x ) ) e. RR ) |
80 |
79
|
flcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ ) |
81 |
|
eqid |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) |
82 |
|
fvexd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. _V ) |
83 |
|
c0ex |
|- 0 e. _V |
84 |
83
|
a1i |
|- ( ph -> 0 e. _V ) |
85 |
81 25 82 84
|
fsuppmptdm |
|- ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) finSupp 0 ) |
86 |
|
oveq2 |
|- ( k = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) |
87 |
86
|
fveq2d |
|- ( k = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) -> ( L ` ( -u 1 ^ k ) ) = ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) |
88 |
|
oveq2 |
|- ( k = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) |
89 |
88
|
fveq2d |
|- ( k = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) -> ( L ` ( -u 1 ^ k ) ) = ( L ` ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ) |
90 |
10 11 14 24 25 67 80 85 87 89
|
gsummhm2 |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) = ( L ` ( -u 1 ^ ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ) |
91 |
8 30
|
mgpbas |
|- ( Base ` Y ) = ( Base ` G ) |
92 |
|
eqid |
|- ( .r ` Y ) = ( .r ` Y ) |
93 |
8 92
|
mgpplusg |
|- ( .r ` Y ) = ( +g ` G ) |
94 |
32
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L : ZZ --> ( Base ` Y ) ) |
95 |
|
m1expcl |
|- ( ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) |
96 |
80 95
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) |
97 |
94 96
|
ffvelrnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) e. ( Base ` Y ) ) |
98 |
|
neg1z |
|- -u 1 e. ZZ |
99 |
2
|
eldifad |
|- ( ph -> Q e. Prime ) |
100 |
99
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. Prime ) |
101 |
|
prmz |
|- ( Q e. Prime -> Q e. ZZ ) |
102 |
100 101
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. ZZ ) |
103 |
77
|
nnzd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. ZZ ) |
104 |
102 103
|
zmulcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. ZZ ) |
105 |
15
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime ) |
106 |
|
prmnn |
|- ( P e. Prime -> P e. NN ) |
107 |
105 106
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN ) |
108 |
104 107
|
zmodcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) mod P ) e. NN0 ) |
109 |
4 108
|
eqeltrid |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. NN0 ) |
110 |
|
zexpcl |
|- ( ( -u 1 e. ZZ /\ R e. NN0 ) -> ( -u 1 ^ R ) e. ZZ ) |
111 |
98 109 110
|
sylancr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. ZZ ) |
112 |
111 102
|
zmulcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ R ) x. Q ) e. ZZ ) |
113 |
94 112
|
ffvelrnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ R ) x. Q ) ) e. ( Base ` Y ) ) |
114 |
|
eqid |
|- ( 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 ) ) ) ) ) ) |
115 |
|
eqid |
|- ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) |
116 |
91 93 22 25 97 113 114 115
|
gsummptfidmadd2 |
|- ( ph -> ( G gsum ( ( 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 gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) ) |
117 |
|
eqidd |
|- ( 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 ) ) ) ) ) ) ) |
118 |
|
eqidd |
|- ( 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 ) ) ) ) |
119 |
25 97 113 117 118
|
offval2 |
|- ( 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 ) ) ) ) ) |
120 |
29
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L e. ( ZZring RingHom Y ) ) |
121 |
|
zringmulr |
|- x. = ( .r ` ZZring ) |
122 |
10 121 92
|
rhmmul |
|- ( ( L e. ( ZZring 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 ) ) ) ) |
123 |
120 96 112 122
|
syl3anc |
|- ( ( 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 ) ) ) ) |
124 |
104
|
zred |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. RR ) |
125 |
107
|
nnrpd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR+ ) |
126 |
|
modval |
|- ( ( ( 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 ) ) ) ) ) |
127 |
124 125 126
|
syl2anc |
|- ( ( 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 ) ) ) ) ) |
128 |
4 127
|
syl5eq |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) ) ) |
129 |
102
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> Q e. CC ) |
130 |
77
|
nncnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. x ) e. CC ) |
131 |
107
|
nncnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. CC ) |
132 |
107
|
nnne0d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P =/= 0 ) |
133 |
129 130 131 132
|
div23d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( Q x. ( 2 x. x ) ) / P ) = ( ( Q / P ) x. ( 2 x. x ) ) ) |
134 |
133
|
fveq2d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) = ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) |
135 |
134
|
oveq2d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q x. ( 2 x. x ) ) / P ) ) ) = ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) |
136 |
135
|
oveq2d |
|- ( ( 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 ) ) ) ) ) ) |
137 |
128 136
|
eqtrd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R = ( ( Q x. ( 2 x. x ) ) - ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) |
138 |
137
|
oveq2d |
|- ( ( 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 ) ) ) ) ) ) ) |
139 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
140 |
105 139
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ ) |
141 |
140 80
|
zmulcld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) |
142 |
141
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC ) |
143 |
104
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) e. CC ) |
144 |
142 143
|
pncan3d |
|- ( ( 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 ) ) ) |
145 |
|
2cnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. CC ) |
146 |
75
|
nncnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> x e. CC ) |
147 |
129 145 146
|
mul12d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. ( 2 x. x ) ) = ( 2 x. ( Q x. x ) ) ) |
148 |
138 144 147
|
3eqtrd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P x. ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) + R ) = ( 2 x. ( Q x. x ) ) ) |
149 |
148
|
oveq2d |
|- ( ( 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 ) ) ) ) |
150 |
39
|
a1i |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 e. CC ) |
151 |
40
|
a1i |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u 1 =/= 0 ) |
152 |
109
|
nn0zd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> R e. ZZ ) |
153 |
|
expaddz |
|- ( ( ( -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 ) ) ) |
154 |
150 151 141 152 153
|
syl22anc |
|- ( ( 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 ) ) ) |
155 |
|
expmulz |
|- ( ( ( -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 ) ) ) ) ) |
156 |
150 151 140 80 155
|
syl22anc |
|- ( ( 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 ) ) ) ) ) |
157 |
|
1cnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 1 e. CC ) |
158 |
|
eldifsni |
|- ( P e. ( Prime \ { 2 } ) -> P =/= 2 ) |
159 |
1 158
|
syl |
|- ( ph -> P =/= 2 ) |
160 |
159
|
necomd |
|- ( ph -> 2 =/= P ) |
161 |
160
|
neneqd |
|- ( ph -> -. 2 = P ) |
162 |
161
|
adantr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. 2 = P ) |
163 |
|
2z |
|- 2 e. ZZ |
164 |
|
uzid |
|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) ) |
165 |
163 164
|
ax-mp |
|- 2 e. ( ZZ>= ` 2 ) |
166 |
|
dvdsprm |
|- ( ( 2 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 2 || P <-> 2 = P ) ) |
167 |
165 105 166
|
sylancr |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 || P <-> 2 = P ) ) |
168 |
162 167
|
mtbird |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. 2 || P ) |
169 |
|
oexpneg |
|- ( ( 1 e. CC /\ P e. NN /\ -. 2 || P ) -> ( -u 1 ^ P ) = -u ( 1 ^ P ) ) |
170 |
157 107 168 169
|
syl3anc |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ P ) = -u ( 1 ^ P ) ) |
171 |
|
1exp |
|- ( P e. ZZ -> ( 1 ^ P ) = 1 ) |
172 |
140 171
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 ^ P ) = 1 ) |
173 |
172
|
negeqd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -u ( 1 ^ P ) = -u 1 ) |
174 |
170 173
|
eqtrd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ P ) = -u 1 ) |
175 |
174
|
oveq1d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ P ) ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) = ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) |
176 |
156 175
|
eqtrd |
|- ( ( 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 ) ) ) ) ) |
177 |
176
|
oveq1d |
|- ( ( 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 ) ) ) |
178 |
154 177
|
eqtrd |
|- ( ( 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 ) ) ) |
179 |
|
nnmulcl |
|- ( ( Q e. NN /\ x e. NN ) -> ( Q x. x ) e. NN ) |
180 |
68 74 179
|
syl2an |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. NN ) |
181 |
180
|
nnnn0d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. NN0 ) |
182 |
|
2nn0 |
|- 2 e. NN0 |
183 |
182
|
a1i |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. NN0 ) |
184 |
150 181 183
|
expmuld |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( 2 x. ( Q x. x ) ) ) = ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) ) |
185 |
|
neg1sqe1 |
|- ( -u 1 ^ 2 ) = 1 |
186 |
185
|
oveq1i |
|- ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) = ( 1 ^ ( Q x. x ) ) |
187 |
180
|
nnzd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( Q x. x ) e. ZZ ) |
188 |
|
1exp |
|- ( ( Q x. x ) e. ZZ -> ( 1 ^ ( Q x. x ) ) = 1 ) |
189 |
187 188
|
syl |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 ^ ( Q x. x ) ) = 1 ) |
190 |
186 189
|
syl5eq |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ 2 ) ^ ( Q x. x ) ) = 1 ) |
191 |
184 190
|
eqtrd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( 2 x. ( Q x. x ) ) ) = 1 ) |
192 |
149 178 191
|
3eqtr3d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) = 1 ) |
193 |
192
|
oveq1d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( -u 1 ^ R ) ) x. Q ) = ( 1 x. Q ) ) |
194 |
96
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. CC ) |
195 |
111
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -u 1 ^ R ) e. CC ) |
196 |
194 195 129
|
mulassd |
|- ( ( 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 ) ) ) |
197 |
129
|
mulid2d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 x. Q ) = Q ) |
198 |
193 196 197
|
3eqtr3d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) = Q ) |
199 |
198
|
fveq2d |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) x. ( ( -u 1 ^ R ) x. Q ) ) ) = ( L ` Q ) ) |
200 |
123 199
|
eqtr3d |
|- ( ( 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 ) ) |
201 |
200
|
mpteq2dva |
|- ( 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 ) ) ) |
202 |
119 201
|
eqtrd |
|- ( 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 ) ) ) |
203 |
202
|
oveq2d |
|- ( ph -> ( G gsum ( ( 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 gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) ) |
204 |
1 2 3 4 5 6 7 8 9
|
lgseisenlem3 |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) = ( 1r ` Y ) ) |
205 |
204
|
oveq2d |
|- ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( ( -u 1 ^ R ) x. Q ) ) ) ) ) = ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) ) |
206 |
116 203 205
|
3eqtr3rd |
|- ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) ) |
207 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
208 |
97
|
fmpttd |
|- ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( Base ` Y ) ) |
209 |
|
fvexd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) e. _V ) |
210 |
|
fvexd |
|- ( ph -> ( 0g ` G ) e. _V ) |
211 |
114 25 209 210
|
fsuppmptdm |
|- ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) finSupp ( 0g ` G ) ) |
212 |
91 207 22 25 208 211
|
gsumcl |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) e. ( Base ` Y ) ) |
213 |
|
eqid |
|- ( 1r ` Y ) = ( 1r ` Y ) |
214 |
30 92 213
|
ringridm |
|- ( ( Y e. Ring /\ ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ) |
215 |
27 212 214
|
syl2anc |
|- ( ph -> ( ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ( .r ` Y ) ( 1r ` Y ) ) = ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) ) |
216 |
99 101
|
syl |
|- ( ph -> Q e. ZZ ) |
217 |
32 216
|
ffvelrnd |
|- ( ph -> ( L ` Q ) e. ( Base ` Y ) ) |
218 |
|
eqid |
|- ( .g ` G ) = ( .g ` G ) |
219 |
91 218
|
gsumconst |
|- ( ( G e. Mnd /\ ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin /\ ( L ` Q ) e. ( Base ` Y ) ) -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) ) |
220 |
24 25 217 219
|
syl3anc |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) ) |
221 |
|
oddprm |
|- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN ) |
222 |
1 221
|
syl |
|- ( ph -> ( ( P - 1 ) / 2 ) e. NN ) |
223 |
222
|
nnnn0d |
|- ( ph -> ( ( P - 1 ) / 2 ) e. NN0 ) |
224 |
|
hashfz1 |
|- ( ( ( P - 1 ) / 2 ) e. NN0 -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) ) |
225 |
223 224
|
syl |
|- ( ph -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) ) |
226 |
225
|
oveq1d |
|- ( ph -> ( ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) ( .g ` G ) ( L ` Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) ) |
227 |
36 10
|
mgpbas |
|- ZZ = ( Base ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) |
228 |
|
eqid |
|- ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) |
229 |
227 228 218
|
mhmmulg |
|- ( ( L e. ( ( ( mulGrp ` CCfld ) |`s ZZ ) MndHom G ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ Q e. ZZ ) -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) ) |
230 |
38 223 216 229
|
syl3anc |
|- ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) ) |
231 |
58
|
a1i |
|- ( ph -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
232 |
|
eqid |
|- ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) ) |
233 |
232 61 228
|
submmulg |
|- ( ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ( ( P - 1 ) / 2 ) e. NN0 /\ Q e. ZZ ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) |
234 |
231 223 216 233
|
syl3anc |
|- ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) |
235 |
216
|
zcnd |
|- ( ph -> Q e. CC ) |
236 |
|
cnfldexp |
|- ( ( Q e. CC /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) ) |
237 |
235 223 236
|
syl2anc |
|- ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` CCfld ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) ) |
238 |
234 237
|
eqtr3d |
|- ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) = ( Q ^ ( ( P - 1 ) / 2 ) ) ) |
239 |
238
|
fveq2d |
|- ( ph -> ( L ` ( ( ( P - 1 ) / 2 ) ( .g ` ( ( mulGrp ` CCfld ) |`s ZZ ) ) Q ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) ) |
240 |
230 239
|
eqtr3d |
|- ( ph -> ( ( ( P - 1 ) / 2 ) ( .g ` G ) ( L ` Q ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) ) |
241 |
220 226 240
|
3eqtrd |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` Q ) ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) ) |
242 |
206 215 241
|
3eqtr3d |
|- ( ph -> ( G gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( -u 1 ^ ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) ) = ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) ) |
243 |
|
subrgsubg |
|- ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) ) |
244 |
56 243
|
ax-mp |
|- ZZ e. ( SubGrp ` CCfld ) |
245 |
|
subgsubm |
|- ( ZZ e. ( SubGrp ` CCfld ) -> ZZ e. ( SubMnd ` CCfld ) ) |
246 |
244 245
|
mp1i |
|- ( ph -> ZZ e. ( SubMnd ` CCfld ) ) |
247 |
80
|
fmpttd |
|- ( ph -> ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ZZ ) |
248 |
|
df-zring |
|- ZZring = ( CCfld |`s ZZ ) |
249 |
25 246 247 248
|
gsumsubm |
|- ( ph -> ( CCfld gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) = ( ZZring gsum ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) |
250 |
80
|
zcnd |
|- ( ( ph /\ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. CC ) |
251 |
25 250
|
gsumfsum |
|- ( ph -> ( CCfld gsum ( 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 ) ) ) ) |
252 |
249 251
|
eqtr3d |
|- ( ph -> ( ZZring gsum ( 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 ) ) ) ) |
253 |
252
|
oveq2d |
|- ( ph -> ( -u 1 ^ ( ZZring gsum ( 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 ) ) ) ) ) |
254 |
253
|
fveq2d |
|- ( ph -> ( L ` ( -u 1 ^ ( ZZring gsum ( 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 ) ) ) ) ) ) |
255 |
90 242 254
|
3eqtr3d |
|- ( ph -> ( L ` ( Q ^ ( ( P - 1 ) / 2 ) ) ) = ( L ` ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) |
256 |
70
|
nnnn0d |
|- ( ph -> P e. NN0 ) |
257 |
|
zexpcl |
|- ( ( Q e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) |
258 |
216 223 257
|
syl2anc |
|- ( ph -> ( Q ^ ( ( P - 1 ) / 2 ) ) e. ZZ ) |
259 |
25 80
|
fsumzcl |
|- ( ph -> sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) e. ZZ ) |
260 |
|
m1expcl |
|- ( 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 ) |
261 |
259 260
|
syl |
|- ( ph -> ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) e. ZZ ) |
262 |
7 9
|
zndvds |
|- ( ( 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 ) ) ) ) ) ) ) |
263 |
256 258 261 262
|
syl3anc |
|- ( 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 ) ) ) ) ) ) ) |
264 |
255 263
|
mpbid |
|- ( ph -> P || ( ( Q ^ ( ( P - 1 ) / 2 ) ) - ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) ) ) |
265 |
|
moddvds |
|- ( ( 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 ) ) ) ) ) ) ) |
266 |
70 258 261 265
|
syl3anc |
|- ( 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 ) ) ) ) ) ) ) |
267 |
264 266
|
mpbird |
|- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) ) |