Proof of Theorem gausslemma2dlem3
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 6808 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
4 | 3 | breq1d 4802 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
5 | 3 | oveq2d 6817 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
6 | 4, 3, 5 | ifbieq12d 4245 |
. . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
7 | 6 | adantl 473 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
8 | | gausslemma2d.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
9 | 8 | gausslemma2dlem0a 25251 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
10 | | elfz2 12497 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻))) |
11 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
12 | 11 | oveq1i 6811 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 + 1) = ((⌊‘(𝑃 / 4)) + 1) |
13 | 12 | breq1i 4799 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 + 1) ≤ 𝑘 ↔ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) |
14 | | nnre 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
15 | | 4re 11260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 4 ∈
ℝ) |
17 | | 4ne0 11280 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 4 ≠
0) |
19 | 14, 16, 18 | redivcld 11016 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 4) ∈
ℝ) |
20 | 19 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 4) ∈
ℝ) |
21 | | fllelt 12763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 / 4) ∈ ℝ →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
23 | 19 | flcld 12764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℤ) |
24 | 23 | zred 11645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℝ) |
25 | | peano2re 10372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((⌊‘(𝑃 /
4)) ∈ ℝ → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℕ →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
27 | 26 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
28 | | zre 11544 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
29 | 28 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → 𝑘 ∈
ℝ) |
30 | | ltleletr 10293 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 / 4) ∈ ℝ ∧
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ ∧ 𝑘
∈ ℝ) → (((𝑃
/ 4) < ((⌊‘(𝑃 / 4)) + 1) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘)) |
31 | 20, 27, 29, 30 | syl3anc 1463 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) ∧ ((⌊‘(𝑃
/ 4)) + 1) ≤ 𝑘) →
(𝑃 / 4) ≤ 𝑘)) |
32 | 31 | expd 451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))) |
33 | 32 | adantld 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
(((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1)) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))) |
34 | 22, 33 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘)) |
35 | 34 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘) |
36 | 14 | rehalfcld 11442 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
37 | 36 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
38 | | 2re 11253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℤ → 2 ∈
ℝ) |
40 | 28, 39 | remulcld 10233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → (𝑘 · 2) ∈
ℝ) |
41 | 40 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) |
42 | | 2pos 11275 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
43 | 38, 42 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) |
45 | | lediv1 11051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
46 | 37, 41, 44, 45 | syl3anc 1463 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
47 | | nncn 11191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
48 | | 2cnne0 11405 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
50 | | divdiv1 10899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2))) |
51 | 47, 49, 49, 50 | syl3anc 1463 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2))) |
52 | | 2t2e4 11340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 2) = 4 |
53 | 52 | oveq2i 6812 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 / (2 · 2)) = (𝑃 / 4) |
54 | 51, 53 | syl6eq 2798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / 4)) |
55 | | zcn 11545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
56 | | 2cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 ∈
ℂ) |
57 | | 2ne0 11276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ≠
0 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 ≠
0) |
59 | 55, 56, 58 | divcan4d 10970 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) / 2) = 𝑘) |
60 | 54, 59 | breqan12rd 4809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
61 | 46, 60 | bitrd 268 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
62 | 61 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
63 | 35, 62 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → (𝑃 / 2) ≤ (𝑘 · 2)) |
64 | 63 | exp31 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (𝑃 ∈ ℕ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 / 2) ≤ (𝑘 · 2)))) |
65 | 64 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
66 | 13, 65 | syl5bi 232 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
67 | 66 | 3ad2ant3 1127 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
68 | 67 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) ≤ 𝑘 → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
69 | 68 | adantr 472 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻) → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
70 | 69 | impcom 445 |
. . . . . . . . . 10
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻)) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
71 | 10, 70 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
72 | 71 | impcom 445 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 / 2) ≤ (𝑘 · 2)) |
73 | | elfzelz 12506 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
74 | 73 | zred 11645 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℝ) |
75 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℝ) |
76 | 74, 75 | remulcld 10233 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℝ) |
77 | | lenlt 10279 |
. . . . . . . . 9
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑘 · 2) ↔
¬ (𝑘 · 2) <
(𝑃 / 2))) |
78 | 36, 76, 77 | syl2an 495 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ¬ (𝑘 · 2) < (𝑃 / 2))) |
79 | 72, 78 | mpbid 222 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
80 | 9, 79 | sylan 489 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
81 | 80 | adantr 472 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
82 | 81 | iffalsed 4229 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑃 − (𝑘 · 2))) |
83 | 7, 82 | eqtrd 2782 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑘 · 2))) |
84 | 8, 11 | gausslemma2dlem0d 25254 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
85 | | nn0p1nn 11495 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
86 | | nnuz 11887 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
87 | 85, 86 | syl6eleq 2837 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
(ℤ≥‘1)) |
88 | 84, 87 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
89 | | fzss1 12544 |
. . . . 5
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
90 | 88, 89 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
91 | 90 | sselda 3732 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ (1...𝐻)) |
92 | | ovexd 6831 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈ V) |
93 | 2, 83, 91, 92 | fvmptd 6438 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
94 | 93 | ralrimiva 3092 |
1
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |