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

Theorem pntlemf 27649
Description: Lemma for pnt 27658. Add up the pieces in pntlemi 27648 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 27639 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1145 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1145 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 27638 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1143 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1143 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
17 2z 12649 . . . . . . . 8 2 ∈ ℤ
18 rpexpcl 14121 . . . . . . . 8 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
1916, 17, 18sylancl 586 . . . . . . 7 (𝜑 → (𝐸↑2) ∈ ℝ+)
2015, 19rpmulcld 13093 . . . . . 6 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
21 3nn0 12544 . . . . . . . . 9 3 ∈ ℕ0
22 2nn 12339 . . . . . . . . 9 2 ∈ ℕ
2321, 22decnncl 12753 . . . . . . . 8 32 ∈ ℕ
24 nnrp 13046 . . . . . . . 8 (32 ∈ ℕ → 32 ∈ ℝ+)
2523, 24ax-mp 5 . . . . . . 7 32 ∈ ℝ+
26 rpmulcl 13058 . . . . . . 7 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
2725, 3, 26sylancr 587 . . . . . 6 (𝜑 → (32 · 𝐵) ∈ ℝ+)
2820, 27rpdivcld 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 (𝜑𝑍 ∈ (𝑊[,)+∞))
341, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33pntlemb 27641 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
3534simp1d 1143 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
3635rpred 13077 . . . . . . 7 (𝜑𝑍 ∈ ℝ)
3734simp2d 1144 . . . . . . . 8 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3837simp1d 1143 . . . . . . 7 (𝜑 → 1 < 𝑍)
3936, 38rplogcld 26671 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℝ+)
40 rpexpcl 14121 . . . . . 6 (((log‘𝑍) ∈ ℝ+ ∧ 2 ∈ ℤ) → ((log‘𝑍)↑2) ∈ ℝ+)
4139, 17, 40sylancl 586 . . . . 5 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ+)
4228, 41rpmulcld 13093 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ+)
4313, 42rpmulcld 13093 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ+)
4443rpred 13077 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
4515, 16rpmulcld 13093 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
46 8re 12362 . . . . . . . 8 8 ∈ ℝ
47 8pos 12378 . . . . . . . 8 0 < 8
4846, 47elrpii 13037 . . . . . . 7 8 ∈ ℝ+
49 rpdivcl 13060 . . . . . . 7 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5045, 48, 49sylancl 586 . . . . . 6 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5150, 39rpmulcld 13093 . . . . 5 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
5213, 51rpmulcld 13093 . . . 4 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
5352rpred 13077 . . 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 27642 . . . . . . 7 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
5756simp1d 1143 . . . . . 6 (𝜑𝑀 ∈ ℕ)
5856simp2d 1144 . . . . . 6 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluznn 12960 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑁 ∈ ℕ)
6057, 58, 59syl2anc 584 . . . . 5 (𝜑𝑁 ∈ ℕ)
6160nnred 12281 . . . 4 (𝜑𝑁 ∈ ℝ)
6257nnred 12281 . . . 4 (𝜑𝑀 ∈ ℝ)
6361, 62resubcld 11691 . . 3 (𝜑 → (𝑁𝑀) ∈ ℝ)
6453, 63remulcld 11291 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ∈ ℝ)
65 fzfid 14014 . . 3 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
667rpred 13077 . . . . . 6 (𝜑𝑈 ∈ ℝ)
67 elfznn 13593 . . . . . 6 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
68 nndivre 12307 . . . . . 6 ((𝑈 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑈 / 𝑛) ∈ ℝ)
6966, 67, 68syl2an 596 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
7035adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
7167adantl 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
7271nnrpd 13075 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
7370, 72rpdivcld 13094 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 27607 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelcdmi 7103 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 70rerpdivcld 13108 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 11289 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 15475 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8069, 79resubcld 11691 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 26665 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 11291 . . 3 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8365, 82fsumrecl 15770 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8445rpcnd 13079 . . . . . . . . 9 (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
8511simp2d 1144 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ+)
8685rpred 13077 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
8712simp2d 1144 . . . . . . . . . . . 12 (𝜑 → 1 < 𝐾)
8886, 87rplogcld 26671 . . . . . . . . . . 11 (𝜑 → (log‘𝐾) ∈ ℝ+)
8939, 88rpdivcld 13094 . . . . . . . . . 10 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ+)
9089rpcnd 13079 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℂ)
91 rpcnne0 13053 . . . . . . . . . 10 (8 ∈ ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0))
9248, 91mp1i 13 . . . . . . . . 9 (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
93 4re 12350 . . . . . . . . . . 11 4 ∈ ℝ
94 4pos 12373 . . . . . . . . . . 11 0 < 4
9593, 94elrpii 13037 . . . . . . . . . 10 4 ∈ ℝ+
96 rpcnne0 13053 . . . . . . . . . 10 (4 ∈ ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0))
9795, 96mp1i 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)))
9984, 90, 92, 97, 98syl22anc 839 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)))
10010fveq2i 6909 . . . . . . . . . . . . . 14 (log‘𝐾) = (log‘(exp‘(𝐵 / 𝐸)))
1013, 16rpdivcld 13094 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐸) ∈ ℝ+)
102101rpred 13077 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / 𝐸) ∈ ℝ)
103102relogefd 26670 . . . . . . . . . . . . . 14 (𝜑 → (log‘(exp‘(𝐵 / 𝐸))) = (𝐵 / 𝐸))
104100, 103eqtrid 2789 . . . . . . . . . . . . 13 (𝜑 → (log‘𝐾) = (𝐵 / 𝐸))
105104oveq2d 7447 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = ((log‘𝑍) / (𝐵 / 𝐸)))
10639rpcnd 13079 . . . . . . . . . . . . 13 (𝜑 → (log‘𝑍) ∈ ℂ)
1073rpcnne0d 13086 . . . . . . . . . . . . 13 (𝜑 → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
10816rpcnne0d 13086 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
109 divdiv2 11979 . . . . . . . . . . . . 13 (((log‘𝑍) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
110106, 107, 108, 109syl3anc 1373 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
111105, 110eqtrd 2777 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = (((log‘𝑍) · 𝐸) / 𝐵))
112111oveq2d 7447 . . . . . . . . . 10 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11316rpcnd 13079 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
114106, 113mulcld 11281 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) · 𝐸) ∈ ℂ)
115 divass 11940 . . . . . . . . . . 11 (((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) · 𝐸) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11684, 114, 107, 115syl3anc 1373 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11715rpcnd 13079 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℂ)
118117, 113, 106, 113mul4d 11473 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
119113sqvald 14183 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
120119oveq2d 7447 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
121113sqcld 14184 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) ∈ ℂ)
122117, 106, 121mul32d 11471 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
123118, 120, 1223eqtr2d 2783 . . . . . . . . . . 11 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
124123oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
125112, 116, 1243eqtr2d 2783 . . . . . . . . 9 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
126 8t4e32 12850 . . . . . . . . . 10 (8 · 4) = 32
127126a1i 11 . . . . . . . . 9 (𝜑 → (8 · 4) = 32)
128125, 127oveq12d 7449 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)) = ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32))
12920rpcnd 13079 . . . . . . . . . . 11 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ)
130129, 106mulcld 11281 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ)
131 rpcnne0 13053 . . . . . . . . . . 11 (32 ∈ ℝ+ → (32 ∈ ℂ ∧ 32 ≠ 0))
13225, 131mp1i 13 . . . . . . . . . 10 (𝜑 → (32 ∈ ℂ ∧ 32 ≠ 0))
133 divdiv1 11978 . . . . . . . . . 10 ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (32 ∈ ℂ ∧ 32 ≠ 0)) → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
134130, 107, 132, 133syl3anc 1373 . . . . . . . . 9 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
13523nncni 12276 . . . . . . . . . . 11 32 ∈ ℂ
1363rpcnd 13079 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
137 mulcom 11241 . . . . . . . . . . 11 ((32 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (32 · 𝐵) = (𝐵 · 32))
138135, 136, 137sylancr 587 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) = (𝐵 · 32))
139138oveq2d 7447 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
14027rpcnne0d 13086 . . . . . . . . . 10 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
141 div23 11941 . . . . . . . . . 10 (((𝐿 · (𝐸↑2)) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
142129, 106, 140, 141syl3anc 1373 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
143134, 139, 1423eqtr2d 2783 . . . . . . . 8 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
14499, 128, 1433eqtrd 2781 . . . . . . 7 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
145144oveq1d 7446 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
14650rpcnd 13079 . . . . . . 7 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℂ)
14789rpred 13077 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ)
148 4nn 12349 . . . . . . . . 9 4 ∈ ℕ
149 nndivre 12307 . . . . . . . . 9 ((((log‘𝑍) / (log‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
150147, 148, 149sylancl 586 . . . . . . . 8 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
151150recnd 11289 . . . . . . 7 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℂ)
152146, 106, 151mul32d 11471 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)))
153106sqvald 14183 . . . . . . . 8 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
154153oveq2d 7447 . . . . . . 7 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
15528rpcnd 13079 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
156155, 106, 106mulassd 11284 . . . . . . 7 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
157154, 156eqtr4d 2780 . . . . . 6 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
158145, 152, 1573eqtr4d 2787 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))
15956simp3d 1145 . . . . . 6 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀))
160150, 63, 51lemul2d 13121 . . . . . 6 (𝜑 → ((((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀) ↔ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
161159, 160mpbid 232 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
162158, 161eqbrtrrd 5167 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
16342rpred 13077 . . . . 5 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
16451rpred 13077 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
165164, 63remulcld 11291 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ∈ ℝ)
166163, 165, 13lemul2d 13121 . . . 4 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ↔ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))))
167162, 166mpbid 232 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
16813rpcnd 13079 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℂ)
16951rpcnd 13079 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℂ)
17063recnd 11289 . . . 4 (𝜑 → (𝑁𝑀) ∈ ℂ)
171168, 169, 170mulassd 11284 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) = ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
172167, 171breqtrrd 5171 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
173 fzfid 14014 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
17460nnzd 12640 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
17585, 174rpexpcld 14286 . . . . . . . . . . 11 (𝜑 → (𝐾𝑁) ∈ ℝ+)
17635, 175rpdivcld 13094 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝑁)) ∈ ℝ+)
177176rprege0d 13084 . . . . . . . . 9 (𝜑 → ((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))))
178 flge0nn0 13860 . . . . . . . . 9 (((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))) → (⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0)
179 nn0p1nn 12565 . . . . . . . . 9 ((⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
180177, 178, 1793syl 18 . . . . . . . 8 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
181 nnuz 12921 . . . . . . . 8 ℕ = (ℤ‘1)
182180, 181eleqtrdi 2851 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1))
183 fzss1 13603 . . . . . . 7 (((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
184182, 183syl 17 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
185184sselda 3983 . . . . 5 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
186185, 82syldan 591 . . . 4 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
187173, 186fsumrecl 15770 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
188 eluzfz2 13572 . . . . 5 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
18958, 188syl 17 . . . 4 (𝜑𝑁 ∈ (𝑀...𝑁))
190 oveq1 7438 . . . . . . . 8 (𝑚 = 𝑀 → (𝑚𝑀) = (𝑀𝑀))
191190oveq2d 7447 . . . . . . 7 (𝑚 = 𝑀 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)))
192 oveq2 7439 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝐾𝑚) = (𝐾𝑀))
193192oveq2d 7447 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑀)))
194193fveq2d 6910 . . . . . . . . . 10 (𝑚 = 𝑀 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑀))))
195194oveq1d 7446 . . . . . . . . 9 (𝑚 = 𝑀 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑀))) + 1))
196195oveq1d 7446 . . . . . . . 8 (𝑚 = 𝑀 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))))
197196sumeq1d 15736 . . . . . . 7 (𝑚 = 𝑀 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
198191, 197breq12d 5156 . . . . . 6 (𝑚 = 𝑀 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
199198imbi2d 340 . . . . 5 (𝑚 = 𝑀 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
200 oveq1 7438 . . . . . . . 8 (𝑚 = 𝑗 → (𝑚𝑀) = (𝑗𝑀))
201200oveq2d 7447 . . . . . . 7 (𝑚 = 𝑗 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)))
202 oveq2 7439 . . . . . . . . . . . 12 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
203202oveq2d 7447 . . . . . . . . . . 11 (𝑚 = 𝑗 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑗)))
204203fveq2d 6910 . . . . . . . . . 10 (𝑚 = 𝑗 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑗))))
205204oveq1d 7446 . . . . . . . . 9 (𝑚 = 𝑗 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
206205oveq1d 7446 . . . . . . . 8 (𝑚 = 𝑗 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
207206sumeq1d 15736 . . . . . . 7 (𝑚 = 𝑗 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
208201, 207breq12d 5156 . . . . . 6 (𝑚 = 𝑗 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
209208imbi2d 340 . . . . 5 (𝑚 = 𝑗 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
210 oveq1 7438 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (𝑚𝑀) = ((𝑗 + 1) − 𝑀))
211210oveq2d 7447 . . . . . . 7 (𝑚 = (𝑗 + 1) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
212 oveq2 7439 . . . . . . . . . . . 12 (𝑚 = (𝑗 + 1) → (𝐾𝑚) = (𝐾↑(𝑗 + 1)))
213212oveq2d 7447 . . . . . . . . . . 11 (𝑚 = (𝑗 + 1) → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾↑(𝑗 + 1))))
214213fveq2d 6910 . . . . . . . . . 10 (𝑚 = (𝑗 + 1) → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))))
215214oveq1d 7446 . . . . . . . . 9 (𝑚 = (𝑗 + 1) → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1))
216215oveq1d 7446 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
217216sumeq1d 15736 . . . . . . 7 (𝑚 = (𝑗 + 1) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
218211, 217breq12d 5156 . . . . . 6 (𝑚 = (𝑗 + 1) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
219218imbi2d 340 . . . . 5 (𝑚 = (𝑗 + 1) → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
220 oveq1 7438 . . . . . . . 8 (𝑚 = 𝑁 → (𝑚𝑀) = (𝑁𝑀))
221220oveq2d 7447 . . . . . . 7 (𝑚 = 𝑁 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
222 oveq2 7439 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝐾𝑚) = (𝐾𝑁))
223222oveq2d 7447 . . . . . . . . . . 11 (𝑚 = 𝑁 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑁)))
224223fveq2d 6910 . . . . . . . . . 10 (𝑚 = 𝑁 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑁))))
225224oveq1d 7446 . . . . . . . . 9 (𝑚 = 𝑁 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑁))) + 1))
226225oveq1d 7446 . . . . . . . 8 (𝑚 = 𝑁 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))))
227226sumeq1d 15736 . . . . . . 7 (𝑚 = 𝑁 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
228221, 227breq12d 5156 . . . . . 6 (𝑚 = 𝑁 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
229228imbi2d 340 . . . . 5 (𝑚 = 𝑁 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
23057nncnd 12282 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
231230subidd 11608 . . . . . . . . 9 (𝜑 → (𝑀𝑀) = 0)
232231oveq2d 7447 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0))
23352rpcnd 13079 . . . . . . . . 9 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
234233mul01d 11460 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0) = 0)
235232, 234eqtrd 2777 . . . . . . 7 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = 0)
236 fzfid 14014 . . . . . . . 8 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
23757nnzd 12640 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
23885, 237rpexpcld 14286 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾𝑀) ∈ ℝ+)
23935, 238rpdivcld 13094 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / (𝐾𝑀)) ∈ ℝ+)
240239rprege0d 13084 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))))
241 flge0nn0 13860 . . . . . . . . . . . . 13 (((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))) → (⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0)
242 nn0p1nn 12565 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
243240, 241, 2423syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
244243, 181eleqtrdi 2851 . . . . . . . . . . 11 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1))
245 fzss1 13603 . . . . . . . . . . 11 (((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
246244, 245syl 17 . . . . . . . . . 10 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
247246sselda 3983 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
248247, 82syldan 591 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
249 elfzle2 13568 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
250249adantl 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
25129simpld 494 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ+)
25235, 251rpdivcld 13094 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
253252rpred 13077 . . . . . . . . . . . . 13 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
254 elfzelz 13564 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℤ)
255 flge 13845 . . . . . . . . . . . . 13 (((𝑍 / 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
256253, 254, 255syl2an 596 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
257250, 256mpbird 257 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (𝑍 / 𝑌))
25871, 257jca 511 . . . . . . . . . 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 27644 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
261258, 260syldan 591 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
262247, 261syldan 591 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
263236, 248, 262fsumge0 15831 . . . . . . 7 (𝜑 → 0 ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
264235, 263eqbrtrd 5165 . . . . . 6 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
265264a1i 11 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
266 pntlem1.K . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
267 eqid 2737 . . . . . . . . . 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 27648 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
26952adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
270269rpred 13077 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
271 elfzoelz 13699 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ ℤ)
272271adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ)
273272zred 12722 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℝ)
27457adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℕ)
275274nnred 12281 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
276273, 275resubcld 11691 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℝ)
277270, 276remulcld 11291 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ∈ ℝ)
278 fzfid 14014 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∈ Fin)
279 ssun1 4178 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
28036adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ)
28185adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ+)
282272peano2zd 12725 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ ℤ)
283281, 282rpexpcld 14286 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑(𝑗 + 1)) ∈ ℝ+)
284280, 283rerpdivcld 13108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ)
285281, 272rpexpcld 14286 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ+)
286280, 285rerpdivcld 13108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ∈ ℝ)
28786adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ)
288 1re 11261 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
289 ltle 11349 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (1 < 𝐾 → 1 ≤ 𝐾))
290288, 86, 289sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 < 𝐾 → 1 ≤ 𝐾))
29187, 290mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐾)
292291adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ≤ 𝐾)
293 uzid 12893 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
294 peano2uz 12943 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
295272, 293, 2943syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ (ℤ𝑗))
296287, 292, 295leexp2ad 14293 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)))
29735adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ+)
298285, 283, 297lediv2d 13101 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)) ↔ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))))
299296, 298mpbid 232 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗)))
300 flword2 13853 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
301284, 286, 299, 300syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
302 eluzp1p1 12906 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
303301, 302syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
304286flcld 13838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ)
305252adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ+)
306305rpred 13077 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ)
307306flcld 13838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ ℤ)
308251adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ+)
309308rpred 13077 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ)
310285rpred 13077 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ)
31130simpld 494 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ+)
312311rpred 13077 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ)
313312adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)
31430simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 < 𝑋)
315314adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < 𝑋)
316 elfzofz 13715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁))
3171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemh 27643 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
318316, 317sylan2 593 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
319318simpld 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 < (𝐾𝑗))
320309, 313, 310, 315, 319lttrd 11422 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < (𝐾𝑗))
321309, 310, 320ltled 11409 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ≤ (𝐾𝑗))
322308, 285, 297lediv2d 13101 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑌 ≤ (𝐾𝑗) ↔ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)))
323321, 322mpbid 232 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌))
324 flwordi 13852 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / 𝑌) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
325286, 306, 323, 324syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
326 eluz2 12884 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))) ↔ ((⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ ∧ (⌊‘(𝑍 / 𝑌)) ∈ ℤ ∧ (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌))))
327304, 307, 325, 326syl3anbrc 1344 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))))
328 fzsplit2 13589 . . . . . . . . . . . . . . . 16 ((((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)) ∧ (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗))))) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
329303, 327, 328syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
330279, 329sseqtrrid 4027 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
331297, 283rpdivcld 13094 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ+)
332331rprege0d 13084 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))))
333 flge0nn0 13860 . . . . . . . . . . . . . . . . 17 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0)
334 nn0p1nn 12565 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
335332, 333, 3343syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
336335, 181eleqtrdi 2851 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1))
337 fzss1 13603 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
338336, 337syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
339330, 338sstrd 3994 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
340339sselda 3983 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
34182adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
342340, 341syldan 591 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
343278, 342fsumrecl 15770 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
344 fzfid 14014 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
345 ssun2 4179 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
346345, 329sseqtrrid 4027 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
347346, 338sstrd 3994 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
348347sselda 3983 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
349348, 341syldan 591 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
350344, 349fsumrecl 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‘𝑛)))))
352270, 277, 343, 350, 351syl22anc 839 . . . . . . . . 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 695 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
354233adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
355 1cnd 11256 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ)
356272zcnd 12723 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ)
357230adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ)
358356, 357subcld 11620 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℂ)
359354, 355, 358adddid 11285 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
360355, 358addcomd 11463 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗𝑀) + 1))
361356, 355, 357addsubd 11641 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 + 1) − 𝑀) = ((𝑗𝑀) + 1))
362360, 361eqtr4d 2780 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗 + 1) − 𝑀))
363362oveq2d 7447 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
364354mulridd 11278 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) = ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))))
365364oveq1d 7446 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
366359, 363, 3653eqtr3d 2785 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
367 reflcl 13836 . . . . . . . . . . . . 13 ((𝑍 / (𝐾𝑗)) ∈ ℝ → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
368286, 367syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
369368ltp1d 12198 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
370 fzdisj 13591 . . . . . . . . . . 11 ((⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
371369, 370syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
372 fzfid 14014 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
373338sselda 3983 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
374373, 341syldan 591 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
375374recnd 11289 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℂ)
376371, 329, 372, 375fsumsplit 15777 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
377366, 376breq12d 5156 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
378353, 377sylibrd 259 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
379378expcom 413 . . . . . 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 13824 . . . 4 (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
382189, 381mpcom 38 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38365, 82, 261, 184fsumless 15832 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38464, 187, 83, 382, 383letrd 11418 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38544, 64, 83, 172, 384letrd 11418 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  cun 3949  cin 3950  wss 3951  c0 4333   class class class wbr 5143  cmpt 5225  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  3c3 12322  4c4 12323  8c8 12327  0cn0 12526  cz 12613  cdc 12733  cuz 12878  +crp 13034  (,)cioo 13387  [,)cico 13389  [,]cicc 13390  ...cfz 13547  ..^cfzo 13694  cfl 13830  cexp 14102  csqrt 15272  abscabs 15273  Σcsu 15722  expce 16097  eceu 16098  logclog 26596  ψcchp 27136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-e 16104  df-sin 16105  df-cos 16106  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-log 26598  df-vma 27141  df-chp 27142
This theorem is referenced by:  pntlemo  27651
  Copyright terms: Public domain W3C validator