| 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 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 17 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 18 | | rpexpcl 14121 |
. . . . . . . 8
⊢ ((𝐸 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐸↑2) ∈
ℝ+) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐸↑2) ∈
ℝ+) |
| 20 | 15, 19 | rpmulcld 13093 |
. . . . . 6
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈
ℝ+) |
| 21 | | 3nn0 12544 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
| 22 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 23 | 21, 22 | decnncl 12753 |
. . . . . . . 8
⊢ ;32 ∈ ℕ |
| 24 | | nnrp 13046 |
. . . . . . . 8
⊢ (;32 ∈ ℕ → ;32 ∈
ℝ+) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢ ;32 ∈
ℝ+ |
| 26 | | rpmulcl 13058 |
. . . . . . 7
⊢ ((;32 ∈ ℝ+ ∧
𝐵 ∈
ℝ+) → (;32
· 𝐵) ∈
ℝ+) |
| 27 | 25, 3, 26 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (;32 · 𝐵) ∈
ℝ+) |
| 28 | 20, 27 | rpdivcld 13094 |
. . . . 5
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) ∈
ℝ+) |
| 29 | | pntlem1.y |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
| 30 | | pntlem1.x |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) |
| 31 | | pntlem1.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 32 | | pntlem1.w |
. . . . . . . . . 10
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
| 33 | | pntlem1.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) |
| 34 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33 | pntlemb 27641 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |
| 35 | 34 | simp1d 1143 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
| 36 | 35 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ ℝ) |
| 37 | 34 | simp2d 1144 |
. . . . . . . 8
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) |
| 38 | 37 | simp1d 1143 |
. . . . . . 7
⊢ (𝜑 → 1 < 𝑍) |
| 39 | 36, 38 | rplogcld 26671 |
. . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℝ+) |
| 40 | | rpexpcl 14121 |
. . . . . 6
⊢
(((log‘𝑍)
∈ ℝ+ ∧ 2 ∈ ℤ) → ((log‘𝑍)↑2) ∈
ℝ+) |
| 41 | 39, 17, 40 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ((log‘𝑍)↑2) ∈
ℝ+) |
| 42 | 28, 41 | rpmulcld 13093 |
. . . 4
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) ∈
ℝ+) |
| 43 | 13, 42 | rpmulcld 13093 |
. . 3
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ∈
ℝ+) |
| 44 | 43 | rpred 13077 |
. 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) |
| 45 | 15, 16 | rpmulcld 13093 |
. . . . . . 7
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) |
| 46 | | 8re 12362 |
. . . . . . . 8
⊢ 8 ∈
ℝ |
| 47 | | 8pos 12378 |
. . . . . . . 8
⊢ 0 <
8 |
| 48 | 46, 47 | elrpii 13037 |
. . . . . . 7
⊢ 8 ∈
ℝ+ |
| 49 | | rpdivcl 13060 |
. . . . . . 7
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈
ℝ+) → ((𝐿 · 𝐸) / 8) ∈
ℝ+) |
| 50 | 45, 48, 49 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈
ℝ+) |
| 51 | 50, 39 | rpmulcld 13093 |
. . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈
ℝ+) |
| 52 | 13, 51 | rpmulcld 13093 |
. . . 4
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈
ℝ+) |
| 53 | 52 | rpred 13077 |
. . 3
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ) |
| 54 | | pntlem1.m |
. . . . . . . 8
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) |
| 55 | | pntlem1.n |
. . . . . . . 8
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) |
| 56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemg 27642 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) |
| 57 | 56 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 58 | 56 | simp2d 1144 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 59 | | eluznn 12960 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℕ) |
| 60 | 57, 58, 59 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 61 | 60 | nnred 12281 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 62 | 57 | nnred 12281 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 63 | 61, 62 | resubcld 11691 |
. . 3
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℝ) |
| 64 | 53, 63 | remulcld 11291 |
. 2
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ∈ ℝ) |
| 65 | | fzfid 14014 |
. . 3
⊢ (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin) |
| 66 | 7 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℝ) |
| 67 | | elfznn 13593 |
. . . . . 6
⊢ (𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌))) → 𝑛 ∈
ℕ) |
| 68 | | nndivre 12307 |
. . . . . 6
⊢ ((𝑈 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑈 / 𝑛) ∈ ℝ) |
| 69 | 66, 67, 68 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ) |
| 70 | 35 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈
ℝ+) |
| 71 | 67 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ) |
| 72 | 71 | nnrpd 13075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+) |
| 73 | 70, 72 | rpdivcld 13094 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈
ℝ+) |
| 74 | 1 | pntrf 27607 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
| 75 | 74 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) |
| 76 | 73, 75 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) |
| 77 | 76, 70 | rerpdivcld 13108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ) |
| 78 | 77 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ) |
| 79 | 78 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ) |
| 80 | 69, 79 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ) |
| 81 | 72 | relogcld 26665 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ) |
| 82 | 80, 81 | remulcld 11291 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 83 | 65, 82 | fsumrecl 15770 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 84 | 45 | rpcnd 13079 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ) |
| 85 | 11 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
| 86 | 85 | rpred 13077 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 87 | 12 | simp2d 1144 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 < 𝐾) |
| 88 | 86, 87 | rplogcld 26671 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝐾) ∈
ℝ+) |
| 89 | 39, 88 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈
ℝ+) |
| 90 | 89 | rpcnd 13079 |
. . . . . . . . 9
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℂ) |
| 91 | | rpcnne0 13053 |
. . . . . . . . . 10
⊢ (8 ∈
ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0)) |
| 92 | 48, 91 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (8 ∈ ℂ ∧ 8
≠ 0)) |
| 93 | | 4re 12350 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
| 94 | | 4pos 12373 |
. . . . . . . . . . 11
⊢ 0 <
4 |
| 95 | 93, 94 | elrpii 13037 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
| 96 | | rpcnne0 13053 |
. . . . . . . . . 10
⊢ (4 ∈
ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0)) |
| 97 | 95, 96 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (4 ∈ ℂ ∧ 4
≠ 0)) |
| 98 | | divmuldiv 11967 |
. . . . . . . . 9
⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) / (log‘𝐾)) ∈ ℂ) ∧ ((8 ∈ ℂ
∧ 8 ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0))) → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4))) |
| 99 | 84, 90, 92, 97, 98 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4))) |
| 100 | 10 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(log‘𝐾) =
(log‘(exp‘(𝐵 /
𝐸))) |
| 101 | 3, 16 | rpdivcld 13094 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 / 𝐸) ∈
ℝ+) |
| 102 | 101 | rpred 13077 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 / 𝐸) ∈ ℝ) |
| 103 | 102 | relogefd 26670 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(log‘(exp‘(𝐵 /
𝐸))) = (𝐵 / 𝐸)) |
| 104 | 100, 103 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘𝐾) = (𝐵 / 𝐸)) |
| 105 | 104 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) = ((log‘𝑍) / (𝐵 / 𝐸))) |
| 106 | 39 | rpcnd 13079 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) |
| 107 | 3 | rpcnne0d 13086 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
| 108 | 16 | rpcnne0d 13086 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) |
| 109 | | divdiv2 11979 |
. . . . . . . . . . . . 13
⊢
(((log‘𝑍)
∈ ℂ ∧ (𝐵
∈ ℂ ∧ 𝐵 ≠
0) ∧ (𝐸 ∈ ℂ
∧ 𝐸 ≠ 0)) →
((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵)) |
| 110 | 106, 107,
108, 109 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵)) |
| 111 | 105, 110 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) = (((log‘𝑍) · 𝐸) / 𝐵)) |
| 112 | 111 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵))) |
| 113 | 16 | rpcnd 13079 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 114 | 106, 113 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑍) · 𝐸) ∈ ℂ) |
| 115 | | divass 11940 |
. . . . . . . . . . 11
⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) · 𝐸) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵))) |
| 116 | 84, 114, 107, 115 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵))) |
| 117 | 15 | rpcnd 13079 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ℂ) |
| 118 | 117, 113,
106, 113 | mul4d 11473 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸))) |
| 119 | 113 | sqvald 14183 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸)) |
| 120 | 119 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸))) |
| 121 | 113 | sqcld 14184 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
| 122 | 117, 106,
121 | mul32d 11471 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍))) |
| 123 | 118, 120,
122 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍))) |
| 124 | 123 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵)) |
| 125 | 112, 116,
124 | 3eqtr2d 2783 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵)) |
| 126 | | 8t4e32 12850 |
. . . . . . . . . 10
⊢ (8
· 4) = ;32 |
| 127 | 126 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (8 · 4) = ;32) |
| 128 | 125, 127 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)) = ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / ;32)) |
| 129 | 20 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ) |
| 130 | 129, 106 | mulcld 11281 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈
ℂ) |
| 131 | | rpcnne0 13053 |
. . . . . . . . . . 11
⊢ (;32 ∈ ℝ+ →
(;32 ∈ ℂ ∧ ;32 ≠ 0)) |
| 132 | 25, 131 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (;32 ∈ ℂ ∧ ;32 ≠ 0)) |
| 133 | | divdiv1 11978 |
. . . . . . . . . 10
⊢ ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (;32 ∈ ℂ ∧ ;32 ≠ 0)) → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / ;32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · ;32))) |
| 134 | 130, 107,
132, 133 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / ;32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · ;32))) |
| 135 | 23 | nncni 12276 |
. . . . . . . . . . 11
⊢ ;32 ∈ ℂ |
| 136 | 3 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 137 | | mulcom 11241 |
. . . . . . . . . . 11
⊢ ((;32 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (;32 · 𝐵) = (𝐵 · ;32)) |
| 138 | 135, 136,
137 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (;32 · 𝐵) = (𝐵 · ;32)) |
| 139 | 138 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (;32 · 𝐵)) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · ;32))) |
| 140 | 27 | rpcnne0d 13086 |
. . . . . . . . . 10
⊢ (𝜑 → ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) |
| 141 | | div23 11941 |
. . . . . . . . . 10
⊢ (((𝐿 · (𝐸↑2)) ∈ ℂ ∧
(log‘𝑍) ∈
ℂ ∧ ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (;32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍))) |
| 142 | 129, 106,
140, 141 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (;32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍))) |
| 143 | 134, 139,
142 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / ;32) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍))) |
| 144 | 99, 128, 143 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍))) |
| 145 | 144 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)) = ((((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍))) |
| 146 | 50 | rpcnd 13079 |
. . . . . . 7
⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℂ) |
| 147 | 89 | rpred 13077 |
. . . . . . . . 9
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ) |
| 148 | | 4nn 12349 |
. . . . . . . . 9
⊢ 4 ∈
ℕ |
| 149 | | nndivre 12307 |
. . . . . . . . 9
⊢
((((log‘𝑍) /
(log‘𝐾)) ∈
ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) |
| 150 | 147, 148,
149 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) |
| 151 | 150 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℂ) |
| 152 | 146, 106,
151 | mul32d 11471 |
. . . . . 6
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍))) |
| 153 | 106 | sqvald 14183 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍))) |
| 154 | 153 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍)))) |
| 155 | 28 | rpcnd 13079 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) ∈ ℂ) |
| 156 | 155, 106,
106 | mulassd 11284 |
. . . . . . 7
⊢ (𝜑 → ((((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍)))) |
| 157 | 154, 156 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) = ((((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍))) |
| 158 | 145, 152,
157 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) |
| 159 | 56 | simp3d 1145 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)) |
| 160 | 150, 63, 51 | lemul2d 13121 |
. . . . . 6
⊢ (𝜑 → ((((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀) ↔ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀)))) |
| 161 | 159, 160 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀))) |
| 162 | 158, 161 | eqbrtrrd 5167 |
. . . 4
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀))) |
| 163 | 42 | rpred 13077 |
. . . . 5
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ) |
| 164 | 51 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ) |
| 165 | 164, 63 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀)) ∈ ℝ) |
| 166 | 163, 165,
13 | lemul2d 13121 |
. . . 4
⊢ (𝜑 → ((((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀)) ↔ ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈 − 𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀))))) |
| 167 | 162, 166 | mpbid 232 |
. . 3
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈 − 𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀)))) |
| 168 | 13 | rpcnd 13079 |
. . . 4
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) |
| 169 | 51 | rpcnd 13079 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℂ) |
| 170 | 63 | recnd 11289 |
. . . 4
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℂ) |
| 171 | 168, 169,
170 | mulassd 11284 |
. . 3
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) = ((𝑈 − 𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁 − 𝑀)))) |
| 172 | 167, 171 | breqtrrd 5171 |
. 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀))) |
| 173 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin) |
| 174 | 60 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 175 | 85, 174 | rpexpcld 14286 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾↑𝑁) ∈
ℝ+) |
| 176 | 35, 175 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑍 / (𝐾↑𝑁)) ∈
ℝ+) |
| 177 | 176 | rprege0d 13084 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑍 / (𝐾↑𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑𝑁)))) |
| 178 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ (((𝑍 / (𝐾↑𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑𝑁))) → (⌊‘(𝑍 / (𝐾↑𝑁))) ∈
ℕ0) |
| 179 | | nn0p1nn 12565 |
. . . . . . . . 9
⊢
((⌊‘(𝑍 /
(𝐾↑𝑁))) ∈ ℕ0 →
((⌊‘(𝑍 / (𝐾↑𝑁))) + 1) ∈ ℕ) |
| 180 | 177, 178,
179 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝑍 / (𝐾↑𝑁))) + 1) ∈ ℕ) |
| 181 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 182 | 180, 181 | eleqtrdi 2851 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑍 / (𝐾↑𝑁))) + 1) ∈
(ℤ≥‘1)) |
| 183 | | fzss1 13603 |
. . . . . . 7
⊢
(((⌊‘(𝑍
/ (𝐾↑𝑁))) + 1) ∈
(ℤ≥‘1) → (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 184 | 182, 183 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 185 | 184 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) |
| 186 | 185, 82 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 187 | 173, 186 | fsumrecl 15770 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 188 | | eluzfz2 13572 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
| 189 | 58, 188 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
| 190 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑚 − 𝑀) = (𝑀 − 𝑀)) |
| 191 | 190 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀))) |
| 192 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (𝐾↑𝑚) = (𝐾↑𝑀)) |
| 193 | 192 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (𝑍 / (𝐾↑𝑚)) = (𝑍 / (𝐾↑𝑀))) |
| 194 | 193 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (⌊‘(𝑍 / (𝐾↑𝑚))) = (⌊‘(𝑍 / (𝐾↑𝑀)))) |
| 195 | 194 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ((⌊‘(𝑍 / (𝐾↑𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)) |
| 196 | 195 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 197 | 196 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 198 | 191, 197 | breq12d 5156 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 199 | 198 | imbi2d 340 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 200 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑗 → (𝑚 − 𝑀) = (𝑗 − 𝑀)) |
| 201 | 200 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) |
| 202 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑗 → (𝐾↑𝑚) = (𝐾↑𝑗)) |
| 203 | 202 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑗 → (𝑍 / (𝐾↑𝑚)) = (𝑍 / (𝐾↑𝑗))) |
| 204 | 203 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (⌊‘(𝑍 / (𝐾↑𝑚))) = (⌊‘(𝑍 / (𝐾↑𝑗)))) |
| 205 | 204 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑗 → ((⌊‘(𝑍 / (𝐾↑𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)) |
| 206 | 205 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑗 → (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 207 | 206 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 208 | 201, 207 | breq12d 5156 |
. . . . . 6
⊢ (𝑚 = 𝑗 → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 209 | 208 | imbi2d 340 |
. . . . 5
⊢ (𝑚 = 𝑗 → ((𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 210 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = (𝑗 + 1) → (𝑚 − 𝑀) = ((𝑗 + 1) − 𝑀)) |
| 211 | 210 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = (𝑗 + 1) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀))) |
| 212 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑗 + 1) → (𝐾↑𝑚) = (𝐾↑(𝑗 + 1))) |
| 213 | 212 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑗 + 1) → (𝑍 / (𝐾↑𝑚)) = (𝑍 / (𝐾↑(𝑗 + 1)))) |
| 214 | 213 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑗 + 1) → (⌊‘(𝑍 / (𝐾↑𝑚))) = (⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))) |
| 215 | 214 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = (𝑗 + 1) → ((⌊‘(𝑍 / (𝐾↑𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)) |
| 216 | 215 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = (𝑗 + 1) → (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 217 | 216 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑚 = (𝑗 + 1) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 218 | 211, 217 | breq12d 5156 |
. . . . . 6
⊢ (𝑚 = (𝑗 + 1) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 219 | 218 | imbi2d 340 |
. . . . 5
⊢ (𝑚 = (𝑗 + 1) → ((𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 220 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (𝑚 − 𝑀) = (𝑁 − 𝑀)) |
| 221 | 220 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀))) |
| 222 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑁 → (𝐾↑𝑚) = (𝐾↑𝑁)) |
| 223 | 222 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → (𝑍 / (𝐾↑𝑚)) = (𝑍 / (𝐾↑𝑁))) |
| 224 | 223 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (⌊‘(𝑍 / (𝐾↑𝑚))) = (⌊‘(𝑍 / (𝐾↑𝑁)))) |
| 225 | 224 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((⌊‘(𝑍 / (𝐾↑𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)) |
| 226 | 225 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 227 | 226 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 228 | 221, 227 | breq12d 5156 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 229 | 228 | imbi2d 340 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 230 | 57 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 231 | 230 | subidd 11608 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 𝑀) = 0) |
| 232 | 231 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0)) |
| 233 | 52 | rpcnd 13079 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ) |
| 234 | 233 | mul01d 11460 |
. . . . . . . 8
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0) = 0) |
| 235 | 232, 234 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) = 0) |
| 236 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin) |
| 237 | 57 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 238 | 85, 237 | rpexpcld 14286 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾↑𝑀) ∈
ℝ+) |
| 239 | 35, 238 | rpdivcld 13094 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍 / (𝐾↑𝑀)) ∈
ℝ+) |
| 240 | 239 | rprege0d 13084 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑍 / (𝐾↑𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑𝑀)))) |
| 241 | | flge0nn0 13860 |
. . . . . . . . . . . . 13
⊢ (((𝑍 / (𝐾↑𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑𝑀))) → (⌊‘(𝑍 / (𝐾↑𝑀))) ∈
ℕ0) |
| 242 | | nn0p1nn 12565 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑍 /
(𝐾↑𝑀))) ∈ ℕ0 →
((⌊‘(𝑍 / (𝐾↑𝑀))) + 1) ∈ ℕ) |
| 243 | 240, 241,
242 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(𝑍 / (𝐾↑𝑀))) + 1) ∈ ℕ) |
| 244 | 243, 181 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘(𝑍 / (𝐾↑𝑀))) + 1) ∈
(ℤ≥‘1)) |
| 245 | | fzss1 13603 |
. . . . . . . . . . 11
⊢
(((⌊‘(𝑍
/ (𝐾↑𝑀))) + 1) ∈
(ℤ≥‘1) → (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 246 | 244, 245 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 247 | 246 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) |
| 248 | 247, 82 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 249 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌))) |
| 250 | 249 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌))) |
| 251 | 29 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
| 252 | 35, 251 | rpdivcld 13094 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍 / 𝑌) ∈
ℝ+) |
| 253 | 252 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ) |
| 254 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌))) → 𝑛 ∈
ℤ) |
| 255 | | flge 13845 |
. . . . . . . . . . . . 13
⊢ (((𝑍 / 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))) |
| 256 | 253, 254,
255 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))) |
| 257 | 250, 256 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (𝑍 / 𝑌)) |
| 258 | 71, 257 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) |
| 259 | | pntlem1.U |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) |
| 260 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259 | pntlemn 27644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 261 | 258, 260 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 262 | 247, 261 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 263 | 236, 248,
262 | fsumge0 15831 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 264 | 235, 263 | eqbrtrd 5165 |
. . . . . 6
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 265 | 264 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 266 | | pntlem1.K |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
| 267 | | eqid 2737 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑍
/ (𝐾↑(𝑗 + 1)))) +
1)...(⌊‘(𝑍 /
(𝐾↑𝑗)))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) |
| 268 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259, 266, 267 | pntlemi 27648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 269 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈
ℝ+) |
| 270 | 269 | rpred 13077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ) |
| 271 | | elfzoelz 13699 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ ℤ) |
| 272 | 271 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ) |
| 273 | 272 | zred 12722 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℝ) |
| 274 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℕ) |
| 275 | 274 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
| 276 | 273, 275 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 − 𝑀) ∈ ℝ) |
| 277 | 270, 276 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ∈ ℝ) |
| 278 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∈ Fin) |
| 279 | | ssun1 4178 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(𝑍
/ (𝐾↑(𝑗 + 1)))) +
1)...(⌊‘(𝑍 /
(𝐾↑𝑗)))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 280 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ) |
| 281 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈
ℝ+) |
| 282 | 272 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ ℤ) |
| 283 | 281, 282 | rpexpcld 14286 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑(𝑗 + 1)) ∈
ℝ+) |
| 284 | 280, 283 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ) |
| 285 | 281, 272 | rpexpcld 14286 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑𝑗) ∈
ℝ+) |
| 286 | 280, 285 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑𝑗)) ∈ ℝ) |
| 287 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ) |
| 288 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
| 289 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ) → (1 < 𝐾 → 1 ≤ 𝐾)) |
| 290 | 288, 86, 289 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 < 𝐾 → 1 ≤ 𝐾)) |
| 291 | 87, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐾) |
| 292 | 291 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 1 ≤ 𝐾) |
| 293 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 294 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 295 | 272, 293,
294 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 296 | 287, 292,
295 | leexp2ad 14293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑𝑗) ≤ (𝐾↑(𝑗 + 1))) |
| 297 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈
ℝ+) |
| 298 | 285, 283,
297 | lediv2d 13101 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝐾↑𝑗) ≤ (𝐾↑(𝑗 + 1)) ↔ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾↑𝑗)))) |
| 299 | 296, 298 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾↑𝑗))) |
| 300 | | flword2 13853 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ (𝑍 / (𝐾↑𝑗)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾↑𝑗))) → (⌊‘(𝑍 / (𝐾↑𝑗))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))))) |
| 301 | 284, 286,
299, 300 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾↑𝑗))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))))) |
| 302 | | eluzp1p1 12906 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘(𝑍 /
(𝐾↑𝑗))) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))) → ((⌊‘(𝑍 / (𝐾↑𝑗))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1))) |
| 303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑𝑗))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1))) |
| 304 | 286 | flcld 13838 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾↑𝑗))) ∈ ℤ) |
| 305 | 252 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈
ℝ+) |
| 306 | 305 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ) |
| 307 | 306 | flcld 13838 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ ℤ) |
| 308 | 251 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈
ℝ+) |
| 309 | 308 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ) |
| 310 | 285 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑𝑗) ∈ ℝ) |
| 311 | 30 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
| 312 | 311 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 313 | 312 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) |
| 314 | 30 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 < 𝑋) |
| 315 | 314 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < 𝑋) |
| 316 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
| 317 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemh 27643 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝑗) ∧ (𝐾↑𝑗) ≤ (√‘𝑍))) |
| 318 | 316, 317 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑋 < (𝐾↑𝑗) ∧ (𝐾↑𝑗) ≤ (√‘𝑍))) |
| 319 | 318 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑋 < (𝐾↑𝑗)) |
| 320 | 309, 313,
310, 315, 319 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < (𝐾↑𝑗)) |
| 321 | 309, 310,
320 | ltled 11409 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ≤ (𝐾↑𝑗)) |
| 322 | 308, 285,
297 | lediv2d 13101 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑌 ≤ (𝐾↑𝑗) ↔ (𝑍 / (𝐾↑𝑗)) ≤ (𝑍 / 𝑌))) |
| 323 | 321, 322 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑𝑗)) ≤ (𝑍 / 𝑌)) |
| 324 | | flwordi 13852 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑍 / (𝐾↑𝑗)) ∈ ℝ ∧ (𝑍 / 𝑌) ∈ ℝ ∧ (𝑍 / (𝐾↑𝑗)) ≤ (𝑍 / 𝑌)) → (⌊‘(𝑍 / (𝐾↑𝑗))) ≤ (⌊‘(𝑍 / 𝑌))) |
| 325 | 286, 306,
323, 324 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾↑𝑗))) ≤ (⌊‘(𝑍 / 𝑌))) |
| 326 | | eluz2 12884 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘(𝑍 /
𝑌)) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑𝑗)))) ↔ ((⌊‘(𝑍 / (𝐾↑𝑗))) ∈ ℤ ∧
(⌊‘(𝑍 / 𝑌)) ∈ ℤ ∧
(⌊‘(𝑍 / (𝐾↑𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))) |
| 327 | 304, 307,
325, 326 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑𝑗))))) |
| 328 | | fzsplit2 13589 |
. . . . . . . . . . . . . . . 16
⊢
((((⌊‘(𝑍
/ (𝐾↑𝑗))) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)) ∧ (⌊‘(𝑍 / 𝑌)) ∈
(ℤ≥‘(⌊‘(𝑍 / (𝐾↑𝑗))))) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))) |
| 329 | 303, 327,
328 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))) |
| 330 | 279, 329 | sseqtrrid 4027 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 331 | 297, 283 | rpdivcld 13094 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈
ℝ+) |
| 332 | 331 | rprege0d 13084 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1))))) |
| 333 | | flge0nn0 13860 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈
ℕ0) |
| 334 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘(𝑍 /
(𝐾↑(𝑗 + 1)))) ∈ ℕ0 →
((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈
ℕ) |
| 335 | 332, 333,
334 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈
ℕ) |
| 336 | 335, 181 | eleqtrdi 2851 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈
(ℤ≥‘1)) |
| 337 | | fzss1 13603 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(𝑍
/ (𝐾↑(𝑗 + 1)))) + 1) ∈
(ℤ≥‘1) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 338 | 336, 337 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 339 | 330, 338 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 340 | 339 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) |
| 341 | 82 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 342 | 340, 341 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 343 | 278, 342 | fsumrecl 15770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 344 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin) |
| 345 | | ssun2 4179 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(𝑍
/ (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 346 | 345, 329 | sseqtrrid 4027 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) |
| 347 | 346, 338 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌)))) |
| 348 | 347 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) |
| 349 | 348, 341 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 350 | 344, 349 | fsumrecl 15770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 351 | | le2add 11745 |
. . . . . . . . . 10
⊢
(((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ ∧ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ∈ ℝ) ∧ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ ∧ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∧ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 352 | 270, 277,
343, 350, 351 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∧ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 353 | 268, 352 | mpand 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 354 | 233 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ) |
| 355 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) |
| 356 | 272 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ) |
| 357 | 230 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ) |
| 358 | 356, 357 | subcld 11620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 − 𝑀) ∈ ℂ) |
| 359 | 354, 355,
358 | adddid 11285 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗 − 𝑀))) = ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)))) |
| 360 | 355, 358 | addcomd 11463 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗 − 𝑀)) = ((𝑗 − 𝑀) + 1)) |
| 361 | 356, 355,
357 | addsubd 11641 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 + 1) − 𝑀) = ((𝑗 − 𝑀) + 1)) |
| 362 | 360, 361 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗 − 𝑀)) = ((𝑗 + 1) − 𝑀)) |
| 363 | 362 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗 − 𝑀))) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀))) |
| 364 | 354 | mulridd 11278 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) = ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍)))) |
| 365 | 364 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)))) |
| 366 | 359, 363,
365 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) = (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)))) |
| 367 | | reflcl 13836 |
. . . . . . . . . . . . 13
⊢ ((𝑍 / (𝐾↑𝑗)) ∈ ℝ →
(⌊‘(𝑍 / (𝐾↑𝑗))) ∈ ℝ) |
| 368 | 286, 367 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾↑𝑗))) ∈ ℝ) |
| 369 | 368 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾↑𝑗))) < ((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)) |
| 370 | | fzdisj 13591 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑍 /
(𝐾↑𝑗))) < ((⌊‘(𝑍 / (𝐾↑𝑗))) + 1) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅) |
| 371 | 369, 370 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅) |
| 372 | | fzfid 14014 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin) |
| 373 | 338 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) |
| 374 | 373, 341 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) |
| 375 | 374 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℂ) |
| 376 | 371, 329,
372, 375 | fsumsplit 15777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 377 | 366, 376 | breq12d 5156 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 378 | 353, 377 | sylibrd 259 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 379 | 378 | expcom 413 |
. . . . . 6
⊢ (𝑗 ∈ (𝑀..^𝑁) → (𝜑 → ((((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 380 | 379 | a2d 29 |
. . . . 5
⊢ (𝑗 ∈ (𝑀..^𝑁) → ((𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) → (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) |
| 381 | 199, 209,
219, 229, 265, 380 | fzind2 13824 |
. . . 4
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) |
| 382 | 189, 381 | mpcom 38 |
. . 3
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 383 | 65, 82, 261, 184 | fsumless 15832 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 384 | 64, 187, 83, 382, 383 | letrd 11418 |
. 2
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁 − 𝑀)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |
| 385 | 44, 64, 83, 172, 384 | letrd 11418 |
1
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) |