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 6556 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) |
4 | 3 | breq1d 4593 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) |
5 | 3 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) |
6 | 4, 3, 5 | ifbieq12d 4063 |
. . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
7 | 6 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) |
8 | | gausslemma2d.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
9 | 8 | gausslemma2dlem0a 24881 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
10 | | elfz2 12204 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻))) |
11 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
12 | 11 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 + 1) = ((⌊‘(𝑃 / 4)) + 1) |
13 | 12 | breq1i 4590 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 + 1) ≤ 𝑘 ↔ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) |
14 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
15 | | 4re 10974 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 4 ∈
ℝ) |
17 | | 4ne0 10994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 4 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 4 ≠
0) |
19 | 14, 16, 18 | redivcld 10732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 4) ∈
ℝ) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 4) ∈
ℝ) |
21 | | fllelt 12460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 / 4) ∈ ℝ →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4))
≤ (𝑃 / 4) ∧ (𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1))) |
23 | 19 | flcld 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℤ) |
24 | 23 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ →
(⌊‘(𝑃 / 4))
∈ ℝ) |
25 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((⌊‘(𝑃 /
4)) ∈ ℝ → ((⌊‘(𝑃 / 4)) + 1) ∈ ℝ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℕ →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ) |
28 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → 𝑘 ∈
ℝ) |
30 | | ltleletr 10009 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 / 4) ∈ ℝ ∧
((⌊‘(𝑃 / 4)) +
1) ∈ ℝ ∧ 𝑘
∈ ℝ) → (((𝑃
/ 4) < ((⌊‘(𝑃 / 4)) + 1) ∧ ((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘) → (𝑃 / 4) ≤ 𝑘)) |
31 | 20, 27, 29, 30 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) ∧ ((⌊‘(𝑃
/ 4)) + 1) ≤ 𝑘) →
(𝑃 / 4) ≤ 𝑘)) |
32 | 31 | expd 451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 4) <
((⌊‘(𝑃 / 4)) +
1) → (((⌊‘(𝑃 / 4)) + 1) ≤ 𝑘 → (𝑃 / 4) ≤ 𝑘))) |
33 | 32 | adantld 482 |
. . . . . . . . . . . . . . . . . . . 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 11156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑃 / 2) ∈
ℝ) |
38 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℤ → 2 ∈
ℝ) |
40 | 28, 39 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → (𝑘 · 2) ∈
ℝ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) |
42 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
43 | 38, 42 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) |
45 | | lediv1 10767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
46 | 37, 41, 44, 45 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2))) |
47 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
48 | | 2cnne0 11119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
50 | | divdiv1 10615 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2))) |
51 | 47, 49, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / (2 · 2))) |
52 | | 2t2e4 11054 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 2) = 4 |
53 | 52 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 / (2 · 2)) = (𝑃 / 4) |
54 | 51, 53 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → ((𝑃 / 2) / 2) = (𝑃 / 4)) |
55 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
56 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 ∈
ℂ) |
57 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ≠
0 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ → 2 ≠
0) |
59 | 55, 56, 58 | divcan4d 10686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℤ → ((𝑘 · 2) / 2) = 𝑘) |
60 | 54, 59 | breqan12rd 4600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (((𝑃 / 2) / 2) ≤ ((𝑘 · 2) / 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
61 | 46, 60 | bitrd 267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ (𝑃 / 4) ≤ 𝑘)) |
63 | 35, 62 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧
((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘) → (𝑃 / 2) ≤ (𝑘 · 2)) |
64 | 63 | exp31 628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℤ → (𝑃 ∈ ℕ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 / 2) ≤ (𝑘 · 2)))) |
65 | 64 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℤ →
(((⌊‘(𝑃 / 4)) +
1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
66 | 13, 65 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
67 | 66 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑘 → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
68 | 67 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) ≤ 𝑘 → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻) → (((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2)))) |
70 | 69 | impcom 445 |
. . . . . . . . . 10
⊢ ((((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻)) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
71 | 10, 70 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑃 ∈ ℕ → (𝑃 / 2) ≤ (𝑘 · 2))) |
72 | 71 | impcom 445 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 / 2) ≤ (𝑘 · 2)) |
73 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
74 | 73 | zred 11358 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℝ) |
75 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℝ) |
76 | 74, 75 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℝ) |
77 | | lenlt 9995 |
. . . . . . . . 9
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑘 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑘 · 2) ↔
¬ (𝑘 · 2) <
(𝑃 / 2))) |
78 | 36, 76, 77 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 / 2) ≤ (𝑘 · 2) ↔ ¬ (𝑘 · 2) < (𝑃 / 2))) |
79 | 72, 78 | mpbid 221 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
80 | 9, 79 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
81 | 80 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → ¬ (𝑘 · 2) < (𝑃 / 2)) |
82 | 81 | iffalsed 4047 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑃 − (𝑘 · 2))) |
83 | 7, 82 | eqtrd 2644 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑘 · 2))) |
84 | 8, 11 | gausslemma2dlem0d 24884 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
85 | | nn0p1nn 11209 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
86 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
87 | 85, 86 | syl6eleq 2698 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
(ℤ≥‘1)) |
88 | 84, 87 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
89 | | fzss1 12251 |
. . . . 5
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
90 | 88, 89 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ⊆ (1...𝐻)) |
91 | 90 | sselda 3568 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ (1...𝐻)) |
92 | | ovex 6577 |
. . . 4
⊢ (𝑃 − (𝑘 · 2)) ∈ V |
93 | 92 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈ V) |
94 | 2, 83, 91, 93 | fvmptd 6197 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
95 | 94 | ralrimiva 2949 |
1
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |