Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
2 | 1 | eldifad 3552 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ ℙ) |
3 | | prmz 15227 |
. . . 4
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝑄 ∈ ℤ) |
5 | | lgseisen.1 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
6 | | lgsval3 24840 |
. . 3
⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑄
/L 𝑃) =
((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
7 | 4, 5, 6 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑄 /L 𝑃) = ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)) |
8 | | prmnn 15226 |
. . . . . . . . 9
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
9 | 2, 8 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ ℕ) |
10 | | oddprm 15353 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
11 | 5, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
12 | 11 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
13 | 9, 12 | nnexpcld 12892 |
. . . . . . 7
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℕ) |
14 | 13 | nnred 10912 |
. . . . . 6
⊢ (𝜑 → (𝑄↑((𝑃 − 1) / 2)) ∈
ℝ) |
15 | | neg1rr 11002 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ∈
ℝ) |
17 | | neg1ne0 11003 |
. . . . . . . 8
⊢ -1 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ≠
0) |
19 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
20 | 9 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℝ) |
21 | 5 | eldifad 3552 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
22 | | prmnn 15226 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℕ) |
24 | 20, 23 | nndivred 10946 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ) |
25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 / 𝑃) ∈ ℝ) |
26 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
27 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ) |
29 | 28 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ) |
30 | | remulcl 9900 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑥
∈ ℝ) → (2 · 𝑥) ∈ ℝ) |
31 | 26, 29, 30 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈
ℝ) |
32 | 25, 31 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 / 𝑃) · (2 · 𝑥)) ∈ ℝ) |
33 | 32 | flcld 12461 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...((𝑃 − 1) / 2))) →
(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈
ℤ) |
34 | 19, 33 | fsumzcl 14313 |
. . . . . . 7
⊢ (𝜑 → Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) |
35 | 16, 18, 34 | reexpclzd 12896 |
. . . . . 6
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℝ) |
36 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
38 | 23 | nnrpd 11746 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
39 | | lgseisen.3 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
40 | | eqid 2610 |
. . . . . . 7
⊢ ((𝑄 · (2 · 𝑥)) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃) |
41 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
((((-1↑((𝑄 · (2
· 𝑥)) mod 𝑃)) · ((𝑄 · (2 · 𝑥)) mod 𝑃)) mod 𝑃) / 2)) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦
((((-1↑((𝑄 · (2
· 𝑥)) mod 𝑃)) · ((𝑄 · (2 · 𝑥)) mod 𝑃)) mod 𝑃) / 2)) |
42 | | eqid 2610 |
. . . . . . 7
⊢ ((𝑄 · (2 · 𝑦)) mod 𝑃) = ((𝑄 · (2 · 𝑦)) mod 𝑃) |
43 | | eqid 2610 |
. . . . . . 7
⊢
(ℤ/nℤ‘𝑃) = (ℤ/nℤ‘𝑃) |
44 | | eqid 2610 |
. . . . . . 7
⊢
(mulGrp‘(ℤ/nℤ‘𝑃)) =
(mulGrp‘(ℤ/nℤ‘𝑃)) |
45 | | eqid 2610 |
. . . . . . 7
⊢
(ℤRHom‘(ℤ/nℤ‘𝑃)) =
(ℤRHom‘(ℤ/nℤ‘𝑃)) |
46 | 5, 1, 39, 40, 41, 42, 43, 44, 45 | lgseisenlem4 24903 |
. . . . . 6
⊢ (𝜑 → ((𝑄↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) mod 𝑃)) |
47 | | modadd1 12569 |
. . . . . 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 𝑃)) |
48 | 14, 35, 37, 38, 46, 47 | syl221anc 1329 |
. . . . 5
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃)) |
49 | | peano2re 10088 |
. . . . . . 7
⊢
((-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℝ →
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) + 1) ∈
ℝ) |
50 | 35, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) ∈ ℝ) |
51 | | df-neg 10148 |
. . . . . . . 8
⊢ -1 = (0
− 1) |
52 | | neg1cn 11001 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -1 ∈
ℂ) |
54 | | absexpz 13893 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))) ∈ ℤ) →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
55 | 53, 18, 34, 54 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = ((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
56 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
57 | 56 | absnegi 13987 |
. . . . . . . . . . . . . . 15
⊢
(abs‘-1) = (abs‘1) |
58 | | abs1 13885 |
. . . . . . . . . . . . . . 15
⊢
(abs‘1) = 1 |
59 | 57, 58 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢
(abs‘-1) = 1 |
60 | 59 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢
((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = (1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) |
61 | | 1exp 12751 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))) ∈ ℤ →
(1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) = 1) |
62 | 34, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = 1) |
63 | 60, 62 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((abs‘-1)↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) = 1) |
64 | 55, 63 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) = 1) |
65 | | 1le1 10534 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
66 | 64, 65 | syl6eqbr 4622 |
. . . . . . . . . 10
⊢ (𝜑 →
(abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ≤ 1) |
67 | | absle 13903 |
. . . . . . . . . . 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))) |
68 | 35, 36, 67 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 →
((abs‘(-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) ≤ 1 ↔ (-1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ≤
1))) |
69 | 66, 68 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (-1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∧
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ≤
1)) |
70 | 69 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → -1 ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))) |
71 | 51, 70 | syl5eqbrr 4619 |
. . . . . . 7
⊢ (𝜑 → (0 − 1) ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥))))) |
72 | | 0red 9920 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
73 | 72, 37, 35 | lesubaddd 10503 |
. . . . . . 7
⊢ (𝜑 → ((0 − 1) ≤
(-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ↔ 0 ≤
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) +
1))) |
74 | 71, 73 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → 0 ≤
((-1↑Σ𝑥 ∈
(1...((𝑃 − 1) /
2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) +
1)) |
75 | 23 | nnred 10912 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℝ) |
76 | | peano2rem 10227 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
78 | 69 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ≤ 1) |
79 | | df-2 10956 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
80 | | eldifsni 4261 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
81 | 5, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ≠ 2) |
82 | 26 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ) |
83 | | prmuz2 15246 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
84 | | eluzle 11576 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
85 | 21, 83, 84 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≤ 𝑃) |
86 | 82, 75, 85 | leltned 10069 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 < 𝑃 ↔ 𝑃 ≠ 2)) |
87 | 81, 86 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → 2 < 𝑃) |
88 | 79, 87 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ (𝜑 → (1 + 1) < 𝑃) |
89 | 37, 37, 75 | ltaddsubd 10506 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + 1) < 𝑃 ↔ 1 < (𝑃 − 1))) |
90 | 88, 89 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → 1 < (𝑃 − 1)) |
91 | 35, 37, 77, 78, 90 | lelttrd 10074 |
. . . . . . 7
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) < (𝑃 − 1)) |
92 | 35, 37, 75 | ltaddsubd 10506 |
. . . . . . 7
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) < 𝑃 ↔ (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) < (𝑃 − 1))) |
93 | 91, 92 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) < 𝑃) |
94 | | modid 12557 |
. . . . . 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)) |
95 | 50, 38, 74, 93, 94 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1)) |
96 | 48, 95 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = ((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1)) |
97 | 96 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1)) |
98 | 35 | recnd 9947 |
. . . 4
⊢ (𝜑 → (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) ∈ ℂ) |
99 | | pncan 10166 |
. . . 4
⊢
(((-1↑Σ𝑥
∈ (1...((𝑃 − 1)
/ 2))(⌊‘((𝑄 /
𝑃) · (2 ·
𝑥)))) ∈ ℂ ∧
1 ∈ ℂ) → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
100 | 98, 56, 99 | sylancl 693 |
. . 3
⊢ (𝜑 → (((-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥)))) + 1) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
101 | 97, 100 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((((𝑄↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |
102 | 7, 101 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑥 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑥))))) |