# Metamath Proof Explorer

## Theorem lgseisenlem4

Description: Lemma for lgseisen . 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)

Ref Expression
Hypotheses lgseisen.1 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.2 ${⊢}{\phi }\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.3 ${⊢}{\phi }\to {P}\ne {Q}$
lgseisen.4 ${⊢}{R}={Q}2{x}\mathrm{mod}{P}$
lgseisen.5 ${⊢}{M}=\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)⟼\frac{{\left(-1\right)}^{{R}}{R}\mathrm{mod}{P}}{2}\right)$
lgseisen.6 ${⊢}{S}={Q}2{y}\mathrm{mod}{P}$
lgseisen.7 ${⊢}{Y}=ℤ/{P}ℤ$
lgseisen.8 ${⊢}{G}={\mathrm{mulGrp}}_{{Y}}$
lgseisen.9 ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
Assertion lgseisenlem4 ${⊢}{\phi }\to {{Q}}^{\frac{{P}-1}{2}}\mathrm{mod}{P}={\left(-1\right)}^{\sum _{{x}=1}^{\frac{{P}-1}{2}}⌊\left(\frac{{Q}}{{P}}\right)2{x}⌋}\mathrm{mod}{P}$

### Proof

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