Proof of Theorem gausslemma2dlem2
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
2 | | oveq1 5917 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
3 | 2 | breq1d 4039 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
4 | 2 | oveq2d 5926 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
5 | 3, 2, 4 | ifbieq12d 3583 |
. . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
6 | 5 | adantl 277 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
7 | | elfz1b 10146 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑀) ↔ (𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀)) |
8 | | nnre 8979 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
9 | 8 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑘 ∈
ℝ) |
10 | | nnre 8979 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
11 | 10 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℝ) |
12 | | 2re 9042 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
13 | | 2pos 9063 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
14 | 12, 13 | pm3.2i 272 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
15 | 14 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) |
16 | | lemul1 8602 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) |
17 | 9, 11, 15, 16 | syl3anc 1249 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) |
18 | | gausslemma2d.p |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
19 | | gausslemma2d.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
20 | 18, 19 | gausslemma2dlem0e 15111 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) |
21 | 20 | adantl 277 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (𝑀 · 2) < (𝑃 / 2)) |
22 | 12 | a1i 9 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) |
23 | 8, 22 | remulcld 8040 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 · 2) ∈
ℝ) |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) |
25 | 12 | a1i 9 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 2 ∈
ℝ) |
26 | 10, 25 | remulcld 8040 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑀 · 2) ∈
ℝ) |
27 | 26 | adantl 277 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑀 · 2) ∈
ℝ) |
28 | 18 | gausslemma2dlem0a 15107 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℕ) |
29 | 28 | nnred 8985 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℝ) |
30 | 29 | rehalfcld 9219 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 / 2) ∈ ℝ) |
31 | | lelttr 8098 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · 2) ∈ ℝ
∧ (𝑀 · 2) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → (((𝑘
· 2) ≤ (𝑀
· 2) ∧ (𝑀
· 2) < (𝑃 / 2))
→ (𝑘 · 2) <
(𝑃 / 2))) |
32 | 24, 27, 30, 31 | syl2an3an 1309 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (((𝑘 · 2) ≤ (𝑀 · 2) ∧ (𝑀 · 2) < (𝑃 / 2)) → (𝑘 · 2) < (𝑃 / 2))) |
33 | 21, 32 | mpan2d 428 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2))) |
34 | 33 | ex 115 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝜑 → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2)))) |
35 | 34 | com23 78 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) |
36 | 17, 35 | sylbid 150 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) |
37 | 36 | 3impia 1202 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) |
38 | 7, 37 | sylbi 121 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) |
39 | 38 | impcom 125 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) < (𝑃 / 2)) |
40 | 39 | adantr 276 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → (𝑘 · 2) < (𝑃 / 2)) |
41 | 40 | iftrued 3564 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑘 · 2)) |
42 | 6, 41 | eqtrd 2226 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑘 · 2)) |
43 | 18, 19 | gausslemma2dlem0d 15110 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
44 | 43 | nn0zd 9427 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
45 | | gausslemma2d.h |
. . . . . . . 8
⊢ 𝐻 = ((𝑃 − 1) / 2) |
46 | 18, 45 | gausslemma2dlem0b 15108 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℕ) |
47 | 46 | nnzd 9428 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) |
48 | 18, 19, 45 | gausslemma2dlem0g 15113 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐻) |
49 | | eluz2 9588 |
. . . . . 6
⊢ (𝐻 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻)) |
50 | 44, 47, 48, 49 | syl3anbrc 1183 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘𝑀)) |
51 | | fzss2 10120 |
. . . . 5
⊢ (𝐻 ∈
(ℤ≥‘𝑀) → (1...𝑀) ⊆ (1...𝐻)) |
52 | 50, 51 | syl 14 |
. . . 4
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝐻)) |
53 | 52 | sselda 3179 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝐻)) |
54 | 53 | elfzelzd 10082 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℤ) |
55 | | 2z 9335 |
. . . . 5
⊢ 2 ∈
ℤ |
56 | 55 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 2 ∈ ℤ) |
57 | 54, 56 | zmulcld 9435 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) ∈ ℤ) |
58 | 1, 42, 53, 57 | fvmptd2 5631 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) = (𝑘 · 2)) |
59 | 58 | ralrimiva 2567 |
1
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) |