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 27641 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |
| 17 | 16 | simp1d 1143 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
| 18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 27639 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) |
| 19 | 18 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
| 20 | | pntlem1.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁)) |
| 21 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 23 | 22 | peano2zd 12725 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
| 24 | 19, 23 | rpexpcld 14286 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈
ℝ+) |
| 25 | 17, 24 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈
ℝ+) |
| 26 | 25 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ) |
| 27 | 26 | flcld 13838 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℤ) |
| 28 | | 1rp 13038 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
| 29 | 1, 2, 3, 4, 5, 6 | pntlemd 27638 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) |
| 30 | 29 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
| 31 | 18 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 32 | 30, 31 | rpmulcld 13093 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) |
| 33 | | rpaddcl 13057 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 +
(𝐿 · 𝐸)) ∈
ℝ+) |
| 34 | 28, 32, 33 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈
ℝ+) |
| 35 | | pntlem1.v |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈
ℝ+) |
| 36 | 34, 35 | rpmulcld 13093 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈
ℝ+) |
| 37 | 17, 36 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈
ℝ+) |
| 38 | 37 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) |
| 39 | 38 | flcld 13838 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℤ) |
| 40 | 36 | rpred 13077 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) |
| 41 | 24 | rpred 13077 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ) |
| 42 | | pntlem1.V |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
| 43 | 42 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))) |
| 44 | 43 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) |
| 45 | 19 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 46 | 19, 22 | rpexpcld 14286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾↑𝐽) ∈
ℝ+) |
| 47 | 46 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ) |
| 48 | 45, 47 | mulcomd 11282 |
. . . . . . . . . 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 27642 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) |
| 52 | 51 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 53 | | elfzouz 13703 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) |
| 54 | 20, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑀)) |
| 55 | | eluznn 12960 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) |
| 56 | 52, 54, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ ℕ) |
| 57 | 56 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
| 58 | 45, 57 | expp1d 14187 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾)) |
| 59 | 48, 58 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1))) |
| 60 | 44, 59 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1))) |
| 61 | 40, 41, 60 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1))) |
| 62 | 36, 24, 17 | lediv2d 13101 |
. . . . . . 7
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)) ↔ (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
| 63 | 61, 62 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) |
| 64 | | flwordi 13852 |
. . . . . 6
⊢ (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝐽 + 1))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
| 65 | 26, 38, 63, 64 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
| 66 | | eluz2 12884 |
. . . . 5
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1))))) ↔ ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℤ ∧
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ∈ ℤ ∧
(⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ≤ (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
| 67 | 27, 39, 65, 66 | syl3anbrc 1344 |
. . . 4
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))))) |
| 68 | | eluzp1p1 12906 |
. . . 4
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝐽 + 1))))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) |
| 69 | | fzss1 13603 |
. . . 4
⊢
(((⌊‘(𝑍
/ ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)) →
(((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉)))) |
| 70 | 67, 68, 69 | 3syl 18 |
. . 3
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉)))) |
| 71 | 17, 35 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / 𝑉) ∈
ℝ+) |
| 72 | 71 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ) |
| 73 | 72 | flcld 13838 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ) |
| 74 | 17, 46 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈
ℝ+) |
| 75 | 74 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈ ℝ) |
| 76 | 75 | flcld 13838 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑𝐽))) ∈ ℤ) |
| 77 | 46 | rpred 13077 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ) |
| 78 | 35 | rpred 13077 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ ℝ) |
| 79 | 43 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → (𝐾↑𝐽) < 𝑉) |
| 80 | 77, 78, 79 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → (𝐾↑𝐽) ≤ 𝑉) |
| 81 | 46, 35, 17 | lediv2d 13101 |
. . . . . . 7
⊢ (𝜑 → ((𝐾↑𝐽) ≤ 𝑉 ↔ (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽)))) |
| 82 | 80, 81 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽))) |
| 83 | | flwordi 13852 |
. . . . . 6
⊢ (((𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / (𝐾↑𝐽)) ∈ ℝ ∧ (𝑍 / 𝑉) ≤ (𝑍 / (𝐾↑𝐽))) → (⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) |
| 84 | 72, 75, 82, 83 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) |
| 85 | | eluz2 12884 |
. . . . 5
⊢
((⌊‘(𝑍 /
(𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉))) ↔ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ ∧
(⌊‘(𝑍 / (𝐾↑𝐽))) ∈ ℤ ∧
(⌊‘(𝑍 / 𝑉)) ≤ (⌊‘(𝑍 / (𝐾↑𝐽))))) |
| 86 | 73, 76, 84, 85 | syl3anbrc 1344 |
. . . 4
⊢ (𝜑 → (⌊‘(𝑍 / (𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉)))) |
| 87 | | fzss2 13604 |
. . . 4
⊢
((⌊‘(𝑍 /
(𝐾↑𝐽))) ∈
(ℤ≥‘(⌊‘(𝑍 / 𝑉))) → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
| 88 | 86, 87 | syl 17 |
. . 3
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
| 89 | 70, 88 | sstrd 3994 |
. 2
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) |
| 90 | | pntlem1.i |
. 2
⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) |
| 91 | | pntlem1.o |
. 2
⊢ 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) |
| 92 | 89, 90, 91 | 3sstr4g 4037 |
1
⊢ (𝜑 → 𝐼 ⊆ 𝑂) |