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

Theorem lgseisenlem4 26729
Description: Lemma for lgseisen 26730. 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 20878 . . . . 5 β„€ = (Baseβ€˜β„€ring)
2 zring0 20882 . . . . 5 0 = (0gβ€˜β„€ring)
3 zringabl 20876 . . . . . 6 β„€ring ∈ Abel
4 ablcmn 19570 . . . . . 6 (β„€ring ∈ Abel β†’ β„€ring ∈ CMnd)
53, 4mp1i 13 . . . . 5 (πœ‘ β†’ β„€ring ∈ CMnd)
6 lgseisen.1 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ (β„™ βˆ– {2}))
76eldifad 3923 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ β„™)
8 lgseisen.7 . . . . . . . . . 10 π‘Œ = (β„€/nβ„€β€˜π‘ƒ)
98znfld 20970 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ π‘Œ ∈ Field)
107, 9syl 17 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ Field)
11 isfld 20197 . . . . . . . . 9 (π‘Œ ∈ Field ↔ (π‘Œ ∈ DivRing ∧ π‘Œ ∈ CRing))
1211simprbi 498 . . . . . . . 8 (π‘Œ ∈ Field β†’ π‘Œ ∈ CRing)
1310, 12syl 17 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ CRing)
14 lgseisen.8 . . . . . . . 8 𝐺 = (mulGrpβ€˜π‘Œ)
1514crngmgp 19973 . . . . . . 7 (π‘Œ ∈ CRing β†’ 𝐺 ∈ CMnd)
1613, 15syl 17 . . . . . 6 (πœ‘ β†’ 𝐺 ∈ CMnd)
17 cmnmnd 19580 . . . . . 6 (𝐺 ∈ CMnd β†’ 𝐺 ∈ Mnd)
1816, 17syl 17 . . . . 5 (πœ‘ β†’ 𝐺 ∈ Mnd)
19 fzfid 13879 . . . . 5 (πœ‘ β†’ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin)
20 crngring 19977 . . . . . . . . . 10 (π‘Œ ∈ CRing β†’ π‘Œ ∈ Ring)
2113, 20syl 17 . . . . . . . . 9 (πœ‘ β†’ π‘Œ ∈ Ring)
22 lgseisen.9 . . . . . . . . . 10 𝐿 = (β„€RHomβ€˜π‘Œ)
2322zrhrhm 20915 . . . . . . . . 9 (π‘Œ ∈ Ring β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
2421, 23syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
25 eqid 2737 . . . . . . . . 9 (Baseβ€˜π‘Œ) = (Baseβ€˜π‘Œ)
261, 25rhmf 20159 . . . . . . . 8 (𝐿 ∈ (β„€ring RingHom π‘Œ) β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
2724, 26syl 17 . . . . . . 7 (πœ‘ β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
28 m1expcl 13993 . . . . . . . 8 (π‘˜ ∈ β„€ β†’ (-1β†‘π‘˜) ∈ β„€)
2928adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„€) β†’ (-1β†‘π‘˜) ∈ β„€)
3027, 29cofmpt 7079 . . . . . 6 (πœ‘ β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) = (π‘˜ ∈ β„€ ↦ (πΏβ€˜(-1β†‘π‘˜))))
31 zringmpg 20895 . . . . . . . . 9 ((mulGrpβ€˜β„‚fld) β†Ύs β„€) = (mulGrpβ€˜β„€ring)
3231, 14rhmmhm 20154 . . . . . . . 8 (𝐿 ∈ (β„€ring RingHom π‘Œ) β†’ 𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺))
3324, 32syl 17 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺))
34 neg1cn 12268 . . . . . . . . . . 11 -1 ∈ β„‚
35 neg1ne0 12270 . . . . . . . . . . 11 -1 β‰  0
36 eqid 2737 . . . . . . . . . . . 12 (mulGrpβ€˜β„‚fld) = (mulGrpβ€˜β„‚fld)
37 eqid 2737 . . . . . . . . . . . 12 ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})) = ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))
3836, 37expghm 20899 . . . . . . . . . . 11 ((-1 ∈ β„‚ ∧ -1 β‰  0) β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring GrpHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))))
3934, 35, 38mp2an 691 . . . . . . . . . 10 (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring GrpHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0})))
40 ghmmhm 19019 . . . . . . . . . 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 20822 . . . . . . . . . 10 β„‚fld ∈ Ring
43 cnfldbas 20803 . . . . . . . . . . . 12 β„‚ = (Baseβ€˜β„‚fld)
44 cnfld0 20824 . . . . . . . . . . . 12 0 = (0gβ€˜β„‚fld)
45 cndrng 20829 . . . . . . . . . . . 12 β„‚fld ∈ DivRing
4643, 44, 45drngui 20192 . . . . . . . . . . 11 (β„‚ βˆ– {0}) = (Unitβ€˜β„‚fld)
4746, 36unitsubm 20100 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
4842, 47ax-mp 5 . . . . . . . . 9 (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))
4937resmhm2 18633 . . . . . . . . 9 (((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs (β„‚ βˆ– {0}))) ∧ (β„‚ βˆ– {0}) ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))) β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)))
5041, 48, 49mp2an 691 . . . . . . . 8 (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld))
51 zsubrg 20853 . . . . . . . . . 10 β„€ ∈ (SubRingβ€˜β„‚fld)
5236subrgsubm 20238 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
5351, 52ax-mp 5 . . . . . . . . 9 β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld))
5429fmpttd 7064 . . . . . . . . . 10 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)):β„€βŸΆβ„€)
5554frnd 6677 . . . . . . . . 9 (πœ‘ β†’ ran (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) βŠ† β„€)
56 eqid 2737 . . . . . . . . . 10 ((mulGrpβ€˜β„‚fld) β†Ύs β„€) = ((mulGrpβ€˜β„‚fld) β†Ύs β„€)
5756resmhm2b 18634 . . . . . . . . 9 ((β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)) ∧ ran (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) βŠ† β„€) β†’ ((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)) ↔ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))))
5853, 55, 57sylancr 588 . . . . . . . 8 (πœ‘ β†’ ((π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom (mulGrpβ€˜β„‚fld)) ↔ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))))
5950, 58mpbii 232 . . . . . . 7 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€)))
60 mhmco 18635 . . . . . . 7 ((𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺) ∧ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜)) ∈ (β„€ring MndHom ((mulGrpβ€˜β„‚fld) β†Ύs β„€))) β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
6133, 59, 60syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝐿 ∘ (π‘˜ ∈ β„€ ↦ (-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
6230, 61eqeltrrd 2839 . . . . 5 (πœ‘ β†’ (π‘˜ ∈ β„€ ↦ (πΏβ€˜(-1β†‘π‘˜))) ∈ (β„€ring MndHom 𝐺))
63 lgseisen.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ (β„™ βˆ– {2}))
6463gausslemma2dlem0a 26707 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ β„•)
6564nnred 12169 . . . . . . . . 9 (πœ‘ β†’ 𝑄 ∈ ℝ)
666gausslemma2dlem0a 26707 . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ β„•)
6765, 66nndivred 12208 . . . . . . . 8 (πœ‘ β†’ (𝑄 / 𝑃) ∈ ℝ)
6867adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 / 𝑃) ∈ ℝ)
69 2nn 12227 . . . . . . . . 9 2 ∈ β„•
70 elfznn 13471 . . . . . . . . . 10 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) β†’ π‘₯ ∈ β„•)
7170adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ π‘₯ ∈ β„•)
72 nnmulcl 12178 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘₯ ∈ β„•) β†’ (2 Β· π‘₯) ∈ β„•)
7369, 71, 72sylancr 588 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„•)
7473nnred 12169 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ ℝ)
7568, 74remulcld 11186 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 / 𝑃) Β· (2 Β· π‘₯)) ∈ ℝ)
7675flcld 13704 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)
77 eqid 2737 . . . . . 6 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
78 fvexd 6858 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ V)
79 c0ex 11150 . . . . . . 7 0 ∈ V
8079a1i 11 . . . . . 6 (πœ‘ β†’ 0 ∈ V)
8177, 19, 78, 80fsuppmptdm 9317 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) finSupp 0)
82 oveq2 7366 . . . . . 6 (π‘˜ = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) β†’ (-1β†‘π‘˜) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
8382fveq2d 6847 . . . . 5 (π‘˜ = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) β†’ (πΏβ€˜(-1β†‘π‘˜)) = (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
84 oveq2 7366 . . . . . 6 (π‘˜ = (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) β†’ (-1β†‘π‘˜) = (-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
8584fveq2d 6847 . . . . 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 19717 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
8714, 25mgpbas 19903 . . . . . . 7 (Baseβ€˜π‘Œ) = (Baseβ€˜πΊ)
88 eqid 2737 . . . . . . . 8 (.rβ€˜π‘Œ) = (.rβ€˜π‘Œ)
8914, 88mgpplusg 19901 . . . . . . 7 (.rβ€˜π‘Œ) = (+gβ€˜πΊ)
9027adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘Œ))
91 m1expcl 13993 . . . . . . . . 9 ((βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€ β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
9276, 91syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
9390, 92ffvelcdmd 7037 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ∈ (Baseβ€˜π‘Œ))
94 neg1z 12540 . . . . . . . . . 10 -1 ∈ β„€
95 lgseisen.4 . . . . . . . . . . 11 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃)
9663eldifad 3923 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑄 ∈ β„™)
9796adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„™)
98 prmz 16552 . . . . . . . . . . . . . 14 (𝑄 ∈ β„™ β†’ 𝑄 ∈ β„€)
9997, 98syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„€)
10073nnzd 12527 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„€)
10199, 100zmulcld 12614 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ β„€)
1027adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„™)
103 prmnn 16551 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
104102, 103syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„•)
105101, 104zmodcld 13798 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) ∈ β„•0)
10695, 105eqeltrid 2842 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 ∈ β„•0)
107 zexpcl 13983 . . . . . . . . . 10 ((-1 ∈ β„€ ∧ 𝑅 ∈ β„•0) β†’ (-1↑𝑅) ∈ β„€)
10894, 106, 107sylancr 588 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑅) ∈ β„€)
109108, 99zmulcld 12614 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑𝑅) Β· 𝑄) ∈ β„€)
11090, 109ffvelcdmd 7037 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑𝑅) Β· 𝑄)) ∈ (Baseβ€˜π‘Œ))
111 eqid 2737 . . . . . . 7 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
112 eqid 2737 . . . . . . 7 (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))
11387, 89, 16, 19, 93, 110, 111, 112gsummptfidmadd2 19704 . . . . . 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 2738 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
115 eqidd 2738 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))
11619, 93, 110, 114, 115offval2 7638 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄)))))
11724adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝐿 ∈ (β„€ring RingHom π‘Œ))
118 zringmulr 20881 . . . . . . . . . . . 12 Β· = (.rβ€˜β„€ring)
1191, 118, 88rhmmul 20160 . . . . . . . . . . 11 ((𝐿 ∈ (β„€ring RingHom π‘Œ) ∧ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€ ∧ ((-1↑𝑅) Β· 𝑄) ∈ β„€) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))))
120117, 92, 109, 119syl3anc 1372 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))))
121101zred 12608 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ ℝ)
122104nnrpd 12956 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ ℝ+)
123 modval 13777 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 Β· (2 Β· π‘₯)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
124121, 122, 123syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) mod 𝑃) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
12595, 124eqtrid 2789 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))))
12699zcnd 12609 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑄 ∈ β„‚)
12773nncnd 12170 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 Β· π‘₯) ∈ β„‚)
128104nncnd 12170 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„‚)
129104nnne0d 12204 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 β‰  0)
130126, 127, 128, 129div23d 11969 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) / 𝑃) = ((𝑄 / 𝑃) Β· (2 Β· π‘₯)))
131130fveq2d 6847 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)) = (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
132131oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃))) = (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
133132oveq2d 7374 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 Β· (2 Β· π‘₯)) / 𝑃)))) = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
134125, 133eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 = ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
135134oveq2d 7374 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅) = ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
136 prmz 16552 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
137102, 136syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑃 ∈ β„€)
138137, 76zmulcld 12614 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
139138zcnd 12609 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„‚)
140101zcnd 12609 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) ∈ β„‚)
141139, 140pncan3d 11516 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + ((𝑄 Β· (2 Β· π‘₯)) βˆ’ (𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (𝑄 Β· (2 Β· π‘₯)))
142 2cnd 12232 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 2 ∈ β„‚)
14371nncnd 12170 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ π‘₯ ∈ β„‚)
144126, 142, 143mul12d 11365 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· (2 Β· π‘₯)) = (2 Β· (𝑄 Β· π‘₯)))
145135, 141, 1443eqtrd 2781 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅) = (2 Β· (𝑄 Β· π‘₯)))
146145oveq2d 7374 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = (-1↑(2 Β· (𝑄 Β· π‘₯))))
14734a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -1 ∈ β„‚)
14835a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -1 β‰  0)
149106nn0zd 12526 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 𝑅 ∈ β„€)
150 expaddz 14013 . . . . . . . . . . . . . . . 16 (((-1 ∈ β„‚ ∧ -1 β‰  0) ∧ ((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€ ∧ 𝑅 ∈ β„€)) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)))
151147, 148, 138, 149, 150syl22anc 838 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)))
152 expmulz 14015 . . . . . . . . . . . . . . . . . 18 (((-1 ∈ β„‚ ∧ -1 β‰  0) ∧ (𝑃 ∈ β„€ ∧ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
153147, 148, 137, 76, 152syl22anc 838 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
154 1cnd 11151 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 1 ∈ β„‚)
155 eldifsni 4751 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ (β„™ βˆ– {2}) β†’ 𝑃 β‰  2)
1566, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑃 β‰  2)
157156necomd 3000 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 2 β‰  𝑃)
158157neneqd 2949 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ 2 = 𝑃)
159158adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ Β¬ 2 = 𝑃)
160 2z 12536 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ β„€
161 uzid 12779 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ β„€ β†’ 2 ∈ (β„€β‰₯β€˜2))
162160, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (β„€β‰₯β€˜2)
163 dvdsprm 16580 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ (β„€β‰₯β€˜2) ∧ 𝑃 ∈ β„™) β†’ (2 βˆ₯ 𝑃 ↔ 2 = 𝑃))
164162, 102, 163sylancr 588 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (2 βˆ₯ 𝑃 ↔ 2 = 𝑃))
165159, 164mtbird 325 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ Β¬ 2 βˆ₯ 𝑃)
166 oexpneg 16228 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ β„‚ ∧ 𝑃 ∈ β„• ∧ Β¬ 2 βˆ₯ 𝑃) β†’ (-1↑𝑃) = -(1↑𝑃))
167154, 104, 165, 166syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑃) = -(1↑𝑃))
168 1exp 13998 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ β„€ β†’ (1↑𝑃) = 1)
169137, 168syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1↑𝑃) = 1)
170169negeqd 11396 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ -(1↑𝑃) = -1)
171167, 170eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑃) = -1)
172171oveq1d 7373 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑𝑃)↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
173153, 172eqtrd 2777 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
174173oveq1d 7373 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) Β· (-1↑𝑅)) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)))
175151, 174eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑((𝑃 Β· (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) + 𝑅)) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)))
176 nnmulcl 12178 . . . . . . . . . . . . . . . . . 18 ((𝑄 ∈ β„• ∧ π‘₯ ∈ β„•) β†’ (𝑄 Β· π‘₯) ∈ β„•)
17764, 70, 176syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„•)
178177nnnn0d 12474 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„•0)
179 2nn0 12431 . . . . . . . . . . . . . . . . 17 2 ∈ β„•0
180179a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ 2 ∈ β„•0)
181147, 178, 180expmuld 14055 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(2 Β· (𝑄 Β· π‘₯))) = ((-1↑2)↑(𝑄 Β· π‘₯)))
182 neg1sqe1 14101 . . . . . . . . . . . . . . . . 17 (-1↑2) = 1
183182oveq1i 7368 . . . . . . . . . . . . . . . 16 ((-1↑2)↑(𝑄 Β· π‘₯)) = (1↑(𝑄 Β· π‘₯))
184177nnzd 12527 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (𝑄 Β· π‘₯) ∈ β„€)
185 1exp 13998 . . . . . . . . . . . . . . . . 17 ((𝑄 Β· π‘₯) ∈ β„€ β†’ (1↑(𝑄 Β· π‘₯)) = 1)
186184, 185syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1↑(𝑄 Β· π‘₯)) = 1)
187183, 186eqtrid 2789 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑2)↑(𝑄 Β· π‘₯)) = 1)
188181, 187eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(2 Β· (𝑄 Β· π‘₯))) = 1)
189146, 175, 1883eqtr3d 2785 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) = 1)
190189oveq1d 7373 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) Β· 𝑄) = (1 Β· 𝑄))
19192zcnd 12609 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„‚)
192108zcnd 12609 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (-1↑𝑅) ∈ β„‚)
193191, 192, 126mulassd 11179 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· (-1↑𝑅)) Β· 𝑄) = ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄)))
194126mulid2d 11174 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (1 Β· 𝑄) = 𝑄)
195190, 193, 1943eqtr3d 2785 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄)) = 𝑄)
196195fveq2d 6847 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜((-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) Β· ((-1↑𝑅) Β· 𝑄))) = (πΏβ€˜π‘„))
197120, 196eqtr3d 2779 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄))) = (πΏβ€˜π‘„))
198197mpteq2dva 5206 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ ((πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))(.rβ€˜π‘Œ)(πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„)))
199116, 198eqtrd 2777 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) ∘f (.rβ€˜π‘Œ)(π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„)))
200199oveq2d 7374 . . . . . 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 26728 . . . . . . 7 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄)))) = (1rβ€˜π‘Œ))
205204oveq2d 7374 . . . . . 6 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜((-1↑𝑅) Β· 𝑄))))) = ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)))
206113, 200, 2053eqtr3rd 2786 . . . . 5 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))))
207 eqid 2737 . . . . . . 7 (0gβ€˜πΊ) = (0gβ€˜πΊ)
20893fmpttd 7064 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))):(1...((𝑃 βˆ’ 1) / 2))⟢(Baseβ€˜π‘Œ))
209 fvexd 6858 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) ∈ V)
210 fvexd 6858 . . . . . . . 8 (πœ‘ β†’ (0gβ€˜πΊ) ∈ V)
211111, 19, 209, 210fsuppmptdm 9317 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) finSupp (0gβ€˜πΊ))
21287, 207, 16, 19, 208, 211gsumcl 19693 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) ∈ (Baseβ€˜π‘Œ))
213 eqid 2737 . . . . . . 7 (1rβ€˜π‘Œ) = (1rβ€˜π‘Œ)
21425, 88, 213ringridm 19994 . . . . . 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 585 . . . . 5 (πœ‘ β†’ ((𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))(.rβ€˜π‘Œ)(1rβ€˜π‘Œ)) = (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))))
21696, 98syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑄 ∈ β„€)
21727, 216ffvelcdmd 7037 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜π‘„) ∈ (Baseβ€˜π‘Œ))
218 eqid 2737 . . . . . . . 8 (.gβ€˜πΊ) = (.gβ€˜πΊ)
21987, 218gsumconst 19712 . . . . . . 7 ((𝐺 ∈ Mnd ∧ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin ∧ (πΏβ€˜π‘„) ∈ (Baseβ€˜π‘Œ)) β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)))
22018, 19, 217, 219syl3anc 1372 . . . . . 6 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)))
221 oddprm 16683 . . . . . . . . . 10 (𝑃 ∈ (β„™ βˆ– {2}) β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
2226, 221syl 17 . . . . . . . . 9 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
223222nnnn0d 12474 . . . . . . . 8 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•0)
224 hashfz1 14247 . . . . . . . 8 (((𝑃 βˆ’ 1) / 2) ∈ β„•0 β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
225223, 224syl 17 . . . . . . 7 (πœ‘ β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
226225oveq1d 7373 . . . . . 6 (πœ‘ β†’ ((β™―β€˜(1...((𝑃 βˆ’ 1) / 2)))(.gβ€˜πΊ)(πΏβ€˜π‘„)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
22731, 1mgpbas 19903 . . . . . . . . 9 β„€ = (Baseβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))
228 eqid 2737 . . . . . . . . 9 (.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€)) = (.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))
229227, 228, 218mhmmulg 18918 . . . . . . . 8 ((𝐿 ∈ (((mulGrpβ€˜β„‚fld) β†Ύs β„€) MndHom 𝐺) ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0 ∧ 𝑄 ∈ β„€) β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
23033, 223, 216, 229syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)))
23153a1i 11 . . . . . . . . . 10 (πœ‘ β†’ β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)))
232 eqid 2737 . . . . . . . . . . 11 (.gβ€˜(mulGrpβ€˜β„‚fld)) = (.gβ€˜(mulGrpβ€˜β„‚fld))
233232, 56, 228submmulg 18921 . . . . . . . . . 10 ((β„€ ∈ (SubMndβ€˜(mulGrpβ€˜β„‚fld)) ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0 ∧ 𝑄 ∈ β„€) β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄))
234231, 223, 216, 233syl3anc 1372 . . . . . . . . 9 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄))
235216zcnd 12609 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ β„‚)
236 cnfldexp 20833 . . . . . . . . . 10 ((𝑄 ∈ β„‚ ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0) β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
237235, 223, 236syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜(mulGrpβ€˜β„‚fld))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
238234, 237eqtr3d 2779 . . . . . . . 8 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄) = (𝑄↑((𝑃 βˆ’ 1) / 2)))
239238fveq2d 6847 . . . . . . 7 (πœ‘ β†’ (πΏβ€˜(((𝑃 βˆ’ 1) / 2)(.gβ€˜((mulGrpβ€˜β„‚fld) β†Ύs β„€))𝑄)) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
240230, 239eqtr3d 2779 . . . . . 6 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2)(.gβ€˜πΊ)(πΏβ€˜π‘„)) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
241220, 226, 2403eqtrd 2781 . . . . 5 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜π‘„))) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
242206, 215, 2413eqtr3d 2785 . . . 4 (πœ‘ β†’ (𝐺 Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(-1↑(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))))
243 subrgsubg 20231 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubGrpβ€˜β„‚fld))
24451, 243ax-mp 5 . . . . . . . . 9 β„€ ∈ (SubGrpβ€˜β„‚fld)
245 subgsubm 18951 . . . . . . . . 9 (β„€ ∈ (SubGrpβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜β„‚fld))
246244, 245mp1i 13 . . . . . . . 8 (πœ‘ β†’ β„€ ∈ (SubMndβ€˜β„‚fld))
24776fmpttd 7064 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))):(1...((𝑃 βˆ’ 1) / 2))βŸΆβ„€)
248 df-zring 20873 . . . . . . . 8 β„€ring = (β„‚fld β†Ύs β„€)
24919, 246, 247, 248gsumsubm 18646 . . . . . . 7 (πœ‘ β†’ (β„‚fld Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25076zcnd 12609 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))) β†’ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„‚)
25119, 250gsumfsum 20867 . . . . . . 7 (πœ‘ β†’ (β„‚fld Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
252249, 251eqtr3d 2779 . . . . . 6 (πœ‘ β†’ (β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))) = Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))
253252oveq2d 7374 . . . . 5 (πœ‘ β†’ (-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))) = (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))
254253fveq2d 6847 . . . 4 (πœ‘ β†’ (πΏβ€˜(-1↑(β„€ring Ξ£g (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25586, 242, 2543eqtr3d 2785 . . 3 (πœ‘ β†’ (πΏβ€˜(𝑄↑((𝑃 βˆ’ 1) / 2))) = (πΏβ€˜(-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))))))
25666nnnn0d 12474 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„•0)
257 zexpcl 13983 . . . . 5 ((𝑄 ∈ β„€ ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0) β†’ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€)
258216, 223, 257syl2anc 585 . . . 4 (πœ‘ β†’ (𝑄↑((𝑃 βˆ’ 1) / 2)) ∈ β„€)
25919, 76fsumzcl 15621 . . . . 5 (πœ‘ β†’ Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€)
260 m1expcl 13993 . . . . 5 (Ξ£π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯))) ∈ β„€ β†’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
261259, 260syl 17 . . . 4 (πœ‘ β†’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) ∈ β„€)
2628, 22zndvds 20959 . . . 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 1372 . . 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 16148 . . 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 1372 . 2 (πœ‘ β†’ (((𝑄↑((𝑃 βˆ’ 1) / 2)) mod 𝑃) = ((-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))) mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑄↑((𝑃 βˆ’ 1) / 2)) βˆ’ (-1↑Σπ‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2))(βŒŠβ€˜((𝑄 / 𝑃) Β· (2 Β· π‘₯)))))))
267264, 266mpbird 257 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 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  Vcvv 3446   βˆ– cdif 3908   βŠ† wss 3911  {csn 4587   class class class wbr 5106   ↦ cmpt 5189  ran crn 5635   ∘ ccom 5638  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358   ∘f cof 7616  Fincfn 8884  β„‚cc 11050  β„cr 11051  0cc0 11052  1c1 11053   + caddc 11055   Β· cmul 11057   βˆ’ cmin 11386  -cneg 11387   / cdiv 11813  β„•cn 12154  2c2 12209  β„•0cn0 12414  β„€cz 12500  β„€β‰₯cuz 12764  β„+crp 12916  ...cfz 13425  βŒŠcfl 13696   mod cmo 13775  β†‘cexp 13968  β™―chash 14231  Ξ£csu 15571   βˆ₯ cdvds 16137  β„™cprime 16548  Basecbs 17084   β†Ύs cress 17113  .rcmulr 17135  0gc0g 17322   Ξ£g cgsu 17323  Mndcmnd 18557   MndHom cmhm 18600  SubMndcsubmnd 18601  .gcmg 18873  SubGrpcsubg 18923   GrpHom cghm 19006  CMndccmn 19563  Abelcabl 19564  mulGrpcmgp 19897  1rcur 19914  Ringcrg 19965  CRingccrg 19966   RingHom crh 20144  DivRingcdr 20186  Fieldcfield 20187  SubRingcsubrg 20221  β„‚fldccnfld 20799  β„€ringczring 20872  β„€RHomczrh 20903  β„€/nβ„€czn 20906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130  ax-addf 11131  ax-mulf 11132
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8649  df-ec 8651  df-qs 8655  df-map 8768  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fsupp 9307  df-sup 9379  df-inf 9380  df-oi 9447  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12765  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-clim 15371  df-sum 15572  df-dvds 16138  df-gcd 16376  df-prm 16549  df-struct 17020  df-sets 17037  df-slot 17055  df-ndx 17067  df-base 17085  df-ress 17114  df-plusg 17147  df-mulr 17148  df-starv 17149  df-sca 17150  df-vsca 17151  df-ip 17152  df-tset 17153  df-ple 17154  df-ds 17156  df-unif 17157  df-0g 17324  df-gsum 17325  df-imas 17391  df-qus 17392  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-mhm 18602  df-submnd 18603  df-grp 18752  df-minusg 18753  df-sbg 18754  df-mulg 18874  df-subg 18926  df-nsg 18927  df-eqg 18928  df-ghm 19007  df-cntz 19098  df-cmn 19565  df-abl 19566  df-mgp 19898  df-ur 19915  df-ring 19967  df-cring 19968  df-oppr 20050  df-dvdsr 20071  df-unit 20072  df-invr 20102  df-dvr 20113  df-rnghom 20147  df-drng 20188  df-field 20189  df-subrg 20223  df-lmod 20327  df-lss 20396  df-lsp 20436  df-sra 20636  df-rgmod 20637  df-lidl 20638  df-rsp 20639  df-2idl 20705  df-nzr 20731  df-rlreg 20756  df-domn 20757  df-idom 20758  df-cnfld 20800  df-zring 20873  df-zrh 20907  df-zn 20910
This theorem is referenced by:  lgseisen  26730
  Copyright terms: Public domain W3C validator