Proof of Theorem gausslemma2d
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | gausslemma2d.h |
. . 3
⊢ 𝐻 = ((𝑃 − 1) / 2) |
3 | | gausslemma2d.r |
. . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | | gausslemma2d.m |
. . 3
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
5 | | gausslemma2d.n |
. . 3
⊢ 𝑁 = (𝐻 − 𝑀) |
6 | 1, 2, 3, 4, 5 | gausslemma2dlem7 15112 |
. 2
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1) |
7 | 1 | gausslemma2dlem0a 15093 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
8 | | nnq 9684 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
9 | 7, 8 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℚ) |
10 | | eldifi 3277 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
11 | | prmgt1 12244 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
12 | 1, 10, 11 | 3syl 17 |
. . . . . 6
⊢ (𝜑 → 1 < 𝑃) |
13 | | q1mod 10413 |
. . . . . 6
⊢ ((𝑃 ∈ ℚ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
14 | 9, 12, 13 | syl2anc 411 |
. . . . 5
⊢ (𝜑 → (1 mod 𝑃) = 1) |
15 | 14 | eqcomd 2195 |
. . . 4
⊢ (𝜑 → 1 = (1 mod 𝑃)) |
16 | 15 | eqeq2d 2201 |
. . 3
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 ↔ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃))) |
17 | | neg1z 9335 |
. . . . . . . . . 10
⊢ -1 ∈
ℤ |
18 | 1, 4, 2, 5 | gausslemma2dlem0h 15100 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
19 | | zexpcl 10599 |
. . . . . . . . . 10
⊢ ((-1
∈ ℤ ∧ 𝑁
∈ ℕ0) → (-1↑𝑁) ∈ ℤ) |
20 | 17, 18, 19 | sylancr 414 |
. . . . . . . . 9
⊢ (𝜑 → (-1↑𝑁) ∈ ℤ) |
21 | | 2nn 9129 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
22 | 21 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℕ) |
23 | 1, 2 | gausslemma2dlem0b 15094 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ ℕ) |
24 | 23 | nnnn0d 9279 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈
ℕ0) |
25 | 22, 24 | nnexpcld 10740 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝐻) ∈ ℕ) |
26 | 25 | nnzd 9424 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐻) ∈ ℤ) |
27 | 20, 26 | zmulcld 9431 |
. . . . . . . 8
⊢ (𝜑 → ((-1↑𝑁) · (2↑𝐻)) ∈
ℤ) |
28 | | zq 9677 |
. . . . . . . 8
⊢
(((-1↑𝑁)
· (2↑𝐻)) ∈
ℤ → ((-1↑𝑁)
· (2↑𝐻)) ∈
ℚ) |
29 | 27, 28 | syl 14 |
. . . . . . 7
⊢ (𝜑 → ((-1↑𝑁) · (2↑𝐻)) ∈
ℚ) |
30 | 29 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((-1↑𝑁) · (2↑𝐻)) ∈ ℚ) |
31 | | 1z 9329 |
. . . . . . 7
⊢ 1 ∈
ℤ |
32 | | zq 9677 |
. . . . . . 7
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
33 | 31, 32 | mp1i 10 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → 1 ∈ ℚ) |
34 | 20 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (-1↑𝑁) ∈ ℤ) |
35 | 9 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → 𝑃 ∈ ℚ) |
36 | 7 | nngt0d 9012 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑃) |
37 | 36 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → 0 < 𝑃) |
38 | | simpr 110 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) |
39 | 30, 33, 34, 35, 37, 38 | modqmul1 10434 |
. . . . 5
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃)) |
40 | 39 | ex 115 |
. . . 4
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃))) |
41 | 20 | zcnd 9426 |
. . . . . . . . 9
⊢ (𝜑 → (-1↑𝑁) ∈ ℂ) |
42 | 25 | nncnd 8982 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐻) ∈ ℂ) |
43 | 41, 42, 41 | mul32d 8158 |
. . . . . . . 8
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) = (((-1↑𝑁) · (-1↑𝑁)) · (2↑𝐻))) |
44 | 18 | nn0cnd 9281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
45 | 44 | 2timesd 9211 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁)) |
46 | 45 | eqcomd 2195 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 𝑁) = (2 · 𝑁)) |
47 | 46 | oveq2d 5922 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 + 𝑁)) = (-1↑(2 · 𝑁))) |
48 | | neg1cn 9073 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℂ |
49 | 48 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → -1 ∈
ℂ) |
50 | 49, 18, 18 | expaddd 10720 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) |
51 | 18 | nn0zd 9423 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
52 | | m1expeven 10631 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ →
(-1↑(2 · 𝑁)) =
1) |
53 | 51, 52 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(2 · 𝑁)) = 1) |
54 | 47, 50, 53 | 3eqtr3d 2230 |
. . . . . . . . 9
⊢ (𝜑 → ((-1↑𝑁) · (-1↑𝑁)) = 1) |
55 | 54 | oveq1d 5921 |
. . . . . . . 8
⊢ (𝜑 → (((-1↑𝑁) · (-1↑𝑁)) · (2↑𝐻)) = (1 · (2↑𝐻))) |
56 | 42 | mullidd 8023 |
. . . . . . . 8
⊢ (𝜑 → (1 · (2↑𝐻)) = (2↑𝐻)) |
57 | 43, 55, 56 | 3eqtrd 2226 |
. . . . . . 7
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) = (2↑𝐻)) |
58 | 57 | oveq1d 5921 |
. . . . . 6
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((2↑𝐻) mod 𝑃)) |
59 | 41 | mullidd 8023 |
. . . . . . 7
⊢ (𝜑 → (1 · (-1↑𝑁)) = (-1↑𝑁)) |
60 | 59 | oveq1d 5921 |
. . . . . 6
⊢ (𝜑 → ((1 ·
(-1↑𝑁)) mod 𝑃) = ((-1↑𝑁) mod 𝑃)) |
61 | 58, 60 | eqeq12d 2204 |
. . . . 5
⊢ (𝜑 → (((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃) ↔ ((2↑𝐻) mod 𝑃) = ((-1↑𝑁) mod 𝑃))) |
62 | 2 | oveq2i 5917 |
. . . . . . . 8
⊢
(2↑𝐻) =
(2↑((𝑃 − 1) /
2)) |
63 | 62 | oveq1i 5916 |
. . . . . . 7
⊢
((2↑𝐻) mod
𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃) |
64 | 63 | eqeq1i 2197 |
. . . . . 6
⊢
(((2↑𝐻) mod
𝑃) = ((-1↑𝑁) mod 𝑃) ↔ ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃)) |
65 | | 2z 9331 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
66 | | lgsvalmod 15063 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝑃
∈ (ℙ ∖ {2})) → ((2 /L 𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)) |
67 | 65, 1, 66 | sylancr 414 |
. . . . . . . . 9
⊢ (𝜑 → ((2 /L
𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)) |
68 | 67 | eqcomd 2195 |
. . . . . . . 8
⊢ (𝜑 → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /L
𝑃) mod 𝑃)) |
69 | 68 | eqeq1d 2198 |
. . . . . . 7
⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃) ↔ ((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃))) |
70 | 1, 4, 2, 5 | gausslemma2dlem0i 15101 |
. . . . . . 7
⊢ (𝜑 → (((2 /L
𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
71 | 69, 70 | sylbid 150 |
. . . . . 6
⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
72 | 64, 71 | biimtrid 152 |
. . . . 5
⊢ (𝜑 → (((2↑𝐻) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
73 | 61, 72 | sylbid 150 |
. . . 4
⊢ (𝜑 → (((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
74 | 40, 73 | syld 45 |
. . 3
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
75 | 16, 74 | sylbid 150 |
. 2
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 → (2 /L 𝑃) = (-1↑𝑁))) |
76 | 6, 75 | mpd 13 |
1
⊢ (𝜑 → (2 /L
𝑃) = (-1↑𝑁)) |