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

Theorem lgseisenlem4 27117
Description: Lemma for lgseisen 27118. The function 𝑀 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 (πœ‘ β†’ 𝑃 ∈ (β„™ βˆ– {2}))
lgseisen.2 (πœ‘ β†’ 𝑄 ∈ (β„™ βˆ– {2}))
lgseisen.3 (πœ‘ β†’ 𝑃 β‰  𝑄)
lgseisen.4 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃)
lgseisen.5 𝑀 = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((((-1↑𝑅) Β· 𝑅) mod 𝑃) / 2))
lgseisen.6 𝑆 = ((𝑄 Β· (2 Β· 𝑦)) mod 𝑃)
lgseisen.7 π‘Œ = (β„€/nβ„€β€˜π‘ƒ)
lgseisen.8 𝐺 = (mulGrpβ€˜π‘Œ)
lgseisen.9 𝐿 = (β„€RHomβ€˜π‘Œ)
Assertion
Ref Expression
lgseisenlem4 (πœ‘ β†’ ((𝑄↑((𝑃 βˆ’ 1) / 2)) mod 𝑃) = ((-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) mod 𝑃))
Distinct variable groups:   π‘₯,𝐺   π‘₯,𝐿   π‘₯,𝑦,𝑃   πœ‘,π‘₯,𝑦   𝑦,𝑀   π‘₯,𝑄,𝑦   π‘₯,π‘Œ   π‘₯,𝑆
Allowed substitution hints:   𝑅(π‘₯,𝑦)   𝑆(𝑦)   𝐺(𝑦)   𝐿(𝑦)   𝑀(π‘₯)   π‘Œ(𝑦)

Proof of Theorem lgseisenlem4
Dummy variable π‘˜ is distinct from all other variables.
StepHypRef Expression
1 zringbas 21224 . . . . 5 β„€ = (Baseβ€˜β„€ring)
2 zring0 21229 . . . . 5 0 = (0gβ€˜β„€ring)
3 zringabl 21222 . . . . . 6 β„€ring ∈ Abel
4 ablcmn 19696 . . . . . 6 (β„€ring ∈ Abel β†’ β„€ring ∈ CMnd)
53, 4mp1i 13 . . . . 5 (πœ‘ β†’ β„€ring ∈ CMnd)
6 lgseisen.1 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ (β„™ βˆ– {2}))
76eldifad 3959 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ β„™)
8 lgseisen.7 . . . . . . . . . 10 π‘Œ = (β„€/nβ„€β€˜π‘ƒ)
98znfld 21335 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ π‘Œ ∈ Field)
107, 9syl 17 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ Field)
11 isfld 20511 . . . . . . . . 9 (π‘Œ ∈ Field ↔ (π‘Œ ∈ DivRing ∧ π‘Œ ∈ CRing))
1211simprbi 495 . . . . . . . 8 (π‘Œ ∈ Field β†’ π‘Œ ∈ CRing)
1310, 12syl 17 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ CRing)
14 lgseisen.8 . . . . . . . 8 𝐺 = (mulGrpβ€˜π‘Œ)
1514crngmgp 20135 . . . . . . 7 (π‘Œ ∈ CRing β†’ 𝐺 ∈ CMnd)
1613, 15syl 17 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ CMnd)
17 cmnmnd 19706 . . . . . 6 (𝐺 ∈ CMnd β†’ 𝐺 ∈ Mnd)
1816, 17syl 17 . . . . 5 (πœ‘ β†’ 𝐺 ∈ Mnd)
19 fzfid 13942 . . . . 5 (πœ‘ β†’ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin)
20 crngring 20139 . . . . . . . . . 10 (π‘Œ ∈ CRing β†’ π‘Œ ∈ Ring)
2113, 20syl 17 . . . . . . . . 9 (πœ‘ β†’ π‘Œ ∈ Ring)
22 lgseisen.9 . . . . . . . . . 10 𝐿 = (β„€RHomβ€˜π‘Œ)
2322zrhrhm 21280 . . . . . . . . 9 (π‘Œ ∈ Ring β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
2421, 23syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
25 eqid 2730 . . . . . . . . 9 (Baseβ€˜π‘Œ) = (Baseβ€˜π‘Œ)
261, 25rhmf 20376 . . . . . . . 8 (𝐿 ∈ (β„€ring RingHom π‘Œ) β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
2724, 26syl 17 . . . . . . 7 (πœ‘ β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
28 m1expcl 14056 . . . . . . . 8 (π‘˜ ∈ β„€ β†’ (-1β†‘π‘˜) ∈ β„€)
2928adantl 480 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„€) β†’ (-1β†‘π‘˜) ∈ β„€)
3027, 29cofmpt 7131 . . . . . 6 (πœ‘ β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) = (π‘˜ ∈ β„€ ↦ (πΏβ€˜(-1β†‘π‘˜))))
31 zringmpg 21242 . . . . . . . . 9 ((mulGrpβ€˜β„‚fld) β†Ύs β„€) = (mulGrpβ€˜β„€ring)
3231, 14rhmmhm 20370 . . . . . . . 8 (𝐿 ∈ (β„€ring RingHom π‘Œ) β†’ 𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺))
3324, 32syl 17 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺))
34 neg1cn 12330 . . . . . . . . . . 11 -1 ∈ β„‚
35 neg1ne0 12332 . . . . . . . . . . 11 -1 β‰  0
36 eqid 2730 . . . . . . . . . . . 12 (mulGrpβ€˜β„‚fld) = (mulGrpβ€˜β„‚fld)
37 eqid 2730 . . . . . . . . . . . 12 ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})) = ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))
3836, 37expghm 21246 . . . . . . . . . . 11 ((-1 ∈ β„‚ ∧ -1 β‰  0) β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring GrpHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))))
3934, 35, 38mp2an 688 . . . . . . . . . 10 (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring GrpHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})))
40 ghmmhm 19140 . . . . . . . . . 10 ((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring GrpHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))))
4139, 40ax-mp 5 . . . . . . . . 9 (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})))
42 cnring 21167 . . . . . . . . . 10 β„‚fld ∈ Ring
43 cnfldbas 21148 . . . . . . . . . . . 12 β„‚ = (Baseβ€˜β„‚fld)
44 cnfld0 21169 . . . . . . . . . . . 12 0 = (0gβ€˜β„‚fld)
45 cndrng 21174 . . . . . . . . . . . 12 β„‚fld ∈ DivRing
4643, 44, 45drngui 20506 . . . . . . . . . . 11 (β„‚ βˆ– {0}) = (Unitβ€˜β„‚fld)
4746, 36unitsubm 20277 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
4842, 47ax-mp 5 . . . . . . . . 9 (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))
4937resmhm2 18738 . . . . . . . . 9 (((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) ∧ (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))) β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)))
5041, 48, 49mp2an 688 . . . . . . . 8 (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld))
51 zsubrg 21198 . . . . . . . . . 10 β„€ ∈ (SubRingβ€˜β„‚fld)
5236subrgsubm 20475 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
5351, 52ax-mp 5 . . . . . . . . 9 β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))
5429fmpttd 7115 . . . . . . . . . 10 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)):β„€βŸΆβ„€)
5554frnd 6724 . . . . . . . . 9 (πœ‘ β†’ ran (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) βŠ† β„€)
56 eqid 2730 . . . . . . . . . 10 ((mulGrpβ€˜β„‚fld) β†Ύs β„€) = ((mulGrpβ€˜β„‚fld) β†Ύs β„€)
5756resmhm2b 18739 . . . . . . . . 9 ((β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)) ∧ ran (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) βŠ† β„€) β†’ ((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)) ↔ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))))
5853, 55, 57sylancr 585 . . . . . . . 8 (πœ‘ β†’ ((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)) ↔ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))))
5950, 58mpbii 232 . . . . . . 7 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€)))
60 mhmco 18740 . . . . . . 7 ((𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺) ∧ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))) β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
6133, 59, 60syl2anc 582 . . . . . 6 (πœ‘ β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
6230, 61eqeltrrd 2832 . . . . 5 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (πΏβ€˜(-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
63 lgseisen.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ (β„™ βˆ– {2}))
6463gausslemma2dlem0a 27095 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ β„•)
6564nnred 12231 . . . . . . . . 9 (πœ‘ β†’ 𝑄 ∈ ℝ)
666gausslemma2dlem0a 27095 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ β„•)
6765, 66nndivred 12270 . . . . . . . 8 (πœ‘ β†’ (𝑄 / 𝑃) ∈ ℝ)
6867adantr 479 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 / 𝑃) ∈ ℝ)
69 2nn 12289 . . . . . . . . 9 2 ∈ β„•
70 elfznn 13534 . . . . . . . . . 10 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) β†’ π‘₯ ∈ β„•)
7170adantl 480 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ π‘₯ ∈ β„•)
72 nnmulcl 12240 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘₯ ∈ β„•) β†’ (2 Β· π‘₯) ∈ β„•)
7369, 71, 72sylancr 585 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„•)
7473nnred 12231 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ ℝ)
7568, 74remulcld 11248 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 / 𝑃) Β· (2 Β· π‘₯)) ∈ ℝ)
7675flcld 13767 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)
77 eqid 2730 . . . . . 6 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
78 fvexd 6905 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ V)
79 c0ex 11212 . . . . . . 7 0 ∈ V
8079a1i 11 . . . . . 6 (πœ‘ β†’ 0 ∈ V)
8177, 19, 78, 80fsuppmptdm 9376 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) finSupp 0)
82 oveq2 7419 . . . . . 6 (π‘˜ = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) β†’ (-1β†‘π‘˜) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
8382fveq2d 6894 . . . . 5 (π‘˜ = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) β†’ (πΏβ€˜(-1β†‘π‘˜)) = (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
84 oveq2 7419 . . . . . 6 (π‘˜ = (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) β†’ (-1β†‘π‘˜) = (-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
8584fveq2d 6894 . . . . 5 (π‘˜ = (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) β†’ (πΏβ€˜(-1β†‘π‘˜)) = (πΏβ€˜(-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
861, 2, 5, 18, 19, 62, 76, 81, 83, 85gsummhm2 19848 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
8714, 25mgpbas 20034 . . . . . . 7 (Baseβ€˜π‘Œ) = (Baseβ€˜πΊ)
88 eqid 2730 . . . . . . . 8 (.rβ€˜π‘Œ) = (.rβ€˜π‘Œ)
8914, 88mgpplusg 20032 . . . . . . 7 (.rβ€˜π‘Œ) = (+gβ€˜πΊ)
9027adantr 479 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
91 m1expcl 14056 . . . . . . . . 9 ((βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€ β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
9276, 91syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
9390, 92ffvelcdmd 7086 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ∈ (Baseβ€˜π‘Œ))
94 neg1z 12602 . . . . . . . . . 10 -1 ∈ β„€
95 lgseisen.4 . . . . . . . . . . 11 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃)
9663eldifad 3959 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑄 ∈ β„™)
9796adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„™)
98 prmz 16616 . . . . . . . . . . . . . 14 (𝑄 ∈ β„™ β†’ 𝑄 ∈ β„€)
9997, 98syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„€)
10073nnzd 12589 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„€)
10199, 100zmulcld 12676 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ β„€)
1027adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„™)
103 prmnn 16615 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
104102, 103syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„•)
105101, 104zmodcld 13861 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) ∈ β„•0)
10695, 105eqeltrid 2835 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 ∈ β„•0)
107 zexpcl 14046 . . . . . . . . . 10 ((-1 ∈ β„€ ∧ 𝑅 ∈ β„•0) β†’ (-1↑𝑅) ∈ β„€)
10894, 106, 107sylancr 585 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑅) ∈ β„€)
109108, 99zmulcld 12676 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑𝑅) Β· 𝑄) ∈ β„€)
11090, 109ffvelcdmd 7086 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑𝑅) Β· 𝑄)) ∈ (Baseβ€˜π‘Œ))
111 eqid 2730 . . . . . . 7 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
112 eqid 2730 . . . . . . 7 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))
11387, 89, 16, 19, 93, 110, 111, 112gsummptfidmadd2 19835 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))) = ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))))
114 eqidd 2731 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
115 eqidd 2731 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))
11619, 93, 110, 114, 115offval2 7692 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄)))))
11724adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
118 zringmulr 21228 . . . . . . . . . . . 12 Β· = (.rβ€˜β„€ring)
1191, 118, 88rhmmul 20377 . . . . . . . . . . 11 ((𝐿 ∈ (β„€ring RingHom π‘Œ) ∧ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€ ∧ ((-1↑𝑅) Β· 𝑄) ∈ β„€) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))))
120117, 92, 109, 119syl3anc 1369 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))))
121101zred 12670 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ ℝ)
122104nnrpd 13018 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ ℝ+)
123 modval 13840 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 Β· (2 Β· π‘₯)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
124121, 122, 123syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
12595, 124eqtrid 2782 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
12699zcnd 12671 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„‚)
12773nncnd 12232 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„‚)
128104nncnd 12232 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„‚)
129104nnne0d 12266 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 β‰  0)
130126, 127, 128, 129div23d 12031 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) / 𝑃) = ((𝑄 / 𝑃) Β· (2 Β· π‘₯)))
131130fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)) = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
132131oveq2d 7427 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃))) = (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
133132oveq2d 7427 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
134125, 133eqtrd 2770 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
135134oveq2d 7427 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅) = ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
136 prmz 16616 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
137102, 136syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„€)
138137, 76zmulcld 12676 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
139138zcnd 12671 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„‚)
140101zcnd 12671 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ β„‚)
141139, 140pncan3d 11578 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (𝑄 Β· (2 Β· π‘₯)))
142 2cnd 12294 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 2 ∈ β„‚)
14371nncnd 12232 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ π‘₯ ∈ β„‚)
144126, 142, 143mul12d 11427 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) = (2 Β· (𝑄 Β· π‘₯)))
145135, 141, 1443eqtrd 2774 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅) = (2 Β· (𝑄 Β· π‘₯)))
146145oveq2d 7427 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = (-1↑(2 Β· (𝑄 Β· π‘₯))))
14734a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -1 ∈ β„‚)
14835a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -1 β‰  0)
149106nn0zd 12588 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 ∈ β„€)
150 expaddz 14076 . . . . . . . . . . . . . . . 16 (((-1 ∈ β„‚ ∧ -1 β‰  0) ∧ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€ ∧ 𝑅 ∈ β„€)) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)))
151147, 148, 138, 149, 150syl22anc 835 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)))
152 expmulz 14078 . . . . . . . . . . . . . . . . . 18 (((-1 ∈ β„‚ ∧ -1 β‰  0) ∧ (𝑃 ∈ β„€ ∧ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
153147, 148, 137, 76, 152syl22anc 835 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
154 1cnd 11213 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 1 ∈ β„‚)
155 eldifsni 4792 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ (β„™ βˆ– {2}) β†’ 𝑃 β‰  2)
1566, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑃 β‰  2)
157156necomd 2994 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 2 β‰  𝑃)
158157neneqd 2943 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ 2 = 𝑃)
159158adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ Β¬ 2 = 𝑃)
160 2z 12598 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ β„€
161 uzid 12841 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ β„€ β†’ 2 ∈ (β„€β‰₯β€˜2))
162160, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (β„€β‰₯β€˜2)
163 dvdsprm 16644 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ (β„€β‰₯β€˜2) ∧ 𝑃 ∈ β„™) β†’ (2 βˆ₯ 𝑃 ↔ 2 = 𝑃))
164162, 102, 163sylancr 585 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 βˆ₯ 𝑃 ↔ 2 = 𝑃))
165159, 164mtbird 324 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ Β¬ 2 βˆ₯ 𝑃)
166 oexpneg 16292 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ β„‚ ∧ 𝑃 ∈ β„• ∧ Β¬ 2 βˆ₯ 𝑃) β†’ (-1↑𝑃) = -(1↑𝑃))
167154, 104, 165, 166syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑃) = -(1↑𝑃))
168 1exp 14061 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ β„€ β†’ (1↑𝑃) = 1)
169137, 168syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1↑𝑃) = 1)
170169negeqd 11458 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -(1↑𝑃) = -1)
171167, 170eqtrd 2770 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑃) = -1)
172171oveq1d 7426 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
173153, 172eqtrd 2770 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
174173oveq1d 7426 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)))
175151, 174eqtrd 2770 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)))
176 nnmulcl 12240 . . . . . . . . . . . . . . . . . 18 ((𝑄 ∈ β„• ∧ π‘₯ ∈ β„•) β†’ (𝑄 Β· π‘₯) ∈ β„•)
17764, 70, 176syl2an 594 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„•)
178177nnnn0d 12536 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„•0)
179 2nn0 12493 . . . . . . . . . . . . . . . . 17 2 ∈ β„•0
180179a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 2 ∈ β„•0)
181147, 178, 180expmuld 14118 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(2 Β· (𝑄 Β· π‘₯))) = ((-1↑2)↑(𝑄 Β· π‘₯)))
182 neg1sqe1 14164 . . . . . . . . . . . . . . . . 17 (-1↑2) = 1
183182oveq1i 7421 . . . . . . . . . . . . . . . 16 ((-1↑2)↑(𝑄 Β· π‘₯)) = (1↑(𝑄 Β· π‘₯))
184177nnzd 12589 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„€)
185 1exp 14061 . . . . . . . . . . . . . . . . 17 ((𝑄 Β· π‘₯) ∈ β„€ β†’ (1↑(𝑄 Β· π‘₯)) = 1)
186184, 185syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1↑(𝑄 Β· π‘₯)) = 1)
187183, 186eqtrid 2782 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑2)↑(𝑄 Β· π‘₯)) = 1)
188181, 187eqtrd 2770 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(2 Β· (𝑄 Β· π‘₯))) = 1)
189146, 175, 1883eqtr3d 2778 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) = 1)
190189oveq1d 7426 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) Β· 𝑄) = (1 Β· 𝑄))
19192zcnd 12671 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„‚)
192108zcnd 12671 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑅) ∈ β„‚)
193191, 192, 126mulassd 11241 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) Β· 𝑄) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄)))
194126mullidd 11236 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1 Β· 𝑄) = 𝑄)
195190, 193, 1943eqtr3d 2778 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄)) = 𝑄)
196195fveq2d 6894 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = (πΏβ€˜π‘„))
197120, 196eqtr3d 2772 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (πΏβ€˜π‘„))
198197mpteq2dva 5247 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„)))
199116, 198eqtrd 2770 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„)))
200199oveq2d 7427 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))))
201 lgseisen.3 . . . . . . . 8 (πœ‘ β†’ 𝑃 β‰  𝑄)
202 lgseisen.5 . . . . . . . 8 𝑀 = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((((-1↑𝑅) Β· 𝑅) mod 𝑃) / 2))
203 lgseisen.6 . . . . . . . 8 𝑆 = ((𝑄 Β· (2 Β· 𝑦)) mod 𝑃)
2046, 63, 201, 95, 202, 203, 8, 14, 22lgseisenlem3 27116 . . . . . . 7 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (1rβ€˜π‘Œ))
205204oveq2d 7427 . . . . . 6 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))) = ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)))
206113, 200, 2053eqtr3rd 2779 . . . . 5 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))))
207 eqid 2730 . . . . . . 7 (0gβ€˜πΊ) = (0gβ€˜πΊ)
20893fmpttd 7115 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))):(1...((𝑃 βˆ’ 1) / 2))⟢(Baseβ€˜π‘Œ))
209 fvexd 6905 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ∈ V)
210 fvexd 6905 . . . . . . . 8 (πœ‘ β†’ (0gβ€˜πΊ) ∈ V)
211111, 19, 209, 210fsuppmptdm 9376 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) finSupp (0gβ€˜πΊ))
21287, 207, 16, 19, 208, 211gsumcl 19824 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) ∈ (Baseβ€˜π‘Œ))
213 eqid 2730 . . . . . . 7 (1rβ€˜π‘Œ) = (1rβ€˜π‘Œ)
21425, 88, 213ringridm 20158 . . . . . 6 ((π‘Œ ∈ Ring ∧ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) ∈ (Baseβ€˜π‘Œ)) β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
21521, 212, 214syl2anc 582 . . . . 5 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
21696, 98syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑄 ∈ β„€)
21727, 216ffvelcdmd 7086 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜π‘„) ∈ (Baseβ€˜π‘Œ))
218 eqid 2730 . . . . . . . 8 (.gβ€˜πΊ) = (.gβ€˜πΊ)
21987, 218gsumconst 19843 . . . . . . 7 ((𝐺 ∈ Mnd ∧ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin ∧ (πΏβ€˜π‘„) ∈ (Baseβ€˜π‘Œ)) β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)))
22018, 19, 217, 219syl3anc 1369 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)))
221 oddprm 16747 . . . . . . . . . 10 (𝑃 ∈ (β„™ βˆ– {2}) β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
2226, 221syl 17 . . . . . . . . 9 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
223222nnnn0d 12536 . . . . . . . 8 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•0)
224 hashfz1 14310 . . . . . . . 8 (((𝑃 βˆ’ 1) / 2) ∈ β„•0 β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
225223, 224syl 17 . . . . . . 7 (πœ‘ β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
226225oveq1d 7426 . . . . . 6 (πœ‘ β†’ ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
22731, 1mgpbas 20034 . . . . . . . . 9 β„€ = (Baseβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))
228 eqid 2730 . . . . . . . . 9 (.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€)) = (.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))
229227, 228, 218mhmmulg 19031 . . . . . . . 8 ((𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺) ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0 ∧ 𝑄 ∈ β„€) β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
23033, 223, 216, 229syl3anc 1369 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
23153a1i 11 . . . . . . . . . 10 (πœ‘ β†’ β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
232 eqid 2730 . . . . . . . . . . 11 (.gβ€˜(mulGrpβ€˜β„‚fld)) = (.gβ€˜(mulGrpβ€˜β„‚fld))
233232, 56, 228submmulg 19034 . . . . . . . . . 10 ((β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)) ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0 ∧ 𝑄 ∈ β„€) β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄))
234231, 223, 216, 233syl3anc 1369 . . . . . . . . 9 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄))
235216zcnd 12671 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ β„‚)
236 cnfldexp 21178 . . . . . . . . . 10 ((𝑄 ∈ β„‚ ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0) β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
237235, 223, 236syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
238234, 237eqtr3d 2772 . . . . . . . 8 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
239238fveq2d 6894 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
240230, 239eqtr3d 2772 . . . . . 6 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
241220, 226, 2403eqtrd 2774 . . . . 5 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
242206, 215, 2413eqtr3d 2778 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
243 subrgsubg 20467 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubGrpβ€˜β„‚fld))
24451, 243ax-mp 5 . . . . . . . . 9 β„€ ∈ (SubGrpβ€˜β„‚fld)
245 subgsubm 19064 . . . . . . . . 9 (β„€ ∈ (SubGrpβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜β„‚fld))
246244, 245mp1i 13 . . . . . . . 8 (πœ‘ β†’ β„€ ∈ (SubMndβ€˜β„‚fld))
24776fmpttd 7115 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))):(1...((𝑃 βˆ’ 1) / 2))βŸΆβ„€)
248 df-zring 21218 . . . . . . . 8 β„€ring = (β„‚fld β†Ύs β„€)
24919, 246, 247, 248gsumsubm 18752 . . . . . . 7 (πœ‘ β†’ (β„‚fld Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25076zcnd 12671 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„‚)
25119, 250gsumfsum 21212 . . . . . . 7 (πœ‘ β†’ (β„‚fld Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
252249, 251eqtr3d 2772 . . . . . 6 (πœ‘ β†’ (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
253252oveq2d 7427 . . . . 5 (πœ‘ β†’ (-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
254253fveq2d 6894 . . . 4 (πœ‘ β†’ (πΏβ€˜(-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25586, 242, 2543eqtr3d 2778 . . 3 (πœ‘ β†’ (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25666nnnn0d 12536 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„•0)
257 zexpcl 14046 . . . . 5 ((𝑄 ∈ β„€ ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0) β†’ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€)
258216, 223, 257syl2anc 582 . . . 4 (πœ‘ β†’ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€)
25919, 76fsumzcl 15685 . . . . 5 (πœ‘ β†’ Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)
260 m1expcl 14056 . . . . 5 (Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€ β†’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
261259, 260syl 17 . . . 4 (πœ‘ β†’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
2628, 22zndvds 21324 . . . 4 ((𝑃 ∈ β„•0 ∧ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€ ∧ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€) β†’ ((πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ↔ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
263256, 258, 261, 262syl3anc 1369 . . 3 (πœ‘ β†’ ((πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ↔ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
264255, 263mpbid 231 . 2 (πœ‘ β†’ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
265 moddvds 16212 . . 3 ((𝑃 ∈ β„• ∧ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€ ∧ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€) β†’ (((𝑄↑((𝑃 βˆ’ 1) / 2)) mod 𝑃) = ((-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
26666, 258, 261, 265syl3anc 1369 . 2 (πœ‘ β†’ (((𝑄↑((𝑃 βˆ’ 1) / 2)) mod 𝑃) = ((-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
267264, 266mpbird 256 1 (πœ‘ β†’ ((𝑄↑((𝑃 βˆ’ 1) / 2)) mod 𝑃) = ((-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) mod 𝑃))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  Vcvv 3472   βˆ– cdif 3944   βŠ† wss 3947  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  ran crn 5676   ∘ ccom 5679  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∘f cof 7670  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  2c2 12271  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12978  ...cfz 13488  βŒŠcfl 13759   mod cmo 13838  β†‘cexp 14031  β™―chash 14294  Ξ£csu 15636   βˆ₯ cdvds 16201  β„™cprime 16612  Basecbs 17148   β†Ύs cress 17177  .rcmulr 17202  0gc0g 17389   Ξ£g cgsu 17390  Mndcmnd 18659   MndHom cmhm 18703  SubMndcsubmnd 18704  .gcmg 18986  SubGrpcsubg 19036   GrpHom cghm 19127  CMndccmn 19689  Abelcabl 19690  mulGrpcmgp 20028  1rcur 20075  Ringcrg 20127  CRingccrg 20128   RingHom crh 20360  SubRingcsubrg 20457  DivRingcdr 20500  Fieldcfield 20501  β„‚fldccnfld 21144  β„€ringczring 21217  β„€RHomczrh 21268  β„€/nβ„€czn 21271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-xnn0 12549  df-z 12563  df-dec 12682  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-sum 15637  df-dvds 16202  df-gcd 16440  df-prm 16613  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-0g 17391  df-gsum 17392  df-imas 17458  df-qus 17459  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18987  df-subg 19039  df-nsg 19040  df-eqg 19041  df-ghm 19128  df-cntz 19222  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-cring 20130  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-dvr 20292  df-rhm 20363  df-nzr 20404  df-subrng 20434  df-subrg 20459  df-drng 20502  df-field 20503  df-lmod 20616  df-lss 20687  df-lsp 20727  df-sra 20930  df-rgmod 20931  df-lidl 20932  df-rsp 20933  df-2idl 21006  df-rlreg 21099  df-domn 21100  df-idom 21101  df-cnfld 21145  df-zring 21218  df-zrh 21272  df-zn 21275
This theorem is referenced by:  lgseisen  27118
  Copyright terms: Public domain W3C validator