MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlemf Structured version   Visualization version   GIF version

Theorem pntlemf 25585
Description: Lemma for pnt 25594. Add up the pieces in pntlemi 25584 to get an estimate slightly better than the naive lower bound 0. (Contributed by Mario Carneiro, 13-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntlem1.a (𝜑𝐴 ∈ ℝ+)
pntlem1.b (𝜑𝐵 ∈ ℝ+)
pntlem1.l (𝜑𝐿 ∈ (0(,)1))
pntlem1.d 𝐷 = (𝐴 + 1)
pntlem1.f 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))
pntlem1.u (𝜑𝑈 ∈ ℝ+)
pntlem1.u2 (𝜑𝑈𝐴)
pntlem1.e 𝐸 = (𝑈 / 𝐷)
pntlem1.k 𝐾 = (exp‘(𝐵 / 𝐸))
pntlem1.y (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
pntlem1.x (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))
pntlem1.c (𝜑𝐶 ∈ ℝ+)
pntlem1.w 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))
pntlem1.z (𝜑𝑍 ∈ (𝑊[,)+∞))
pntlem1.m 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
pntlem1.n 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
pntlem1.U (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)
pntlem1.K (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
Assertion
Ref Expression
pntlemf (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Distinct variable groups:   𝑧,𝐶   𝑦,𝑛,𝑧,𝑢,𝐿   𝑛,𝐾,𝑦,𝑧   𝑛,𝑀,𝑧   𝜑,𝑛   𝑛,𝑁,𝑧   𝑅,𝑛,𝑢,𝑦,𝑧   𝑈,𝑛,𝑧   𝑛,𝑊,𝑧   𝑛,𝑋,𝑦,𝑧   𝑛,𝑌,𝑧   𝑛,𝑎,𝑢,𝑦,𝑧,𝐸   𝑛,𝑍,𝑢,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑢,𝑎)   𝐴(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐵(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐶(𝑦,𝑢,𝑛,𝑎)   𝐷(𝑦,𝑧,𝑢,𝑛,𝑎)   𝑅(𝑎)   𝑈(𝑦,𝑢,𝑎)   𝐹(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐾(𝑢,𝑎)   𝐿(𝑎)   𝑀(𝑦,𝑢,𝑎)   𝑁(𝑦,𝑢,𝑎)   𝑊(𝑦,𝑢,𝑎)   𝑋(𝑢,𝑎)   𝑌(𝑦,𝑢,𝑎)   𝑍(𝑦,𝑎)

Proof of Theorem pntlemf
Dummy variables 𝑗 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef 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‘(𝐵 / 𝐸))
111, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 25575 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1174 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1174 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 25574 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1172 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1172 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
17 2z 11656 . . . . . . . 8 2 ∈ ℤ
18 rpexpcl 13086 . . . . . . . 8 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
1916, 17, 18sylancl 580 . . . . . . 7 (𝜑 → (𝐸↑2) ∈ ℝ+)
2015, 19rpmulcld 12086 . . . . . 6 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
21 3nn0 11558 . . . . . . . . 9 3 ∈ ℕ0
22 2nn 11345 . . . . . . . . 9 2 ∈ ℕ
2321, 22decnncl 11761 . . . . . . . 8 32 ∈ ℕ
24 nnrp 12041 . . . . . . . 8 (32 ∈ ℕ → 32 ∈ ℝ+)
2523, 24ax-mp 5 . . . . . . 7 32 ∈ ℝ+
26 rpmulcl 12053 . . . . . . 7 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
2725, 3, 26sylancr 581 . . . . . 6 (𝜑 → (32 · 𝐵) ∈ ℝ+)
2820, 27rpdivcld 12087 . . . . 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 (𝜑𝑍 ∈ (𝑊[,)+∞))
341, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33pntlemb 25577 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
3534simp1d 1172 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
3635rpred 12070 . . . . . . 7 (𝜑𝑍 ∈ ℝ)
3734simp2d 1173 . . . . . . . 8 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3837simp1d 1172 . . . . . . 7 (𝜑 → 1 < 𝑍)
3936, 38rplogcld 24666 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℝ+)
40 rpexpcl 13086 . . . . . 6 (((log‘𝑍) ∈ ℝ+ ∧ 2 ∈ ℤ) → ((log‘𝑍)↑2) ∈ ℝ+)
4139, 17, 40sylancl 580 . . . . 5 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ+)
4228, 41rpmulcld 12086 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ+)
4313, 42rpmulcld 12086 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ+)
4443rpred 12070 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
4515, 16rpmulcld 12086 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
46 8re 11373 . . . . . . . 8 8 ∈ ℝ
47 8pos 11391 . . . . . . . 8 0 < 8
4846, 47elrpii 12031 . . . . . . 7 8 ∈ ℝ+
49 rpdivcl 12054 . . . . . . 7 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5045, 48, 49sylancl 580 . . . . . 6 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5150, 39rpmulcld 12086 . . . . 5 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
5213, 51rpmulcld 12086 . . . 4 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
5352rpred 12070 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
54 pntlem1.m . . . . . . . 8 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
55 pntlem1.n . . . . . . . 8 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
561, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemg 25578 . . . . . . 7 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
5756simp1d 1172 . . . . . 6 (𝜑𝑀 ∈ ℕ)
5856simp2d 1173 . . . . . 6 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluznn 11959 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑁 ∈ ℕ)
6057, 58, 59syl2anc 579 . . . . 5 (𝜑𝑁 ∈ ℕ)
6160nnred 11291 . . . 4 (𝜑𝑁 ∈ ℝ)
6257nnred 11291 . . . 4 (𝜑𝑀 ∈ ℝ)
6361, 62resubcld 10712 . . 3 (𝜑 → (𝑁𝑀) ∈ ℝ)
6453, 63remulcld 10324 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ∈ ℝ)
65 fzfid 12980 . . 3 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
667rpred 12070 . . . . . 6 (𝜑𝑈 ∈ ℝ)
67 elfznn 12577 . . . . . 6 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
68 nndivre 11313 . . . . . 6 ((𝑈 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑈 / 𝑛) ∈ ℝ)
6966, 67, 68syl2an 589 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
7035adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
7167adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
7271nnrpd 12068 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
7370, 72rpdivcld 12087 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 25543 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelrni 6548 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 70rerpdivcld 12101 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 10322 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 14462 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8069, 79resubcld 10712 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 24660 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 10324 . . 3 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8365, 82fsumrecl 14752 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8445rpcnd 12072 . . . . . . . . 9 (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
8511simp2d 1173 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ+)
8685rpred 12070 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
8712simp2d 1173 . . . . . . . . . . . 12 (𝜑 → 1 < 𝐾)
8886, 87rplogcld 24666 . . . . . . . . . . 11 (𝜑 → (log‘𝐾) ∈ ℝ+)
8939, 88rpdivcld 12087 . . . . . . . . . 10 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ+)
9089rpcnd 12072 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℂ)
91 rpcnne0 12048 . . . . . . . . . 10 (8 ∈ ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0))
9248, 91mp1i 13 . . . . . . . . 9 (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
93 4re 11357 . . . . . . . . . . 11 4 ∈ ℝ
94 4pos 11386 . . . . . . . . . . 11 0 < 4
9593, 94elrpii 12031 . . . . . . . . . 10 4 ∈ ℝ+
96 rpcnne0 12048 . . . . . . . . . 10 (4 ∈ ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0))
9795, 96mp1i 13 . . . . . . . . 9 (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
98 divmuldiv 10979 . . . . . . . . 9 ((((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) / (log‘𝐾)) ∈ ℂ) ∧ ((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0))) → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)))
9984, 90, 92, 97, 98syl22anc 867 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)))
10010fveq2i 6378 . . . . . . . . . . . . . 14 (log‘𝐾) = (log‘(exp‘(𝐵 / 𝐸)))
1013, 16rpdivcld 12087 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐸) ∈ ℝ+)
102101rpred 12070 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / 𝐸) ∈ ℝ)
103102relogefd 24665 . . . . . . . . . . . . . 14 (𝜑 → (log‘(exp‘(𝐵 / 𝐸))) = (𝐵 / 𝐸))
104100, 103syl5eq 2811 . . . . . . . . . . . . 13 (𝜑 → (log‘𝐾) = (𝐵 / 𝐸))
105104oveq2d 6858 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = ((log‘𝑍) / (𝐵 / 𝐸)))
10639rpcnd 12072 . . . . . . . . . . . . 13 (𝜑 → (log‘𝑍) ∈ ℂ)
1073rpcnne0d 12079 . . . . . . . . . . . . 13 (𝜑 → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
10816rpcnne0d 12079 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
109 divdiv2 10991 . . . . . . . . . . . . 13 (((log‘𝑍) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
110106, 107, 108, 109syl3anc 1490 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
111105, 110eqtrd 2799 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = (((log‘𝑍) · 𝐸) / 𝐵))
112111oveq2d 6858 . . . . . . . . . 10 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11316rpcnd 12072 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
114106, 113mulcld 10314 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) · 𝐸) ∈ ℂ)
115 divass 10957 . . . . . . . . . . 11 (((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) · 𝐸) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11684, 114, 107, 115syl3anc 1490 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11715rpcnd 12072 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℂ)
118117, 113, 106, 113mul4d 10502 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
119113sqvald 13212 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
120119oveq2d 6858 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
121113sqcld 13213 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) ∈ ℂ)
122117, 106, 121mul32d 10500 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
123118, 120, 1223eqtr2d 2805 . . . . . . . . . . 11 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
124123oveq1d 6857 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
125112, 116, 1243eqtr2d 2805 . . . . . . . . 9 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
126 8t4e32 11858 . . . . . . . . . 10 (8 · 4) = 32
127126a1i 11 . . . . . . . . 9 (𝜑 → (8 · 4) = 32)
128125, 127oveq12d 6860 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)) = ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32))
12920rpcnd 12072 . . . . . . . . . . 11 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ)
130129, 106mulcld 10314 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ)
131 rpcnne0 12048 . . . . . . . . . . 11 (32 ∈ ℝ+ → (32 ∈ ℂ ∧ 32 ≠ 0))
13225, 131mp1i 13 . . . . . . . . . 10 (𝜑 → (32 ∈ ℂ ∧ 32 ≠ 0))
133 divdiv1 10990 . . . . . . . . . 10 ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (32 ∈ ℂ ∧ 32 ≠ 0)) → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
134130, 107, 132, 133syl3anc 1490 . . . . . . . . 9 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
13523nncni 11285 . . . . . . . . . . 11 32 ∈ ℂ
1363rpcnd 12072 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
137 mulcom 10275 . . . . . . . . . . 11 ((32 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (32 · 𝐵) = (𝐵 · 32))
138135, 136, 137sylancr 581 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) = (𝐵 · 32))
139138oveq2d 6858 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
14027rpcnne0d 12079 . . . . . . . . . 10 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
141 div23 10958 . . . . . . . . . 10 (((𝐿 · (𝐸↑2)) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
142129, 106, 140, 141syl3anc 1490 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
143134, 139, 1423eqtr2d 2805 . . . . . . . 8 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
14499, 128, 1433eqtrd 2803 . . . . . . 7 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
145144oveq1d 6857 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
14650rpcnd 12072 . . . . . . 7 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℂ)
14789rpred 12070 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ)
148 4nn 11356 . . . . . . . . 9 4 ∈ ℕ
149 nndivre 11313 . . . . . . . . 9 ((((log‘𝑍) / (log‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
150147, 148, 149sylancl 580 . . . . . . . 8 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
151150recnd 10322 . . . . . . 7 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℂ)
152146, 106, 151mul32d 10500 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)))
153106sqvald 13212 . . . . . . . 8 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
154153oveq2d 6858 . . . . . . 7 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
15528rpcnd 12072 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
156155, 106, 106mulassd 10317 . . . . . . 7 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
157154, 156eqtr4d 2802 . . . . . 6 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
158145, 152, 1573eqtr4d 2809 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))
15956simp3d 1174 . . . . . 6 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀))
160150, 63, 51lemul2d 12114 . . . . . 6 (𝜑 → ((((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀) ↔ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
161159, 160mpbid 223 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
162158, 161eqbrtrrd 4833 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
16342rpred 12070 . . . . 5 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
16451rpred 12070 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
165164, 63remulcld 10324 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ∈ ℝ)
166163, 165, 13lemul2d 12114 . . . 4 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ↔ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))))
167162, 166mpbid 223 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
16813rpcnd 12072 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℂ)
16951rpcnd 12072 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℂ)
17063recnd 10322 . . . 4 (𝜑 → (𝑁𝑀) ∈ ℂ)
171168, 169, 170mulassd 10317 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) = ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
172167, 171breqtrrd 4837 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
173 fzfid 12980 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
17460nnzd 11728 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
17585, 174rpexpcld 13239 . . . . . . . . . . 11 (𝜑 → (𝐾𝑁) ∈ ℝ+)
17635, 175rpdivcld 12087 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝑁)) ∈ ℝ+)
177176rprege0d 12077 . . . . . . . . 9 (𝜑 → ((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))))
178 flge0nn0 12829 . . . . . . . . 9 (((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))) → (⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0)
179 nn0p1nn 11579 . . . . . . . . 9 ((⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
180177, 178, 1793syl 18 . . . . . . . 8 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
181 nnuz 11923 . . . . . . . 8 ℕ = (ℤ‘1)
182180, 181syl6eleq 2854 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1))
183 fzss1 12587 . . . . . . 7 (((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
184182, 183syl 17 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
185184sselda 3761 . . . . 5 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
186185, 82syldan 585 . . . 4 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
187173, 186fsumrecl 14752 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
188 eluzfz2 12556 . . . . 5 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
18958, 188syl 17 . . . 4 (𝜑𝑁 ∈ (𝑀...𝑁))
190 oveq1 6849 . . . . . . . 8 (𝑚 = 𝑀 → (𝑚𝑀) = (𝑀𝑀))
191190oveq2d 6858 . . . . . . 7 (𝑚 = 𝑀 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)))
192 oveq2 6850 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝐾𝑚) = (𝐾𝑀))
193192oveq2d 6858 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑀)))
194193fveq2d 6379 . . . . . . . . . 10 (𝑚 = 𝑀 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑀))))
195194oveq1d 6857 . . . . . . . . 9 (𝑚 = 𝑀 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑀))) + 1))
196195oveq1d 6857 . . . . . . . 8 (𝑚 = 𝑀 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))))
197196sumeq1d 14718 . . . . . . 7 (𝑚 = 𝑀 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
198191, 197breq12d 4822 . . . . . 6 (𝑚 = 𝑀 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
199198imbi2d 331 . . . . 5 (𝑚 = 𝑀 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
200 oveq1 6849 . . . . . . . 8 (𝑚 = 𝑗 → (𝑚𝑀) = (𝑗𝑀))
201200oveq2d 6858 . . . . . . 7 (𝑚 = 𝑗 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)))
202 oveq2 6850 . . . . . . . . . . . 12 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
203202oveq2d 6858 . . . . . . . . . . 11 (𝑚 = 𝑗 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑗)))
204203fveq2d 6379 . . . . . . . . . 10 (𝑚 = 𝑗 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑗))))
205204oveq1d 6857 . . . . . . . . 9 (𝑚 = 𝑗 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
206205oveq1d 6857 . . . . . . . 8 (𝑚 = 𝑗 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
207206sumeq1d 14718 . . . . . . 7 (𝑚 = 𝑗 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
208201, 207breq12d 4822 . . . . . 6 (𝑚 = 𝑗 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
209208imbi2d 331 . . . . 5 (𝑚 = 𝑗 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
210 oveq1 6849 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (𝑚𝑀) = ((𝑗 + 1) − 𝑀))
211210oveq2d 6858 . . . . . . 7 (𝑚 = (𝑗 + 1) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
212 oveq2 6850 . . . . . . . . . . . 12 (𝑚 = (𝑗 + 1) → (𝐾𝑚) = (𝐾↑(𝑗 + 1)))
213212oveq2d 6858 . . . . . . . . . . 11 (𝑚 = (𝑗 + 1) → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾↑(𝑗 + 1))))
214213fveq2d 6379 . . . . . . . . . 10 (𝑚 = (𝑗 + 1) → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))))
215214oveq1d 6857 . . . . . . . . 9 (𝑚 = (𝑗 + 1) → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1))
216215oveq1d 6857 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
217216sumeq1d 14718 . . . . . . 7 (𝑚 = (𝑗 + 1) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
218211, 217breq12d 4822 . . . . . 6 (𝑚 = (𝑗 + 1) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
219218imbi2d 331 . . . . 5 (𝑚 = (𝑗 + 1) → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
220 oveq1 6849 . . . . . . . 8 (𝑚 = 𝑁 → (𝑚𝑀) = (𝑁𝑀))
221220oveq2d 6858 . . . . . . 7 (𝑚 = 𝑁 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
222 oveq2 6850 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝐾𝑚) = (𝐾𝑁))
223222oveq2d 6858 . . . . . . . . . . 11 (𝑚 = 𝑁 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑁)))
224223fveq2d 6379 . . . . . . . . . 10 (𝑚 = 𝑁 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑁))))
225224oveq1d 6857 . . . . . . . . 9 (𝑚 = 𝑁 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑁))) + 1))
226225oveq1d 6857 . . . . . . . 8 (𝑚 = 𝑁 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))))
227226sumeq1d 14718 . . . . . . 7 (𝑚 = 𝑁 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
228221, 227breq12d 4822 . . . . . 6 (𝑚 = 𝑁 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
229228imbi2d 331 . . . . 5 (𝑚 = 𝑁 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
23057nncnd 11292 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
231230subidd 10634 . . . . . . . . 9 (𝜑 → (𝑀𝑀) = 0)
232231oveq2d 6858 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0))
23352rpcnd 12072 . . . . . . . . 9 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
234233mul01d 10489 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0) = 0)
235232, 234eqtrd 2799 . . . . . . 7 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = 0)
236 fzfid 12980 . . . . . . . 8 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
23757nnzd 11728 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
23885, 237rpexpcld 13239 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾𝑀) ∈ ℝ+)
23935, 238rpdivcld 12087 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / (𝐾𝑀)) ∈ ℝ+)
240239rprege0d 12077 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))))
241 flge0nn0 12829 . . . . . . . . . . . . 13 (((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))) → (⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0)
242 nn0p1nn 11579 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
243240, 241, 2423syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
244243, 181syl6eleq 2854 . . . . . . . . . . 11 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1))
245 fzss1 12587 . . . . . . . . . . 11 (((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
246244, 245syl 17 . . . . . . . . . 10 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
247246sselda 3761 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
248247, 82syldan 585 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
249 elfzle2 12552 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
250249adantl 473 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
25129simpld 488 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ+)
25235, 251rpdivcld 12087 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
253252rpred 12070 . . . . . . . . . . . . 13 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
254 elfzelz 12549 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℤ)
255 flge 12814 . . . . . . . . . . . . 13 (((𝑍 / 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
256253, 254, 255syl2an 589 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
257250, 256mpbird 248 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (𝑍 / 𝑌))
25871, 257jca 507 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌)))
259 pntlem1.U . . . . . . . . . . 11 (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)
2601, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259pntlemn 25580 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
261258, 260syldan 585 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
262247, 261syldan 585 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
263236, 248, 262fsumge0 14813 . . . . . . 7 (𝜑 → 0 ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
264235, 263eqbrtrd 4831 . . . . . 6 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
265264a1i 11 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
266 pntlem1.K . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
267 eqid 2765 . . . . . . . . . 10 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))
2681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259, 266, 267pntlemi 25584 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
26952adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
270269rpred 12070 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
271 elfzoelz 12678 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ ℤ)
272271adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ)
273272zred 11729 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℝ)
27457adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℕ)
275274nnred 11291 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
276273, 275resubcld 10712 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℝ)
277270, 276remulcld 10324 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ∈ ℝ)
278 fzfid 12980 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∈ Fin)
279 ssun1 3938 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
28036adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ)
28185adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ+)
282272peano2zd 11732 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ ℤ)
283281, 282rpexpcld 13239 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑(𝑗 + 1)) ∈ ℝ+)
284280, 283rerpdivcld 12101 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ)
285281, 272rpexpcld 13239 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ+)
286280, 285rerpdivcld 12101 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ∈ ℝ)
28786adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ)
288 1re 10293 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
289 ltle 10380 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (1 < 𝐾 → 1 ≤ 𝐾))
290288, 86, 289sylancr 581 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 < 𝐾 → 1 ≤ 𝐾))
29187, 290mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐾)
292291adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ≤ 𝐾)
293 uzid 11901 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
294 peano2uz 11941 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
295272, 293, 2943syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ (ℤ𝑗))
296287, 292, 295leexp2ad 13248 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)))
29735adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ+)
298285, 283, 297lediv2d 12094 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)) ↔ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))))
299296, 298mpbid 223 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗)))
300 flword2 12822 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
301284, 286, 299, 300syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
302 eluzp1p1 11912 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
303301, 302syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
304286flcld 12807 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ)
305252adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ+)
306305rpred 12070 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ)
307306flcld 12807 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ ℤ)
308251adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ+)
309308rpred 12070 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ)
310285rpred 12070 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ)
31130simpld 488 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ+)
312311rpred 12070 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ)
313312adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)
31430simprd 489 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 < 𝑋)
315314adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < 𝑋)
316 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁))
3171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemh 25579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
318316, 317sylan2 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
319318simpld 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 < (𝐾𝑗))
320309, 313, 310, 315, 319lttrd 10452 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < (𝐾𝑗))
321309, 310, 320ltled 10439 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ≤ (𝐾𝑗))
322308, 285, 297lediv2d 12094 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑌 ≤ (𝐾𝑗) ↔ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)))
323321, 322mpbid 223 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌))
324 flwordi 12821 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / 𝑌) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
325286, 306, 323, 324syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
326 eluz2 11892 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))) ↔ ((⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ ∧ (⌊‘(𝑍 / 𝑌)) ∈ ℤ ∧ (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌))))
327304, 307, 325, 326syl3anbrc 1443 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))))
328 fzsplit2 12573 . . . . . . . . . . . . . . . 16 ((((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)) ∧ (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗))))) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
329303, 327, 328syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
330279, 329syl5sseqr 3814 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
331297, 283rpdivcld 12087 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ+)
332331rprege0d 12077 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))))
333 flge0nn0 12829 . . . . . . . . . . . . . . . . 17 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0)
334 nn0p1nn 11579 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
335332, 333, 3343syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
336335, 181syl6eleq 2854 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1))
337 fzss1 12587 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
338336, 337syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
339330, 338sstrd 3771 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
340339sselda 3761 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
34182adantlr 706 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
342340, 341syldan 585 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
343278, 342fsumrecl 14752 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
344 fzfid 12980 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
345 ssun2 3939 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
346345, 329syl5sseqr 3814 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
347346, 338sstrd 3771 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
348347sselda 3761 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
349348, 341syldan 585 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
350344, 349fsumrecl 14752 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
351 le2add 10764 . . . . . . . . . 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‘𝑛)))))
352270, 277, 343, 350, 351syl22anc 867 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∧ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
353268, 352mpand 686 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
354233adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
355 1cnd 10288 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ)
356272zcnd 11730 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ)
357230adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ)
358356, 357subcld 10646 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℂ)
359354, 355, 358adddid 10318 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
360355, 358addcomd 10492 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗𝑀) + 1))
361356, 355, 357addsubd 10667 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 + 1) − 𝑀) = ((𝑗𝑀) + 1))
362360, 361eqtr4d 2802 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗 + 1) − 𝑀))
363362oveq2d 6858 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
364354mulid1d 10311 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) = ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))))
365364oveq1d 6857 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
366359, 363, 3653eqtr3d 2807 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
367 reflcl 12805 . . . . . . . . . . . . 13 ((𝑍 / (𝐾𝑗)) ∈ ℝ → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
368286, 367syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
369368ltp1d 11208 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
370 fzdisj 12575 . . . . . . . . . . 11 ((⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
371369, 370syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
372 fzfid 12980 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
373338sselda 3761 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
374373, 341syldan 585 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
375374recnd 10322 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℂ)
376371, 329, 372, 375fsumsplit 14758 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
377366, 376breq12d 4822 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
378353, 377sylibrd 250 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
379378expcom 402 . . . . . 6 (𝑗 ∈ (𝑀..^𝑁) → (𝜑 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
380379a2d 29 . . . . 5 (𝑗 ∈ (𝑀..^𝑁) → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
381199, 209, 219, 229, 265, 380fzind2 12794 . . . 4 (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
382189, 381mpcom 38 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38365, 82, 261, 184fsumless 14814 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38464, 187, 83, 382, 383letrd 10448 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38544, 64, 83, 172, 384letrd 10448 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  cun 3730  cin 3731  wss 3732  c0 4079   class class class wbr 4809  cmpt 4888  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  +∞cpnf 10325   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  2c2 11327  3c3 11328  4c4 11329  8c8 11333  0cn0 11538  cz 11624  cdc 11740  cuz 11886  +crp 12028  (,)cioo 12377  [,)cico 12379  [,]cicc 12380  ...cfz 12533  ..^cfzo 12673  cfl 12799  cexp 13067  csqrt 14260  abscabs 14261  Σcsu 14703  expce 15076  eceu 15077  logclog 24592  ψcchp 25110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14094  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-limsup 14489  df-clim 14506  df-rlim 14507  df-sum 14704  df-ef 15082  df-e 15083  df-sin 15084  df-cos 15085  df-pi 15087  df-dvds 15268  df-gcd 15500  df-prm 15668  df-pc 15823  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-0g 16370  df-gsum 16371  df-topgen 16372  df-pt 16373  df-prds 16376  df-xrs 16430  df-qtop 16435  df-imas 16436  df-xps 16438  df-mre 16514  df-mrc 16515  df-acs 16517  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-submnd 17604  df-mulg 17810  df-cntz 18015  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922  df-log 24594  df-vma 25115  df-chp 25116
This theorem is referenced by:  pntlemo  25587
  Copyright terms: Public domain W3C validator