Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
2 | 1 | eldifad 3878 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ ℙ) |
3 | | prmz 16232 |
. . . 4
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝑄 ∈ ℤ) |
5 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
6 | | lgsval3 26196 |
. . 3
⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑄
/L 𝑃) =
((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
7 | 4, 5, 6 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
8 | 1 | gausslemma2dlem0a 26237 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℕ) |
9 | | oddprm 16363 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
10 | 5, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
11 | 10 | nnnn0d 12150 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
12 | 8, 11 | nnexpcld 13812 |
. . . . . . 7
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℕ) |
13 | 12 | nnred 11845 |
. . . . . 6
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℝ) |
14 | | neg1rr 11945 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ∈
ℝ) |
16 | | neg1ne0 11946 |
. . . . . . . 8
⊢ -1 ≠
0 |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ≠
0) |
18 | | fzfid 13546 |
. . . . . . . 8
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
19 | 8 | nnred 11845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℝ) |
20 | 5 | gausslemma2dlem0a 26237 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℕ) |
21 | 19, 20 | nndivred 11884 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
22 | 21 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ) |
23 | | 2re 11904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
24 | | elfznn 13141 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
25 | 24 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
26 | 25 | nnred 11845 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ) |
27 | | remulcl 10814 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑥
∈ ℝ) → (2 · 𝑥) ∈ ℝ) |
28 | 23, 26, 27 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℝ) |
29 | 22, 28 | remulcld 10863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ) |
30 | 29 | flcld 13373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℤ) |
31 | 18, 30 | fsumzcl 15299 |
. . . . . . 7
⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) |
32 | 15, 17, 31 | reexpclzd 13816 |
. . . . . 6
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℝ) |
33 | | 1re 10833 |
. . . . . . 7
⊢ 1 ∈
ℝ |
34 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
35 | 20 | nnrpd 12626 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
36 | | lgseisen.3 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
37 | | eqid 2737 |
. . . . . . 7
⊢ ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃) |
38 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
((((-1↑((𝑄 · (2
· 𝑥)) mod 𝑃)) · ((𝑄 · (2 · 𝑥)) mod 𝑃)) mod 𝑃) / 2)) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
((((-1↑((𝑄 · (2
· 𝑥)) mod 𝑃)) · ((𝑄 · (2 · 𝑥)) mod 𝑃)) mod 𝑃) / 2)) |
39 | | eqid 2737 |
. . . . . . 7
⊢ ((𝑄 · (2 · 𝑦)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃) |
40 | | eqid 2737 |
. . . . . . 7
⊢
(ℤ/nℤ‘𝑃) = (ℤ/nℤ‘𝑃) |
41 | | eqid 2737 |
. . . . . . 7
⊢
(mulGrp‘(ℤ/nℤ‘𝑃)) =
(mulGrp‘(ℤ/nℤ‘𝑃)) |
42 | | eqid 2737 |
. . . . . . 7
⊢
(ℤRHom‘(ℤ/nℤ‘𝑃)) =
(ℤRHom‘(ℤ/nℤ‘𝑃)) |
43 | 5, 1, 36, 37, 38, 39, 40, 41, 42 | lgseisenlem4 26259 |
. . . . . 6
⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) |
44 | | modadd1 13481 |
. . . . . 6
⊢ ((((𝑄↑((𝑃 − 1) / 2)) ∈ ℝ ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℝ) ∧
(1 ∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) → (((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃)) |
45 | 13, 32, 34, 35, 43, 44 | syl221anc 1383 |
. . . . 5
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃)) |
46 | | peano2re 11005 |
. . . . . . 7
⊢
((-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℝ →
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) + 1) ∈
ℝ) |
47 | 32, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) ∈ ℝ) |
48 | | df-neg 11065 |
. . . . . . . 8
⊢ -1 = (0
− 1) |
49 | | neg1cn 11944 |
. . . . . . . . . . . . 13
⊢ -1 ∈
ℂ |
50 | | absexpz 14869 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
51 | 49, 16, 31, 50 | mp3an12i 1467 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
52 | | ax-1cn 10787 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
53 | 52 | absnegi 14964 |
. . . . . . . . . . . . . . 15
⊢
(abs‘-1) = (abs‘1) |
54 | | abs1 14861 |
. . . . . . . . . . . . . . 15
⊢
(abs‘1) = 1 |
55 | 53, 54 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢
(abs‘-1) = 1 |
56 | 55 | oveq1i 7223 |
. . . . . . . . . . . . 13
⊢
((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
57 | | 1exp 13664 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))) ∈ ℤ →
(1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) = 1) |
58 | 31, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = 1) |
59 | 56, 58 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = 1) |
60 | 51, 59 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = 1) |
61 | | 1le1 11460 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
62 | 60, 61 | eqbrtrdi 5092 |
. . . . . . . . . 10
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ≤ 1) |
63 | | absle 14879 |
. . . . . . . . . . 11
⊢
(((-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℝ ∧
1 ∈ ℝ) → ((abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ≤ 1 ↔ (-1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ≤
1))) |
64 | 32, 33, 63 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 →
((abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ≤ 1 ↔ (-1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ≤
1))) |
65 | 62, 64 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (-1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ≤
1)) |
66 | 65 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → -1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))) |
67 | 48, 66 | eqbrtrrid 5089 |
. . . . . . 7
⊢ (𝜑 → (0 − 1) ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))) |
68 | | 0red 10836 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
69 | 68, 34, 32 | lesubaddd 11429 |
. . . . . . 7
⊢ (𝜑 → ((0 − 1) ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ↔ 0 ≤
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) +
1))) |
70 | 67, 69 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → 0 ≤
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) +
1)) |
71 | 20 | nnred 11845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℝ) |
72 | | peano2rem 11145 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
73 | 71, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
74 | 65 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ≤ 1) |
75 | | df-2 11893 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
76 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
77 | 5 | eldifad 3878 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
78 | | prmuz2 16253 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
79 | | eluzle 12451 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
80 | 77, 78, 79 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝑃) |
81 | | eldifsni 4703 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
82 | 5, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ≠ 2) |
83 | 76, 71, 80, 82 | leneltd 10986 |
. . . . . . . . . 10
⊢ (𝜑 → 2 < 𝑃) |
84 | 75, 83 | eqbrtrrid 5089 |
. . . . . . . . 9
⊢ (𝜑 → (1 + 1) < 𝑃) |
85 | 34, 34, 71 | ltaddsubd 11432 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + 1) < 𝑃 ↔ 1 < (𝑃 − 1))) |
86 | 84, 85 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → 1 < (𝑃 − 1)) |
87 | 32, 34, 73, 74, 86 | lelttrd 10990 |
. . . . . . 7
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) < (𝑃 − 1)) |
88 | 32, 34, 71 | ltaddsubd 11432 |
. . . . . . 7
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) < 𝑃 ↔ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) < (𝑃 − 1))) |
89 | 87, 88 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) < 𝑃) |
90 | | modid 13469 |
. . . . . 6
⊢
(((((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) ∧ ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) < 𝑃)) → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1)) |
91 | 47, 35, 70, 89, 90 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1)) |
92 | 45, 91 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1)) |
93 | 92 | oveq1d 7228 |
. . 3
⊢ (𝜑 → ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1)) |
94 | 32 | recnd 10861 |
. . . 4
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ) |
95 | | pncan 11084 |
. . . 4
⊢
(((-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℂ ∧
1 ∈ ℂ) → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
96 | 94, 52, 95 | sylancl 589 |
. . 3
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
97 | 93, 96 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
98 | 7, 97 | eqtrd 2777 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |