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 ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 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 lgseisenlem4 ( 𝜑 → ( ( 𝑄 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( - 1 ↑ Σ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑥 ) ) ) ) mod 𝑃 ) )

Proof

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