Step | Hyp | Ref
| Expression |
1 | | zringbas 19643 |
. . . . 5
⊢ ℤ =
(Base‘ℤring) |
2 | | zring0 19647 |
. . . . 5
⊢ 0 =
(0g‘ℤring) |
3 | | zringabl 19641 |
. . . . . 6
⊢
ℤring ∈ Abel |
4 | | ablcmn 18022 |
. . . . . 6
⊢
(ℤring ∈ Abel → ℤring ∈
CMnd) |
5 | 3, 4 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ℤring
∈ CMnd) |
6 | | lgseisen.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
7 | 6 | eldifad 3552 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℙ) |
8 | | lgseisen.7 |
. . . . . . . . . 10
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
9 | 8 | znfld 19728 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Field) |
11 | | isfld 18579 |
. . . . . . . . 9
⊢ (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing)) |
12 | 11 | simprbi 479 |
. . . . . . . 8
⊢ (𝑌 ∈ Field → 𝑌 ∈ CRing) |
13 | 10, 12 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ CRing) |
14 | | lgseisen.8 |
. . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝑌) |
15 | 14 | crngmgp 18378 |
. . . . . . 7
⊢ (𝑌 ∈ CRing → 𝐺 ∈ CMnd) |
16 | 13, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ CMnd) |
17 | | cmnmnd 18031 |
. . . . . 6
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) |
19 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
20 | | m1expcl 12745 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ →
(-1↑𝑘) ∈
ℤ) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈
ℤ) |
22 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) = (𝑘 ∈ ℤ ↦ (-1↑𝑘))) |
23 | | crngring 18381 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
24 | 13, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ Ring) |
25 | | lgseisen.9 |
. . . . . . . . . . 11
⊢ 𝐿 = (ℤRHom‘𝑌) |
26 | 25 | zrhrhm 19679 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
27 | 24, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
28 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑌) =
(Base‘𝑌) |
29 | 1, 28 | rhmf 18549 |
. . . . . . . . 9
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
30 | 27, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
31 | 30 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝐿 = (𝑥 ∈ ℤ ↦ (𝐿‘𝑥))) |
32 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (-1↑𝑘) → (𝐿‘𝑥) = (𝐿‘(-1↑𝑘))) |
33 | 21, 22, 31, 32 | fmptco 6303 |
. . . . . 6
⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) = (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘)))) |
34 | | zringmpg 19659 |
. . . . . . . . 9
⊢
((mulGrp‘ℂfld) ↾s ℤ) =
(mulGrp‘ℤring) |
35 | 34, 14 | rhmmhm 18545 |
. . . . . . . 8
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺)) |
36 | 27, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺)) |
37 | | neg1cn 11001 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
38 | | neg1ne0 11003 |
. . . . . . . . . . 11
⊢ -1 ≠
0 |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
40 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
41 | 39, 40 | expghm 19663 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))) |
42 | 37, 38, 41 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) |
43 | | ghmmhm 17493 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring GrpHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})))) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) |
45 | | cnring 19587 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
46 | | cnfldbas 19571 |
. . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) |
47 | | cnfld0 19589 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
48 | | cndrng 19594 |
. . . . . . . . . . . 12
⊢
ℂfld ∈ DivRing |
49 | 46, 47, 48 | drngui 18576 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
50 | 49, 39 | unitsubm 18493 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) |
51 | 45, 50 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld)) |
52 | 40 | resmhm2 17183 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) ∧ (ℂ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℂfld))) → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom
(mulGrp‘ℂfld))) |
53 | 44, 51, 52 | mp2an 704 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom
(mulGrp‘ℂfld)) |
54 | | zsubrg 19618 |
. . . . . . . . . 10
⊢ ℤ
∈ (SubRing‘ℂfld) |
55 | 39 | subrgsubm 18616 |
. . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . 9
⊢ ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) |
57 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) = (𝑘 ∈ ℤ ↦
(-1↑𝑘)) |
58 | 21, 57 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)):ℤ⟶ℤ) |
59 | | frn 5966 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ↦
(-1↑𝑘)):ℤ⟶ℤ → ran (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ⊆
ℤ) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ⊆
ℤ) |
61 | | eqid 2610 |
. . . . . . . . . 10
⊢
((mulGrp‘ℂfld) ↾s ℤ) =
((mulGrp‘ℂfld) ↾s
ℤ) |
62 | 61 | resmhm2b 17184 |
. . . . . . . . 9
⊢ ((ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ran (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ⊆
ℤ) → ((𝑘 ∈
ℤ ↦ (-1↑𝑘)) ∈ (ℤring MndHom
(mulGrp‘ℂfld)) ↔ (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ)))) |
63 | 56, 60, 62 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom (mulGrp‘ℂfld)) ↔
(𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ)))) |
64 | 53, 63 | mpbii 222 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ))) |
65 | | mhmco 17185 |
. . . . . . 7
⊢ ((𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺) ∧ (𝑘 ∈ ℤ ↦
(-1↑𝑘)) ∈
(ℤring MndHom ((mulGrp‘ℂfld)
↾s ℤ))) → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈
(ℤring MndHom 𝐺)) |
66 | 36, 64, 65 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐿 ∘ (𝑘 ∈ ℤ ↦ (-1↑𝑘))) ∈
(ℤring MndHom 𝐺)) |
67 | 33, 66 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℤ ↦ (𝐿‘(-1↑𝑘))) ∈ (ℤring MndHom
𝐺)) |
68 | | lgseisen.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
69 | 68 | eldifad 3552 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℙ) |
70 | | prmnn 15226 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℕ) |
72 | 71 | nnred 10912 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℝ) |
73 | | prmnn 15226 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
74 | 7, 73 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
75 | 72, 74 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
76 | 75 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ) |
77 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
78 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
79 | 78 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
80 | | nnmulcl 10920 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑥
∈ ℕ) → (2 · 𝑥) ∈ ℕ) |
81 | 77, 79, 80 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℕ) |
82 | 81 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℝ) |
83 | 76, 82 | remulcld 9949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ) |
84 | 83 | flcld 12461 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℤ) |
85 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
86 | | fvex 6113 |
. . . . . . 7
⊢
(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))) ∈
V |
87 | 86 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ V) |
88 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
89 | 88 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
V) |
90 | 85, 19, 87, 89 | fsuppmptdm 8169 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) finSupp 0) |
91 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (-1↑𝑘) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
92 | 91 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
93 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (-1↑𝑘) =
(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) |
94 | 93 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) → (𝐿‘(-1↑𝑘)) = (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) |
95 | 1, 2, 5, 18, 19, 67, 84, 90, 92, 94 | gsummhm2 18162 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) |
96 | 14, 28 | mgpbas 18318 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝐺) |
97 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑌) = (.r‘𝑌) |
98 | 14, 97 | mgpplusg 18316 |
. . . . . . 7
⊢
(.r‘𝑌) = (+g‘𝐺) |
99 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
100 | | m1expcl 12745 |
. . . . . . . . 9
⊢
((⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥))) ∈ ℤ →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℤ) |
101 | 84, 100 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℤ) |
102 | 99, 101 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ (Base‘𝑌)) |
103 | | neg1z 11290 |
. . . . . . . . . 10
⊢ -1 ∈
ℤ |
104 | | lgseisen.4 |
. . . . . . . . . . 11
⊢ 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃) |
105 | 69 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ) |
106 | | prmz 15227 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ) |
108 | 81 | nnzd 11357 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℤ) |
109 | 107, 108 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ) |
110 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
111 | 110, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
112 | 109, 111 | zmodcld 12553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈
ℕ0) |
113 | 104, 112 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈
ℕ0) |
114 | | zexpcl 12737 |
. . . . . . . . . 10
⊢ ((-1
∈ ℤ ∧ 𝑅
∈ ℕ0) → (-1↑𝑅) ∈ ℤ) |
115 | 103, 113,
114 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℤ) |
116 | 115, 107 | zmulcld 11364 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ) |
117 | 99, 116 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌)) |
118 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
119 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) |
120 | 96, 98, 16, 19, 102, 117, 118, 119 | gsummptfidmadd2 18149 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))) |
121 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) |
122 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) |
123 | 19, 102, 117, 121, 122 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))))) |
124 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom
𝑌)) |
125 | | zringmulr 19646 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℤring) |
126 | 1, 125, 97 | rhmmul 18550 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑌) ∧
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈ ℤ ∧
((-1↑𝑅) · 𝑄) ∈ ℤ) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) |
127 | 124, 101,
116, 126 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) |
128 | 109 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ) |
129 | 111 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈
ℝ+) |
130 | | modval 12532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((𝑄 · (2
· 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) |
131 | 128, 129,
130 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) |
132 | 104, 131 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))))) |
133 | 107 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ) |
134 | 81 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℂ) |
135 | 111 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℂ) |
136 | 111 | nnne0d 10942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ≠ 0) |
137 | 133, 134,
135, 136 | div23d 10717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑥))) |
138 | 137 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 ·
(2 · 𝑥)) / 𝑃)) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
139 | 138 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃))) = (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 · (2 · 𝑥)) / 𝑃)))) = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
141 | 132, 140 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 = ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
142 | 141 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) |
143 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
144 | 110, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
145 | 144, 84 | zmulcld 11364 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) |
146 | 145 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ) |
147 | 109 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℂ) |
148 | 146, 147 | pncan3d 10274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + ((𝑄 · (2 · 𝑥)) − (𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (𝑄 · (2 · 𝑥))) |
149 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℂ) |
150 | 79 | nncnd 10913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℂ) |
151 | 133, 149,
150 | mul12d 10124 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) = (2 · (𝑄 · 𝑥))) |
152 | 142, 148,
151 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅) = (2 · (𝑄 · 𝑥))) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = (-1↑(2 · (𝑄 · 𝑥)))) |
154 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ∈
ℂ) |
155 | 38 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -1 ≠
0) |
156 | 113 | nn0zd 11356 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ) |
157 | | expaddz 12766 |
. . . . . . . . . . . . . . . 16
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ ∧ 𝑅 ∈ ℤ)) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅))) |
158 | 154, 155,
145, 156, 157 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅))) |
159 | | expmulz 12768 |
. . . . . . . . . . . . . . . . . 18
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (𝑃 ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ)) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
160 | 154, 155,
144, 84, 159 | syl22anc 1319 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
161 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 1 ∈
ℂ) |
162 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
163 | 6, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑃 ≠ 2) |
164 | 163 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 2 ≠ 𝑃) |
165 | 164 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 2 = 𝑃) |
166 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 = 𝑃) |
167 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℤ |
168 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
169 | 167, 168 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
(ℤ≥‘2) |
170 | | dvdsprm 15253 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
171 | 169, 110,
170 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
172 | 166, 171 | mtbird 314 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 2 ∥
𝑃) |
173 | | oexpneg 14907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ 𝑃
∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (-1↑𝑃) = -(1↑𝑃)) |
174 | 161, 111,
172, 173 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -(1↑𝑃)) |
175 | | 1exp 12751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ →
(1↑𝑃) =
1) |
176 | 144, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑𝑃) = 1) |
177 | 176 | negeqd 10154 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → -(1↑𝑃) = -1) |
178 | 174, 177 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑃) = -1) |
179 | 178 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑃)↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
180 | 160, 179 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
181 | 180 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑(𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) · (-1↑𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅))) |
182 | 158, 181 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑((𝑃 · (⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 𝑅)) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅))) |
183 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (𝑄 · 𝑥) ∈ ℕ) |
184 | 71, 78, 183 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℕ) |
185 | 184 | nnnn0d 11228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈
ℕ0) |
186 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ0 |
187 | 186 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) |
188 | 154, 185,
187 | expmuld 12873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2
· (𝑄 · 𝑥))) = ((-1↑2)↑(𝑄 · 𝑥))) |
189 | | neg1sqe1 12821 |
. . . . . . . . . . . . . . . . 17
⊢
(-1↑2) = 1 |
190 | 189 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢
((-1↑2)↑(𝑄
· 𝑥)) =
(1↑(𝑄 · 𝑥)) |
191 | 184 | nnzd 11357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · 𝑥) ∈ ℤ) |
192 | | 1exp 12751 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑄 · 𝑥) ∈ ℤ → (1↑(𝑄 · 𝑥)) = 1) |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1↑(𝑄 · 𝑥)) = 1) |
194 | 190, 193 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑2)↑(𝑄
· 𝑥)) =
1) |
195 | 188, 194 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑(2
· (𝑄 · 𝑥))) = 1) |
196 | 153, 182,
195 | 3eqtr3d 2652 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) = 1) |
197 | 196 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = (1 · 𝑄)) |
198 | 101 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(-1↑(⌊‘((𝑄
/ 𝑃) · (2 ·
𝑥)))) ∈
ℂ) |
199 | 115 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈
ℂ) |
200 | 198, 199,
133 | mulassd 9942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · (-1↑𝑅)) · 𝑄) = ((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) |
201 | 133 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (1 · 𝑄) = 𝑄) |
202 | 197, 200,
201 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄)) = 𝑄) |
203 | 202 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) · ((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄)) |
204 | 127, 203 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄))) = (𝐿‘𝑄)) |
205 | 204 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))(.r‘𝑌)(𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) |
206 | 123, 205 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) |
207 | 206 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) ∘𝑓
(.r‘𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))) |
208 | | lgseisen.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
209 | | lgseisen.5 |
. . . . . . . 8
⊢ 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) |
210 | | lgseisen.6 |
. . . . . . . 8
⊢ 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃) |
211 | 6, 68, 208, 104, 209, 210, 8, 14, 25 | lgseisenlem3 24902 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r‘𝑌)) |
212 | 211 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌))) |
213 | 120, 207,
212 | 3eqtr3rd 2653 |
. . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄)))) |
214 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
215 | 102, 118 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌)) |
216 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ V |
217 | 216 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ∈ V) |
218 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝐺) ∈ V |
219 | 218 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
220 | 118, 19, 217, 219 | fsuppmptdm 8169 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) finSupp (0g‘𝐺)) |
221 | 96, 214, 16, 19, 215, 220 | gsumcl 18139 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) |
222 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑌) = (1r‘𝑌) |
223 | 28, 97, 222 | ringridm 18395 |
. . . . . 6
⊢ ((𝑌 ∈ Ring ∧ (𝐺 Σg
(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) ∈ (Base‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) |
224 | 24, 221, 223 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))(.r‘𝑌)(1r‘𝑌)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))))) |
225 | 69, 106 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℤ) |
226 | 30, 225 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘𝑄) ∈ (Base‘𝑌)) |
227 | | eqid 2610 |
. . . . . . . 8
⊢
(.g‘𝐺) = (.g‘𝐺) |
228 | 96, 227 | gsumconst 18157 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (1...((𝑃 − 1) / 2)) ∈ Fin
∧ (𝐿‘𝑄) ∈ (Base‘𝑌)) → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((#‘(1...((𝑃 − 1) / 2)))(.g‘𝐺)(𝐿‘𝑄))) |
229 | 18, 19, 226, 228 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = ((#‘(1...((𝑃 − 1) / 2)))(.g‘𝐺)(𝐿‘𝑄))) |
230 | | oddprm 15353 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
231 | 6, 230 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
232 | 231 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
233 | | hashfz1 12996 |
. . . . . . . 8
⊢ (((𝑃 − 1) / 2) ∈
ℕ0 → (#‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2)) |
234 | 232, 233 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) /
2)) |
235 | 234 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((#‘(1...((𝑃 − 1) /
2)))(.g‘𝐺)(𝐿‘𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) |
236 | 34, 1 | mgpbas 18318 |
. . . . . . . . 9
⊢ ℤ =
(Base‘((mulGrp‘ℂfld) ↾s
ℤ)) |
237 | | eqid 2610 |
. . . . . . . . 9
⊢
(.g‘((mulGrp‘ℂfld)
↾s ℤ)) =
(.g‘((mulGrp‘ℂfld) ↾s
ℤ)) |
238 | 236, 237,
227 | mhmmulg 17406 |
. . . . . . . 8
⊢ ((𝐿 ∈
(((mulGrp‘ℂfld) ↾s ℤ) MndHom
𝐺) ∧ ((𝑃 − 1) / 2) ∈
ℕ0 ∧ 𝑄
∈ ℤ) → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) |
239 | 36, 232, 225, 238 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄))) |
240 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) |
241 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
242 | 241, 61, 237 | submmulg 17409 |
. . . . . . . . . 10
⊢ ((ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ ((𝑃 − 1) / 2) ∈
ℕ0 ∧ 𝑄
∈ ℤ) → (((𝑃
− 1) / 2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) |
243 | 240, 232,
225, 242 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) |
244 | 225 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℂ) |
245 | | cnfldexp 19598 |
. . . . . . . . . 10
⊢ ((𝑄 ∈ ℂ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2))) |
246 | 244, 232,
245 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘(mulGrp‘ℂfld))𝑄) = (𝑄↑((𝑃 − 1) / 2))) |
247 | 243, 246 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄) = (𝑄↑((𝑃 − 1) / 2))) |
248 | 247 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘(((𝑃 − 1) /
2)(.g‘((mulGrp‘ℂfld)
↾s ℤ))𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) |
249 | 239, 248 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (((𝑃 − 1) / 2)(.g‘𝐺)(𝐿‘𝑄)) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) |
250 | 229, 235,
249 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘𝑄))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) |
251 | 213, 224,
250 | 3eqtr3d 2652 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(-1↑(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(𝑄↑((𝑃 − 1) / 2)))) |
252 | | subrgsubg 18609 |
. . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubGrp‘ℂfld)) |
253 | 54, 252 | ax-mp 5 |
. . . . . . . . 9
⊢ ℤ
∈ (SubGrp‘ℂfld) |
254 | | subgsubm 17439 |
. . . . . . . . 9
⊢ (ℤ
∈ (SubGrp‘ℂfld) → ℤ ∈
(SubMnd‘ℂfld)) |
255 | 253, 254 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ℤ ∈
(SubMnd‘ℂfld)) |
256 | 84, 85 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))):(1...((𝑃 − 1) /
2))⟶ℤ) |
257 | | df-zring 19638 |
. . . . . . . 8
⊢
ℤring = (ℂfld ↾s
ℤ) |
258 | 19, 255, 256, 257 | gsumsubm 17196 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
259 | 84 | zcnd 11359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℂ) |
260 | 19, 259 | gsumfsum 19632 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
261 | 258, 260 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
262 | 261 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 →
(-1↑(ℤring Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
263 | 262 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝐿‘(-1↑(ℤring
Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
264 | 95, 251, 263 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))))) |
265 | 74 | nnnn0d 11228 |
. . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
266 | | zexpcl 12737 |
. . . . 5
⊢ ((𝑄 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝑄↑((𝑃 − 1) / 2)) ∈
ℤ) |
267 | 225, 232,
266 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℤ) |
268 | 19, 84 | fsumzcl 14313 |
. . . . 5
⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) |
269 | | m1expcl 12745 |
. . . . 5
⊢
(Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))) ∈ ℤ →
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈
ℤ) |
270 | 268, 269 | syl 17 |
. . . 4
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℤ) |
271 | 8, 25 | zndvds 19717 |
. . . 4
⊢ ((𝑃 ∈ ℕ0
∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ
∧ (-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℤ)
→ ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) |
272 | 265, 267,
270, 271 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝐿‘(𝑄↑((𝑃 − 1) / 2))) = (𝐿‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) |
273 | 264, 272 | mpbid 221 |
. 2
⊢ (𝜑 → 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))))) |
274 | | moddvds 14829 |
. . 3
⊢ ((𝑃 ∈ ℕ ∧ (𝑄↑((𝑃 − 1) / 2)) ∈ ℤ ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℤ)
→ (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) |
275 | 74, 267, 270, 274 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃) ↔ 𝑃 ∥ ((𝑄↑((𝑃 − 1) / 2)) −
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))))) |
276 | 273, 275 | mpbird 246 |
1
⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) |