Proof of Theorem pntlemq
Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . 10
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
2 | | pntlem1.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
3 | | pntlem1.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
4 | | pntlem1.l |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
5 | | pntlem1.d |
. . . . . . . . . 10
⊢ 𝐷 = (𝐴 + 1) |
6 | | pntlem1.f |
. . . . . . . . . 10
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) |
7 | | pntlem1.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
8 | | pntlem1.u2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
9 | | pntlem1.e |
. . . . . . . . . 10
⊢ 𝐸 = (𝑈 / 𝐷) |
10 | | pntlem1.k |
. . . . . . . . . 10
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) |
11 | | pntlem1.y |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
12 | | pntlem1.x |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) |
13 | | pntlem1.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
14 | | pntlem1.w |
. . . . . . . . . 10
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
15 | | pntlem1.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | pntlemb 26745 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |
17 | 16 | simp1d 1141 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 26743 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) |
19 | 18 | simp2d 1142 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
20 | | pntlem1.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁)) |
21 | | elfzoelz 13387 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
23 | 22 | peano2zd 12429 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
24 | 19, 23 | rpexpcld 13962 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈
ℝ+) |
25 | 17, 24 | rpdivcld 12789 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈
ℝ+) |
26 | 25 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ) |
27 | 26 | flcld 13518 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℤ) |
28 | | 1rp 12734 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
29 | 1, 2, 3, 4, 5, 6 | pntlemd 26742 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) |
30 | 29 | simp1d 1141 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
31 | 18 | simp1d 1141 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
32 | 30, 31 | rpmulcld 12788 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) |
33 | | rpaddcl 12752 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 +
(𝐿 · 𝐸)) ∈
ℝ+) |
34 | 28, 32, 33 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈
ℝ+) |
35 | | pntlem1.v |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈
ℝ+) |
36 | 34, 35 | rpmulcld 12788 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈
ℝ+) |
37 | 17, 36 | rpdivcld 12789 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈
ℝ+) |
38 | 37 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) |
39 | 38 | flcld 13518 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℤ) |
40 | 36 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) |
41 | 24 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ) |
42 | | pntlem1.V |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
43 | 42 | simpld 495 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))) |
44 | 43 | simprd 496 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) |
45 | 19 | rpcnd 12774 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℂ) |
46 | 19, 22 | rpexpcld 13962 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾↑𝐽) ∈
ℝ+) |
47 | 46 | rpcnd 12774 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ) |
48 | 45, 47 | mulcomd 10996 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = ((𝐾↑𝐽) · 𝐾)) |
49 | | pntlem1.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) |
50 | | pntlem1.n |
. . . . . . . . . . . . . . 15
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) |
51 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 49, 50 | pntlemg 26746 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) |
52 | 51 | simp1d 1141 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
53 | | elfzouz 13391 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) |
54 | 20, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑀)) |
55 | | eluznn 12658 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) |
56 | 52, 54, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ ℕ) |
57 | 56 | nnnn0d 12293 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
58 | 45, 57 | expp1d 13865 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾)) |
59 | 48, 58 | eqtr4d 2781 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1))) |
60 | 44, 59 | breqtrd 5100 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1))) |
61 | 40, 41, 60 | ltled 11123 |
. . . . . . 7
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1))) |
62 | 36, 24, 17 | lediv2d 12796 |
. . . . . . 7
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)) ↔ (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
63 | 61, 62 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) |
64 | | flwordi 13532 |
. . . . . 6
⊢ (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
65 | 26, 38, 63, 64 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
66 | | eluz2 12588 |
. . . . 5
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1))))) ↔ ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℤ ∧
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ∈ ℤ ∧
(⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
67 | 27, 39, 65, 66 | syl3anbrc 1342 |
. . . 4
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))))) |
68 | | eluzp1p1 12610 |
. . . 4
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1))))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) |
69 | | fzss1 13295 |
. . . 4
⊢
(((⌊‘(𝑍
/ ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)) →
(((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉)))) |
70 | 67, 68, 69 | 3syl 18 |
. . 3
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉)))) |
71 | 17, 35 | rpdivcld 12789 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / 𝑉) ∈
ℝ+) |
72 | 71 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ) |
73 | 72 | flcld 13518 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ) |
74 | 17, 46 | rpdivcld 12789 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈
ℝ+) |
75 | 74 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈ ℝ) |
76 | 75 | flcld 13518 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑𝐽))) ∈ ℤ) |
77 | 46 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ) |
78 | 35 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ ℝ) |
79 | 43 | simpld 495 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑𝐽) < 𝑉) |
80 | 77, 78, 79 | ltled 11123 |
. . . . . . 7
⊢ (𝜑 → (𝐾↑𝐽) ≤ 𝑉) |
81 | 46, 35, 17 | lediv2d 12796 |
. . . . . . 7
⊢ (𝜑 → ((𝐾↑𝐽) ≤ 𝑉 ↔ (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽)))) |
82 | 80, 81 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽))) |
83 | | flwordi 13532 |
. . . . . 6
⊢ (((𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / (𝐾↑𝐽)) ∈ ℝ ∧ (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽))) → (⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) |
84 | 72, 75, 82, 83 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) |
85 | | eluz2 12588 |
. . . . 5
⊢
((⌊‘(𝑍 /
(𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉))) ↔ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ ∧
(⌊‘(𝑍 / (𝐾↑𝐽))) ∈ ℤ ∧
(⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽))))) |
86 | 73, 76, 84, 85 | syl3anbrc 1342 |
. . . 4
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉)))) |
87 | | fzss2 13296 |
. . . 4
⊢
((⌊‘(𝑍 /
(𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉))) → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
88 | 86, 87 | syl 17 |
. . 3
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
89 | 70, 88 | sstrd 3931 |
. 2
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
90 | | pntlem1.i |
. 2
⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) |
91 | | pntlem1.o |
. 2
⊢ 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) |
92 | 89, 90, 91 | 3sstr4g 3966 |
1
⊢ (𝜑 → 𝐼 ⊆ 𝑂) |