Proof of Theorem gausslemma2dlem2
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . . 4
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
3 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
4 | 3 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
5 | 3 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
6 | 4, 3, 5 | ifbieq12d 4113 |
. . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
7 | 6 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
8 | | elfz1b 12409 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑀) ↔ (𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀)) |
9 | | nnre 11027 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
10 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑘 ∈
ℝ) |
11 | | nnre 11027 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
12 | 11 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℝ) |
13 | | 2re 11090 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
14 | | 2pos 11112 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
15 | 13, 14 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) |
17 | | lemul1 10875 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) |
18 | 10, 12, 16, 17 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) |
19 | | gausslemma2d.p |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
20 | | gausslemma2d.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
21 | 19, 20 | gausslemma2dlem0e 25085 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) |
22 | 21 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (𝑀 · 2) < (𝑃 / 2)) |
23 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) |
24 | 9, 23 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 · 2) ∈
ℝ) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) |
26 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 2 ∈
ℝ) |
27 | 11, 26 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑀 · 2) ∈
ℝ) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑀 · 2) ∈
ℝ) |
29 | 19 | gausslemma2dlem0a 25081 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℕ) |
30 | 29 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℝ) |
31 | 30 | rehalfcld 11279 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 / 2) ∈ ℝ) |
32 | | lelttr 10128 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · 2) ∈ ℝ
∧ (𝑀 · 2) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → (((𝑘
· 2) ≤ (𝑀
· 2) ∧ (𝑀
· 2) < (𝑃 / 2))
→ (𝑘 · 2) <
(𝑃 / 2))) |
33 | 25, 28, 31, 32 | syl2an3an 1386 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (((𝑘 · 2) ≤ (𝑀 · 2) ∧ (𝑀 · 2) < (𝑃 / 2)) → (𝑘 · 2) < (𝑃 / 2))) |
34 | 22, 33 | mpan2d 710 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2))) |
35 | 34 | ex 450 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝜑 → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2)))) |
36 | 35 | com23 86 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) |
37 | 18, 36 | sylbid 230 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) |
38 | 37 | 3impia 1261 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) |
39 | 8, 38 | sylbi 207 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) |
40 | 39 | impcom 446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) < (𝑃 / 2)) |
41 | 40 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → (𝑘 · 2) < (𝑃 / 2)) |
42 | 41 | iftrued 4094 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑘 · 2)) |
43 | 7, 42 | eqtrd 2656 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑘 · 2)) |
44 | 19, 20 | gausslemma2dlem0d 25084 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
45 | 44 | nn0zd 11480 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
46 | | gausslemma2d.h |
. . . . . . . 8
⊢ 𝐻 = ((𝑃 − 1) / 2) |
47 | 19, 46 | gausslemma2dlem0b 25082 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℕ) |
48 | 47 | nnzd 11481 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) |
49 | 19, 20, 46 | gausslemma2dlem0g 25087 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐻) |
50 | | eluz2 11693 |
. . . . . 6
⊢ (𝐻 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻)) |
51 | 45, 48, 49, 50 | syl3anbrc 1246 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘𝑀)) |
52 | | fzss2 12381 |
. . . . 5
⊢ (𝐻 ∈
(ℤ≥‘𝑀) → (1...𝑀) ⊆ (1...𝐻)) |
53 | 51, 52 | syl 17 |
. . . 4
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝐻)) |
54 | 53 | sselda 3603 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝐻)) |
55 | | ovexd 6680 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) ∈ V) |
56 | 2, 43, 54, 55 | fvmptd 6288 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) = (𝑘 · 2)) |
57 | 56 | ralrimiva 2966 |
1
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) |