Proof of Theorem pntlemj
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pntlem1.r | . . . . . . 7
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 2 |  | pntlem1.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 3 |  | pntlem1.b | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 4 |  | pntlem1.l | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | 
| 5 |  | pntlem1.d | . . . . . . 7
⊢ 𝐷 = (𝐴 + 1) | 
| 6 |  | pntlem1.f | . . . . . . 7
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) | 
| 7 |  | pntlem1.u | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 8 |  | pntlem1.u2 | . . . . . . 7
⊢ (𝜑 → 𝑈 ≤ 𝐴) | 
| 9 |  | pntlem1.e | . . . . . . 7
⊢ 𝐸 = (𝑈 / 𝐷) | 
| 10 |  | pntlem1.k | . . . . . . 7
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) | 
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 27639 | . . . . . 6
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) | 
| 12 | 11 | simp3d 1145 | . . . . 5
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) | 
| 13 | 12 | simp3d 1145 | . . . 4
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) | 
| 14 | 1, 2, 3, 4, 5, 6 | pntlemd 27638 | . . . . . . . 8
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) | 
| 15 | 14 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈
ℝ+) | 
| 16 | 11 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 17 | 15, 16 | rpmulcld 13093 | . . . . . 6
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) | 
| 18 |  | 8nn 12361 | . . . . . . 7
⊢ 8 ∈
ℕ | 
| 19 |  | nnrp 13046 | . . . . . . 7
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) | 
| 20 | 18, 19 | ax-mp 5 | . . . . . 6
⊢ 8 ∈
ℝ+ | 
| 21 |  | rpdivcl 13060 | . . . . . 6
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈
ℝ+) → ((𝐿 · 𝐸) / 8) ∈
ℝ+) | 
| 22 | 17, 20, 21 | sylancl 586 | . . . . 5
⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈
ℝ+) | 
| 23 |  | pntlem1.y | . . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) | 
| 24 |  | pntlem1.x | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) | 
| 25 |  | pntlem1.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 26 |  | pntlem1.w | . . . . . . . . 9
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 27 |  | pntlem1.z | . . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) | 
| 28 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27 | pntlemb 27641 | . . . . . . . 8
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 29 | 28 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 30 | 29 | rpred 13077 | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 31 | 28 | simp2d 1144 | . . . . . . 7
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) | 
| 32 | 31 | simp1d 1143 | . . . . . 6
⊢ (𝜑 → 1 < 𝑍) | 
| 33 | 30, 32 | rplogcld 26671 | . . . . 5
⊢ (𝜑 → (log‘𝑍) ∈
ℝ+) | 
| 34 | 22, 33 | rpmulcld 13093 | . . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈
ℝ+) | 
| 35 | 13, 34 | rpmulcld 13093 | . . 3
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈
ℝ+) | 
| 36 | 35 | rpred 13077 | . 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ) | 
| 37 |  | pntlem1.i | . . . . . 6
⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) | 
| 38 |  | fzfid 14014 | . . . . . 6
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin) | 
| 39 | 37, 38 | eqeltrid 2845 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ Fin) | 
| 40 |  | hashcl 14395 | . . . . 5
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) | 
| 41 | 39, 40 | syl 17 | . . . 4
⊢ (𝜑 → (♯‘𝐼) ∈
ℕ0) | 
| 42 | 41 | nn0red 12588 | . . 3
⊢ (𝜑 → (♯‘𝐼) ∈
ℝ) | 
| 43 | 13 | rpred 13077 | . . . 4
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ) | 
| 44 |  | pntlem1.v | . . . . . . 7
⊢ (𝜑 → 𝑉 ∈
ℝ+) | 
| 45 | 29, 44 | rpdivcld 13094 | . . . . . 6
⊢ (𝜑 → (𝑍 / 𝑉) ∈
ℝ+) | 
| 46 | 45 | relogcld 26665 | . . . . 5
⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ) | 
| 47 | 46, 45 | rerpdivcld 13108 | . . . 4
⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ) | 
| 48 | 43, 47 | remulcld 11291 | . . 3
⊢ (𝜑 → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ) | 
| 49 | 42, 48 | remulcld 11291 | . 2
⊢ (𝜑 → ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ∈ ℝ) | 
| 50 |  | pntlem1.o | . . . 4
⊢ 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) | 
| 51 |  | fzfid 14014 | . . . 4
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) ∈ Fin) | 
| 52 | 50, 51 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝑂 ∈ Fin) | 
| 53 | 7 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 54 | 53 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑈 ∈ ℝ) | 
| 55 | 11 | simp2d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 56 |  | pntlem1.j | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁)) | 
| 57 |  | elfzoelz 13699 | . . . . . . . . . . . . 13
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 59 | 58 | peano2zd 12725 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) | 
| 60 | 55, 59 | rpexpcld 14286 | . . . . . . . . . 10
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈
ℝ+) | 
| 61 | 29, 60 | rpdivcld 13094 | . . . . . . . . 9
⊢ (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈
ℝ+) | 
| 62 | 61 | rprege0d 13084 | . . . . . . . 8
⊢ (𝜑 → ((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1))))) | 
| 63 |  | flge0nn0 13860 | . . . . . . . 8
⊢ (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈
ℕ0) | 
| 64 |  | nn0p1nn 12565 | . . . . . . . 8
⊢
((⌊‘(𝑍 /
(𝐾↑(𝐽 + 1)))) ∈ ℕ0 →
((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈
ℕ) | 
| 65 | 62, 63, 64 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈
ℕ) | 
| 66 |  | elfzuz 13560 | . . . . . . . 8
⊢ (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) → 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) | 
| 67 | 66, 50 | eleq2s 2859 | . . . . . . 7
⊢ (𝑛 ∈ 𝑂 → 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) | 
| 68 |  | eluznn 12960 | . . . . . . 7
⊢
((((⌊‘(𝑍
/ (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ
∧ 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) → 𝑛 ∈ ℕ) | 
| 69 | 65, 67, 68 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ ℕ) | 
| 70 | 54, 69 | nndivred 12320 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑈 / 𝑛) ∈ ℝ) | 
| 71 | 29 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑍 ∈
ℝ+) | 
| 72 | 69 | nnrpd 13075 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ ℝ+) | 
| 73 | 71, 72 | rpdivcld 13094 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑍 / 𝑛) ∈
ℝ+) | 
| 74 | 1 | pntrf 27607 | . . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ | 
| 75 | 74 | ffvelcdmi 7103 | . . . . . . . . 9
⊢ ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) | 
| 76 | 73, 75 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) | 
| 77 | 76, 71 | rerpdivcld 13108 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ) | 
| 78 | 77 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ) | 
| 79 | 78 | abscld 15475 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ) | 
| 80 | 70, 79 | resubcld 11691 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ) | 
| 81 | 72 | relogcld 26665 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (log‘𝑛) ∈ ℝ) | 
| 82 | 80, 81 | remulcld 11291 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) | 
| 83 | 52, 82 | fsumrecl 15770 | . 2
⊢ (𝜑 → Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) | 
| 84 |  | pntlem1.m | . . 3
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) | 
| 85 |  | pntlem1.n | . . 3
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) | 
| 86 |  | pntlem1.U | . . 3
⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) | 
| 87 |  | pntlem1.K | . . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 88 |  | pntlem1.V | . . 3
⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 89 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37 | pntlemr 27646 | . 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) | 
| 90 | 48 | recnd 11289 | . . . . 5
⊢ (𝜑 → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) | 
| 91 |  | fsumconst 15826 | . . . . 5
⊢ ((𝐼 ∈ Fin ∧ ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) → Σ𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) | 
| 92 | 39, 90, 91 | syl2anc 584 | . . . 4
⊢ (𝜑 → Σ𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) | 
| 93 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37 | pntlemq 27645 | . . . . 5
⊢ (𝜑 → 𝐼 ⊆ 𝑂) | 
| 94 | 90 | ralrimivw 3150 | . . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) | 
| 95 | 52 | olcd 875 | . . . . 5
⊢ (𝜑 → (𝑂 ⊆ (ℤ≥‘1)
∨ 𝑂 ∈
Fin)) | 
| 96 |  | sumss2 15762 | . . . . 5
⊢ (((𝐼 ⊆ 𝑂 ∧ ∀𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) ∧ (𝑂 ⊆ (ℤ≥‘1)
∨ 𝑂 ∈ Fin)) →
Σ𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛 ∈ 𝑂 if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0)) | 
| 97 | 93, 94, 95, 96 | syl21anc 838 | . . . 4
⊢ (𝜑 → Σ𝑛 ∈ 𝐼 ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛 ∈ 𝑂 if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0)) | 
| 98 | 92, 97 | eqtr3d 2779 | . . 3
⊢ (𝜑 → ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = Σ𝑛 ∈ 𝑂 if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0)) | 
| 99 | 48 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ) | 
| 100 | 99 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑂) ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ) | 
| 101 |  | 0red 11264 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑂) ∧ ¬ 𝑛 ∈ 𝐼) → 0 ∈ ℝ) | 
| 102 | 100, 101 | ifclda 4561 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ∈ ℝ) | 
| 103 |  | breq1 5146 | . . . . 5
⊢ (((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) | 
| 104 |  | breq1 5146 | . . . . 5
⊢ (0 =
if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) | 
| 105 | 13 | rpregt0d 13083 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑈 − 𝐸) ∈ ℝ ∧ 0 < (𝑈 − 𝐸))) | 
| 106 | 105 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) ∈ ℝ ∧ 0 < (𝑈 − 𝐸))) | 
| 107 | 106 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑈 − 𝐸) ∈ ℝ) | 
| 108 |  | 1rp 13038 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ | 
| 109 |  | rpaddcl 13057 | . . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 +
(𝐿 · 𝐸)) ∈
ℝ+) | 
| 110 | 108, 17, 109 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈
ℝ+) | 
| 111 | 110, 44 | rpmulcld 13093 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈
ℝ+) | 
| 112 | 29, 111 | rpdivcld 13094 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈
ℝ+) | 
| 113 | 112 | rprege0d 13084 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 114 |  | flge0nn0 13860 | . . . . . . . . . . . . 13
⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈
ℕ0) | 
| 115 |  | nn0p1nn 12565 | . . . . . . . . . . . . 13
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0 →
((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ) | 
| 116 | 113, 114,
115 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ) | 
| 117 |  | elfzuz 13560 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) | 
| 118 | 117, 37 | eleq2s 2859 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝐼 → 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) | 
| 119 |  | eluznn 12960 | . . . . . . . . . . . 12
⊢
((((⌊‘(𝑍
/ ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) → 𝑛 ∈ ℕ) | 
| 120 | 116, 118,
119 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ ℕ) | 
| 121 | 120 | nnrpd 13075 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ ℝ+) | 
| 122 | 121 | relogcld 26665 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (log‘𝑛) ∈ ℝ) | 
| 123 | 122, 120 | nndivred 12320 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((log‘𝑛) / 𝑛) ∈ ℝ) | 
| 124 | 107, 123 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛)) ∈ ℝ) | 
| 125 | 93 | sselda 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ 𝑂) | 
| 126 | 125, 82 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) | 
| 127 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ 𝐼) | 
| 128 | 127, 37 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))) | 
| 129 |  | elfzle2 13568 | . . . . . . . . . . 11
⊢ (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉))) | 
| 130 | 128, 129 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉))) | 
| 131 | 45 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ) | 
| 132 | 131 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / 𝑉) ∈ ℝ) | 
| 133 | 128 | elfzelzd 13565 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ ℤ) | 
| 134 |  | flge 13845 | . . . . . . . . . . 11
⊢ (((𝑍 / 𝑉) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))) | 
| 135 | 132, 133,
134 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))) | 
| 136 | 130, 135 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ≤ (𝑍 / 𝑉)) | 
| 137 | 120 | nnred 12281 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ ℝ) | 
| 138 |  | ere 16125 | . . . . . . . . . . . 12
⊢ e ∈
ℝ | 
| 139 | 138 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → e ∈ ℝ) | 
| 140 | 112 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) | 
| 141 | 140 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) | 
| 142 | 138 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → e ∈
ℝ) | 
| 143 | 29 | rpsqrtcld 15450 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) | 
| 144 | 143 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) | 
| 145 | 31 | simp2d 1144 | . . . . . . . . . . . . 13
⊢ (𝜑 → e ≤
(√‘𝑍)) | 
| 146 | 111 | rpred 13077 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) | 
| 147 | 60 | rpred 13077 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ) | 
| 148 | 88 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))) | 
| 149 | 148 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) | 
| 150 | 55 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 151 | 55, 58 | rpexpcld 14286 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐾↑𝐽) ∈
ℝ+) | 
| 152 | 151 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ) | 
| 153 | 150, 152 | mulcomd 11282 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = ((𝐾↑𝐽) · 𝐾)) | 
| 154 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemg 27642 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) | 
| 155 | 154 | simp1d 1143 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 156 |  | elfzouz 13703 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) | 
| 157 | 56, 156 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑀)) | 
| 158 |  | eluznn 12960 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) | 
| 159 | 155, 157,
158 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐽 ∈ ℕ) | 
| 160 | 159 | nnnn0d 12587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 161 | 150, 160 | expp1d 14187 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾)) | 
| 162 | 153, 161 | eqtr4d 2780 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1))) | 
| 163 | 149, 162 | breqtrd 5169 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1))) | 
| 164 | 146, 147,
163 | ltled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1))) | 
| 165 |  | fzofzp1 13803 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁)) | 
| 166 | 56, 165 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁)) | 
| 167 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemh 27643 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) | 
| 168 | 166, 167 | mpdan 687 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) | 
| 169 | 168 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)) | 
| 170 | 146, 147,
144, 164, 169 | letrd 11418 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍)) | 
| 171 | 146, 144,
143 | lemul2d 13121 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))) | 
| 172 | 170, 171 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))) | 
| 173 | 29 | rprege0d 13084 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 174 |  | remsqsqrt 15295 | . . . . . . . . . . . . . . . 16
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) | 
| 175 | 173, 174 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) | 
| 176 | 172, 175 | breqtrd 5169 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍) | 
| 177 | 144, 30, 111 | lemuldivd 13126 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 178 | 176, 177 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 179 | 142, 144,
140, 145, 178 | letrd 11418 | . . . . . . . . . . . 12
⊢ (𝜑 → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 180 | 179 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 181 |  | reflcl 13836 | . . . . . . . . . . . . . 14
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ →
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) | 
| 182 |  | peano2re 11434 | . . . . . . . . . . . . . 14
⊢
((⌊‘(𝑍 /
((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ →
((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ) | 
| 183 | 140, 181,
182 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ) | 
| 184 | 183 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ) | 
| 185 |  | fllep1 13841 | . . . . . . . . . . . . 13
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) | 
| 186 | 141, 185 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) | 
| 187 |  | elfzle1 13567 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛) | 
| 188 | 128, 187 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛) | 
| 189 | 141, 184,
137, 186, 188 | letrd 11418 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛) | 
| 190 | 139, 141,
137, 180, 189 | letrd 11418 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → e ≤ 𝑛) | 
| 191 | 139, 137,
132, 190, 136 | letrd 11418 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → e ≤ (𝑍 / 𝑉)) | 
| 192 |  | logdivle 26664 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℝ ∧ e ≤
𝑛) ∧ ((𝑍 / 𝑉) ∈ ℝ ∧ e ≤ (𝑍 / 𝑉))) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛))) | 
| 193 | 137, 190,
132, 191, 192 | syl22anc 839 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛))) | 
| 194 | 136, 193 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)) | 
| 195 | 47 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ) | 
| 196 |  | lemul2 12120 | . . . . . . . . 9
⊢
((((log‘(𝑍 /
𝑉)) / (𝑍 / 𝑉)) ∈ ℝ ∧ ((log‘𝑛) / 𝑛) ∈ ℝ ∧ ((𝑈 − 𝐸) ∈ ℝ ∧ 0 < (𝑈 − 𝐸))) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛)))) | 
| 197 | 195, 123,
106, 196 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛)))) | 
| 198 | 194, 197 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛))) | 
| 199 | 13 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) | 
| 200 | 199 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑈 − 𝐸) ∈ ℂ) | 
| 201 | 122 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (log‘𝑛) ∈ ℂ) | 
| 202 | 121 | rpcnne0d 13086 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) | 
| 203 |  | div23 11941 | . . . . . . . . . 10
⊢ (((𝑈 − 𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈 − 𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈 − 𝐸) / 𝑛) · (log‘𝑛))) | 
| 204 | 200, 201,
202, 203 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑈 − 𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈 − 𝐸) / 𝑛) · (log‘𝑛))) | 
| 205 |  | divass 11940 | . . . . . . . . . 10
⊢ (((𝑈 − 𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈 − 𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛))) | 
| 206 | 200, 201,
202, 205 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑈 − 𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛))) | 
| 207 | 204, 206 | eqtr3d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑈 − 𝐸) / 𝑛) · (log‘𝑛)) = ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛))) | 
| 208 | 43 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑈 − 𝐸) ∈ ℝ) | 
| 209 | 208, 120 | nndivred 12320 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) / 𝑛) ∈ ℝ) | 
| 210 | 125, 80 | syldan 591 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ) | 
| 211 |  | log1 26627 | . . . . . . . . . 10
⊢
(log‘1) = 0 | 
| 212 | 120 | nnge1d 12314 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 1 ≤ 𝑛) | 
| 213 |  | logleb 26645 | . . . . . . . . . . . 12
⊢ ((1
∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (1 ≤
𝑛 ↔ (log‘1) ≤
(log‘𝑛))) | 
| 214 | 108, 121,
213 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛))) | 
| 215 | 212, 214 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (log‘1) ≤ (log‘𝑛)) | 
| 216 | 211, 215 | eqbrtrrid 5179 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 0 ≤ (log‘𝑛)) | 
| 217 | 7 | rpcnd 13079 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 218 | 217 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑈 ∈ ℂ) | 
| 219 | 16 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 220 | 219 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝐸 ∈ ℝ) | 
| 221 | 220 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝐸 ∈ ℂ) | 
| 222 |  | divsubdir 11961 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑈 − 𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛))) | 
| 223 | 218, 221,
202, 222 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛))) | 
| 224 | 125, 79 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ) | 
| 225 | 220, 120 | nndivred 12320 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝐸 / 𝑛) ∈ ℝ) | 
| 226 | 125, 70 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑈 / 𝑛) ∈ ℝ) | 
| 227 | 125, 76 | syldan 591 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) | 
| 228 | 227 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ) | 
| 229 | 29 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑍 ∈
ℝ+) | 
| 230 | 229 | rpcnne0d 13086 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) | 
| 231 |  | divdiv2 11979 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍)) | 
| 232 | 228, 230,
202, 231 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍)) | 
| 233 | 121 | rpcnd 13079 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ ℂ) | 
| 234 |  | div23 11941 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) | 
| 235 | 228, 233,
230, 234 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) | 
| 236 | 232, 235 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) | 
| 237 | 236 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))) | 
| 238 | 125, 78 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ) | 
| 239 | 238, 233 | absmuld 15493 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛))) | 
| 240 | 121 | rprege0d 13084 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛)) | 
| 241 |  | absid 15335 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) → (abs‘𝑛) = 𝑛) | 
| 242 | 240, 241 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘𝑛) = 𝑛) | 
| 243 | 242 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛)) | 
| 244 | 237, 239,
243 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛)) | 
| 245 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑍 / 𝑛) → (𝑅‘𝑢) = (𝑅‘(𝑍 / 𝑛))) | 
| 246 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑍 / 𝑛) → 𝑢 = (𝑍 / 𝑛)) | 
| 247 | 245, 246 | oveq12d 7449 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑍 / 𝑛) → ((𝑅‘𝑢) / 𝑢) = ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) | 
| 248 | 247 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑍 / 𝑛) → (abs‘((𝑅‘𝑢) / 𝑢)) = (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)))) | 
| 249 | 248 | breq1d 5153 | . . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑍 / 𝑛) → ((abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸)) | 
| 250 | 88 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) | 
| 251 | 250 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) | 
| 252 | 30 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑍 ∈ ℝ) | 
| 253 | 252, 120 | nndivred 12320 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / 𝑛) ∈ ℝ) | 
| 254 | 44 | rpregt0d 13083 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 < 𝑉)) | 
| 255 | 254 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑉 ∈ ℝ ∧ 0 < 𝑉)) | 
| 256 |  | lemuldiv2 12149 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ (𝑉 ∈ ℝ ∧ 0 <
𝑉)) → ((𝑉 · 𝑛) ≤ 𝑍 ↔ 𝑛 ≤ (𝑍 / 𝑉))) | 
| 257 | 137, 252,
255, 256 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑉 · 𝑛) ≤ 𝑍 ↔ 𝑛 ≤ (𝑍 / 𝑉))) | 
| 258 | 136, 257 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑉 · 𝑛) ≤ 𝑍) | 
| 259 | 255 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑉 ∈ ℝ) | 
| 260 | 259, 252,
121 | lemuldivd 13126 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑉 · 𝑛) ≤ 𝑍 ↔ 𝑉 ≤ (𝑍 / 𝑛))) | 
| 261 | 258, 260 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑉 ≤ (𝑍 / 𝑛)) | 
| 262 | 111 | rpregt0d 13083 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 263 | 262 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 264 | 121 | rpregt0d 13083 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑛 ∈ ℝ ∧ 0 < 𝑛)) | 
| 265 |  | lediv23 12160 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑍 ∈ ℝ ∧ (((1 +
(𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 266 | 252, 263,
264, 265 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 267 | 189, 266 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)) | 
| 268 | 44 | rpred 13077 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑉 ∈ ℝ) | 
| 269 | 268 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 𝑉 ∈ ℝ) | 
| 270 | 146 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) | 
| 271 |  | elicc2 13452 | . . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ ℝ ∧ ((1 +
(𝐿 · 𝐸)) · 𝑉) ∈ ℝ) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 272 | 269, 270,
271 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 273 | 253, 261,
267, 272 | mpbir3and 1343 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 274 | 249, 251,
273 | rspcdva 3623 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸) | 
| 275 | 244, 274 | eqbrtrrd 5167 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸) | 
| 276 | 224, 220,
121 | lemuldivd 13126 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛))) | 
| 277 | 275, 276 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛)) | 
| 278 | 224, 225,
226, 277 | lesub2dd 11880 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 / 𝑛) − (𝐸 / 𝑛)) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)))) | 
| 279 | 223, 278 | eqbrtrd 5165 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) / 𝑛) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)))) | 
| 280 | 209, 210,
122, 216, 279 | lemul1ad 12207 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (((𝑈 − 𝐸) / 𝑛) · (log‘𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 281 | 207, 280 | eqbrtrrd 5167 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘𝑛) / 𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 282 | 99, 124, 126, 198, 281 | letrd 11418 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 283 | 282 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑂) ∧ 𝑛 ∈ 𝐼) → ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 284 | 69 | nnred 12281 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ ℝ) | 
| 285 | 29, 151 | rpdivcld 13094 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈
ℝ+) | 
| 286 | 285 | rpred 13077 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ∈ ℝ) | 
| 287 | 286 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑍 / (𝐾↑𝐽)) ∈ ℝ) | 
| 288 | 23 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈
ℝ+) | 
| 289 | 29, 288 | rpdivcld 13094 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 / 𝑌) ∈
ℝ+) | 
| 290 | 289 | rpred 13077 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ) | 
| 291 | 290 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑍 / 𝑌) ∈ ℝ) | 
| 292 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ 𝑂) | 
| 293 | 292, 50 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))) | 
| 294 |  | elfzle2 13568 | . . . . . . . . . . 11
⊢ (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽)))) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) | 
| 295 | 293, 294 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾↑𝐽)))) | 
| 296 | 69 | nnzd 12640 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ∈ ℤ) | 
| 297 |  | flge 13845 | . . . . . . . . . . 11
⊢ (((𝑍 / (𝐾↑𝐽)) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / (𝐾↑𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾↑𝐽))))) | 
| 298 | 287, 296,
297 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑛 ≤ (𝑍 / (𝐾↑𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾↑𝐽))))) | 
| 299 | 295, 298 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ≤ (𝑍 / (𝐾↑𝐽))) | 
| 300 | 288 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 301 | 24 | simpld 494 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈
ℝ+) | 
| 302 | 301 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 303 | 151 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ) | 
| 304 | 24 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 < 𝑋) | 
| 305 | 300, 302,
304 | ltled 11409 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ≤ 𝑋) | 
| 306 |  | elfzofz 13715 | . . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (𝑀...𝑁)) | 
| 307 | 56, 306 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) | 
| 308 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemh 27643 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍))) | 
| 309 | 307, 308 | mpdan 687 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍))) | 
| 310 | 309 | simpld 494 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 < (𝐾↑𝐽)) | 
| 311 | 302, 303,
310 | ltled 11409 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≤ (𝐾↑𝐽)) | 
| 312 | 300, 302,
303, 305, 311 | letrd 11418 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ≤ (𝐾↑𝐽)) | 
| 313 | 288, 151,
29 | lediv2d 13101 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ≤ (𝐾↑𝐽) ↔ (𝑍 / (𝐾↑𝐽)) ≤ (𝑍 / 𝑌))) | 
| 314 | 312, 313 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / (𝐾↑𝐽)) ≤ (𝑍 / 𝑌)) | 
| 315 | 314 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑍 / (𝐾↑𝐽)) ≤ (𝑍 / 𝑌)) | 
| 316 | 284, 287,
291, 299, 315 | letrd 11418 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 𝑛 ≤ (𝑍 / 𝑌)) | 
| 317 | 69, 316 | jca 511 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) | 
| 318 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86 | pntlemn 27644 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 319 | 317, 318 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 320 | 319 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑂) ∧ ¬ 𝑛 ∈ 𝐼) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 321 | 103, 104,
283, 320 | ifbothda 4564 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑂) → if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 322 | 52, 102, 82, 321 | fsumle 15835 | . . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝑂 if(𝑛 ∈ 𝐼, ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 323 | 98, 322 | eqbrtrd 5165 | . 2
⊢ (𝜑 → ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 324 | 36, 49, 83, 89, 323 | letrd 11418 | 1
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |