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 26041 |
. 2
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1) |
7 | | eldifi 4028 |
. . . . . . 7
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
8 | | prmnn 16055 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
9 | 8 | nnred 11674 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
10 | | prmgt1 16078 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
11 | 9, 10 | jca 516 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 <
𝑃)) |
12 | 1, 7, 11 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∈ ℝ ∧ 1 < 𝑃)) |
13 | | 1mod 13305 |
. . . . . 6
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → (1 mod 𝑃) = 1) |
15 | 14 | eqcomd 2765 |
. . . 4
⊢ (𝜑 → 1 = (1 mod 𝑃)) |
16 | 15 | eqeq2d 2770 |
. . 3
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 ↔ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃))) |
17 | | neg1z 12042 |
. . . . . . . . . . 11
⊢ -1 ∈
ℤ |
18 | 1, 4, 2, 5 | gausslemma2dlem0h 26031 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
19 | | zexpcl 13479 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℤ ∧ 𝑁
∈ ℕ0) → (-1↑𝑁) ∈ ℤ) |
20 | 17, 18, 19 | sylancr 591 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑𝑁) ∈ ℤ) |
21 | | 2nn 11732 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℕ) |
23 | 1, 2 | gausslemma2dlem0b 26025 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ ℕ) |
24 | 23 | nnnn0d 11979 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈
ℕ0) |
25 | 22, 24 | nnexpcld 13641 |
. . . . . . . . . . 11
⊢ (𝜑 → (2↑𝐻) ∈ ℕ) |
26 | 25 | nnzd 12110 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝐻) ∈ ℤ) |
27 | 20, 26 | zmulcld 12117 |
. . . . . . . . 9
⊢ (𝜑 → ((-1↑𝑁) · (2↑𝐻)) ∈
ℤ) |
28 | 27 | zred 12111 |
. . . . . . . 8
⊢ (𝜑 → ((-1↑𝑁) · (2↑𝐻)) ∈
ℝ) |
29 | | 1red 10665 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
30 | 28, 29 | jca 516 |
. . . . . . 7
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈
ℝ)) |
31 | 30 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((-1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈
ℝ)) |
32 | 1 | gausslemma2dlem0a 26024 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
33 | 32 | nnrpd 12455 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
34 | 20, 33 | jca 516 |
. . . . . . 7
⊢ (𝜑 → ((-1↑𝑁) ∈ ℤ ∧ 𝑃 ∈
ℝ+)) |
35 | 34 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((-1↑𝑁) ∈ ℤ ∧ 𝑃 ∈
ℝ+)) |
36 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) |
37 | | modmul1 13326 |
. . . . . 6
⊢
(((((-1↑𝑁)
· (2↑𝐻)) ∈
ℝ ∧ 1 ∈ ℝ) ∧ ((-1↑𝑁) ∈ ℤ ∧ 𝑃 ∈ ℝ+) ∧
(((-1↑𝑁) ·
(2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃)) |
38 | 31, 35, 36, 37 | syl3anc 1369 |
. . . . 5
⊢ ((𝜑 ∧ (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃)) |
39 | 38 | ex 417 |
. . . 4
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃))) |
40 | 20 | zcnd 12112 |
. . . . . . . . 9
⊢ (𝜑 → (-1↑𝑁) ∈ ℂ) |
41 | 25 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐻) ∈ ℂ) |
42 | 40, 41, 40 | mul32d 10873 |
. . . . . . . 8
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) = (((-1↑𝑁) · (-1↑𝑁)) · (2↑𝐻))) |
43 | 18 | nn0cnd 11981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
44 | 43 | 2timesd 11902 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁)) |
45 | 44 | eqcomd 2765 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 𝑁) = (2 · 𝑁)) |
46 | 45 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 + 𝑁)) = (-1↑(2 · 𝑁))) |
47 | | neg1cn 11773 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℂ |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → -1 ∈
ℂ) |
49 | 48, 18, 18 | expaddd 13547 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) |
50 | 18 | nn0zd 12109 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
51 | | m1expeven 13511 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ →
(-1↑(2 · 𝑁)) =
1) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(2 · 𝑁)) = 1) |
53 | 46, 49, 52 | 3eqtr3d 2802 |
. . . . . . . . 9
⊢ (𝜑 → ((-1↑𝑁) · (-1↑𝑁)) = 1) |
54 | 53 | oveq1d 7158 |
. . . . . . . 8
⊢ (𝜑 → (((-1↑𝑁) · (-1↑𝑁)) · (2↑𝐻)) = (1 · (2↑𝐻))) |
55 | 41 | mulid2d 10682 |
. . . . . . . 8
⊢ (𝜑 → (1 · (2↑𝐻)) = (2↑𝐻)) |
56 | 42, 54, 55 | 3eqtrd 2798 |
. . . . . . 7
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) = (2↑𝐻)) |
57 | 56 | oveq1d 7158 |
. . . . . 6
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((2↑𝐻) mod 𝑃)) |
58 | 40 | mulid2d 10682 |
. . . . . . 7
⊢ (𝜑 → (1 · (-1↑𝑁)) = (-1↑𝑁)) |
59 | 58 | oveq1d 7158 |
. . . . . 6
⊢ (𝜑 → ((1 ·
(-1↑𝑁)) mod 𝑃) = ((-1↑𝑁) mod 𝑃)) |
60 | 57, 59 | eqeq12d 2775 |
. . . . 5
⊢ (𝜑 → (((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃) ↔ ((2↑𝐻) mod 𝑃) = ((-1↑𝑁) mod 𝑃))) |
61 | 2 | oveq2i 7154 |
. . . . . . . 8
⊢
(2↑𝐻) =
(2↑((𝑃 − 1) /
2)) |
62 | 61 | oveq1i 7153 |
. . . . . . 7
⊢
((2↑𝐻) mod
𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃) |
63 | 62 | eqeq1i 2764 |
. . . . . 6
⊢
(((2↑𝐻) mod
𝑃) = ((-1↑𝑁) mod 𝑃) ↔ ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃)) |
64 | | 2z 12038 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
65 | | lgsvalmod 25984 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝑃
∈ (ℙ ∖ {2})) → ((2 /L 𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)) |
66 | 64, 1, 65 | sylancr 591 |
. . . . . . . . 9
⊢ (𝜑 → ((2 /L
𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)) |
67 | 66 | eqcomd 2765 |
. . . . . . . 8
⊢ (𝜑 → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /L
𝑃) mod 𝑃)) |
68 | 67 | eqeq1d 2761 |
. . . . . . 7
⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃) ↔ ((2 /L 𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃))) |
69 | 1, 4, 2, 5 | gausslemma2dlem0i 26032 |
. . . . . . 7
⊢ (𝜑 → (((2 /L
𝑃) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
70 | 68, 69 | sylbid 243 |
. . . . . 6
⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
71 | 63, 70 | syl5bi 245 |
. . . . 5
⊢ (𝜑 → (((2↑𝐻) mod 𝑃) = ((-1↑𝑁) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
72 | 60, 71 | sylbid 243 |
. . . 4
⊢ (𝜑 → (((((-1↑𝑁) · (2↑𝐻)) · (-1↑𝑁)) mod 𝑃) = ((1 · (-1↑𝑁)) mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
73 | 39, 72 | syld 47 |
. . 3
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → (2 /L 𝑃) = (-1↑𝑁))) |
74 | 16, 73 | sylbid 243 |
. 2
⊢ (𝜑 → ((((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 → (2 /L 𝑃) = (-1↑𝑁))) |
75 | 6, 74 | mpd 15 |
1
⊢ (𝜑 → (2 /L
𝑃) = (-1↑𝑁)) |