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

Theorem pntlemf 25491
Description: Lemma for pnt 25500. Add up the pieces in pntlemi 25490 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 25481 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1139 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1139 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 25480 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1137 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1137 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
17 2z 11599 . . . . . . . 8 2 ∈ ℤ
18 rpexpcl 13071 . . . . . . . 8 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
1916, 17, 18sylancl 697 . . . . . . 7 (𝜑 → (𝐸↑2) ∈ ℝ+)
2015, 19rpmulcld 12079 . . . . . 6 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
21 3nn0 11500 . . . . . . . . 9 3 ∈ ℕ0
22 2nn 11375 . . . . . . . . 9 2 ∈ ℕ
2321, 22decnncl 11708 . . . . . . . 8 32 ∈ ℕ
24 nnrp 12033 . . . . . . . 8 (32 ∈ ℕ → 32 ∈ ℝ+)
2523, 24ax-mp 5 . . . . . . 7 32 ∈ ℝ+
26 rpmulcl 12046 . . . . . . 7 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
2725, 3, 26sylancr 698 . . . . . 6 (𝜑 → (32 · 𝐵) ∈ ℝ+)
2820, 27rpdivcld 12080 . . . . 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 25483 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
3534simp1d 1137 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
3635rpred 12063 . . . . . . 7 (𝜑𝑍 ∈ ℝ)
3734simp2d 1138 . . . . . . . 8 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3837simp1d 1137 . . . . . . 7 (𝜑 → 1 < 𝑍)
3936, 38rplogcld 24572 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℝ+)
40 rpexpcl 13071 . . . . . 6 (((log‘𝑍) ∈ ℝ+ ∧ 2 ∈ ℤ) → ((log‘𝑍)↑2) ∈ ℝ+)
4139, 17, 40sylancl 697 . . . . 5 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ+)
4228, 41rpmulcld 12079 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ+)
4313, 42rpmulcld 12079 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ+)
4443rpred 12063 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
4515, 16rpmulcld 12079 . . . . . . 7 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
46 8re 11295 . . . . . . . 8 8 ∈ ℝ
47 8pos 11311 . . . . . . . 8 0 < 8
4846, 47elrpii 12026 . . . . . . 7 8 ∈ ℝ+
49 rpdivcl 12047 . . . . . . 7 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5045, 48, 49sylancl 697 . . . . . 6 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
5150, 39rpmulcld 12079 . . . . 5 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
5213, 51rpmulcld 12079 . . . 4 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
5352rpred 12063 . . 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 25484 . . . . . . 7 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
5756simp1d 1137 . . . . . 6 (𝜑𝑀 ∈ ℕ)
5856simp2d 1138 . . . . . 6 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluznn 11949 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑁 ∈ ℕ)
6057, 58, 59syl2anc 696 . . . . 5 (𝜑𝑁 ∈ ℕ)
6160nnred 11225 . . . 4 (𝜑𝑁 ∈ ℝ)
6257nnred 11225 . . . 4 (𝜑𝑀 ∈ ℝ)
6361, 62resubcld 10648 . . 3 (𝜑 → (𝑁𝑀) ∈ ℝ)
6453, 63remulcld 10260 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ∈ ℝ)
65 fzfid 12964 . . 3 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
667rpred 12063 . . . . . 6 (𝜑𝑈 ∈ ℝ)
67 elfznn 12561 . . . . . 6 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
68 nndivre 11246 . . . . . 6 ((𝑈 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑈 / 𝑛) ∈ ℝ)
6966, 67, 68syl2an 495 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
7035adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
7167adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
7271nnrpd 12061 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
7370, 72rpdivcld 12080 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 25449 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelrni 6519 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 70rerpdivcld 12094 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 10258 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 14372 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8069, 79resubcld 10648 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 24566 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 10260 . . 3 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8365, 82fsumrecl 14662 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8445rpcnd 12065 . . . . . . . . 9 (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
8511simp2d 1138 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ+)
8685rpred 12063 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
8712simp2d 1138 . . . . . . . . . . . 12 (𝜑 → 1 < 𝐾)
8886, 87rplogcld 24572 . . . . . . . . . . 11 (𝜑 → (log‘𝐾) ∈ ℝ+)
8939, 88rpdivcld 12080 . . . . . . . . . 10 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ+)
9089rpcnd 12065 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℂ)
91 rpcnne0 12041 . . . . . . . . . 10 (8 ∈ ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0))
9248, 91mp1i 13 . . . . . . . . 9 (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
93 4re 11287 . . . . . . . . . . 11 4 ∈ ℝ
94 4pos 11306 . . . . . . . . . . 11 0 < 4
9593, 94elrpii 12026 . . . . . . . . . 10 4 ∈ ℝ+
96 rpcnne0 12041 . . . . . . . . . 10 (4 ∈ ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0))
9795, 96mp1i 13 . . . . . . . . 9 (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
98 divmuldiv 10915 . . . . . . . . 9 ((((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) / (log‘𝐾)) ∈ ℂ) ∧ ((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0))) → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)))
9984, 90, 92, 97, 98syl22anc 1478 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)))
10010fveq2i 6353 . . . . . . . . . . . . . 14 (log‘𝐾) = (log‘(exp‘(𝐵 / 𝐸)))
1013, 16rpdivcld 12080 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐸) ∈ ℝ+)
102101rpred 12063 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / 𝐸) ∈ ℝ)
103102relogefd 24571 . . . . . . . . . . . . . 14 (𝜑 → (log‘(exp‘(𝐵 / 𝐸))) = (𝐵 / 𝐸))
104100, 103syl5eq 2804 . . . . . . . . . . . . 13 (𝜑 → (log‘𝐾) = (𝐵 / 𝐸))
105104oveq2d 6827 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = ((log‘𝑍) / (𝐵 / 𝐸)))
10639rpcnd 12065 . . . . . . . . . . . . 13 (𝜑 → (log‘𝑍) ∈ ℂ)
1073rpcnne0d 12072 . . . . . . . . . . . . 13 (𝜑 → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
10816rpcnne0d 12072 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
109 divdiv2 10927 . . . . . . . . . . . . 13 (((log‘𝑍) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
110106, 107, 108, 109syl3anc 1477 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍) / (𝐵 / 𝐸)) = (((log‘𝑍) · 𝐸) / 𝐵))
111105, 110eqtrd 2792 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) / (log‘𝐾)) = (((log‘𝑍) · 𝐸) / 𝐵))
112111oveq2d 6827 . . . . . . . . . 10 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11316rpcnd 12065 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
114106, 113mulcld 10250 . . . . . . . . . . 11 (𝜑 → ((log‘𝑍) · 𝐸) ∈ ℂ)
115 divass 10893 . . . . . . . . . . 11 (((𝐿 · 𝐸) ∈ ℂ ∧ ((log‘𝑍) · 𝐸) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11684, 114, 107, 115syl3anc 1477 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = ((𝐿 · 𝐸) · (((log‘𝑍) · 𝐸) / 𝐵)))
11715rpcnd 12065 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℂ)
118117, 113, 106, 113mul4d 10438 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
119113sqvald 13197 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
120119oveq2d 6827 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (log‘𝑍)) · (𝐸 · 𝐸)))
121113sqcld 13198 . . . . . . . . . . . . 13 (𝜑 → (𝐸↑2) ∈ ℂ)
122117, 106, 121mul32d 10436 . . . . . . . . . . . 12 (𝜑 → ((𝐿 · (log‘𝑍)) · (𝐸↑2)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
123118, 120, 1223eqtr2d 2798 . . . . . . . . . . 11 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) = ((𝐿 · (𝐸↑2)) · (log‘𝑍)))
124123oveq1d 6826 . . . . . . . . . 10 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) · 𝐸)) / 𝐵) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
125112, 116, 1243eqtr2d 2798 . . . . . . . . 9 (𝜑 → ((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵))
126 8t4e32 11846 . . . . . . . . . 10 (8 · 4) = 32
127126a1i 11 . . . . . . . . 9 (𝜑 → (8 · 4) = 32)
128125, 127oveq12d 6829 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) · ((log‘𝑍) / (log‘𝐾))) / (8 · 4)) = ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32))
12920rpcnd 12065 . . . . . . . . . . 11 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ)
130129, 106mulcld 10250 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ)
131 rpcnne0 12041 . . . . . . . . . . 11 (32 ∈ ℝ+ → (32 ∈ ℂ ∧ 32 ≠ 0))
13225, 131mp1i 13 . . . . . . . . . 10 (𝜑 → (32 ∈ ℂ ∧ 32 ≠ 0))
133 divdiv1 10926 . . . . . . . . . 10 ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (32 ∈ ℂ ∧ 32 ≠ 0)) → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
134130, 107, 132, 133syl3anc 1477 . . . . . . . . 9 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
13523nncni 11220 . . . . . . . . . . 11 32 ∈ ℂ
1363rpcnd 12065 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
137 mulcom 10212 . . . . . . . . . . 11 ((32 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (32 · 𝐵) = (𝐵 · 32))
138135, 136, 137sylancr 698 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) = (𝐵 · 32))
139138oveq2d 6827 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (𝐵 · 32)))
14027rpcnne0d 12072 . . . . . . . . . 10 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
141 div23 10894 . . . . . . . . . 10 (((𝐿 · (𝐸↑2)) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
142129, 106, 140, 141syl3anc 1477 . . . . . . . . 9 (𝜑 → (((𝐿 · (𝐸↑2)) · (log‘𝑍)) / (32 · 𝐵)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
143134, 139, 1423eqtr2d 2798 . . . . . . . 8 (𝜑 → ((((𝐿 · (𝐸↑2)) · (log‘𝑍)) / 𝐵) / 32) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
14499, 128, 1433eqtrd 2796 . . . . . . 7 (𝜑 → (((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)))
145144oveq1d 6826 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
14650rpcnd 12065 . . . . . . 7 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℂ)
14789rpred 12063 . . . . . . . . 9 (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ)
148 4nn 11377 . . . . . . . . 9 4 ∈ ℕ
149 nndivre 11246 . . . . . . . . 9 ((((log‘𝑍) / (log‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
150147, 148, 149sylancl 697 . . . . . . . 8 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ)
151150recnd 10258 . . . . . . 7 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℂ)
152146, 106, 151mul32d 10436 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = ((((𝐿 · 𝐸) / 8) · (((log‘𝑍) / (log‘𝐾)) / 4)) · (log‘𝑍)))
153106sqvald 13197 . . . . . . . 8 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
154153oveq2d 6827 . . . . . . 7 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
15528rpcnd 12065 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
156155, 106, 106mulassd 10253 . . . . . . 7 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍) · (log‘𝑍))))
157154, 156eqtr4d 2795 . . . . . 6 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) = ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · (log‘𝑍)) · (log‘𝑍)))
158145, 152, 1573eqtr4d 2802 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) = (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))
15956simp3d 1139 . . . . . 6 (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀))
160150, 63, 51lemul2d 12107 . . . . . 6 (𝜑 → ((((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀) ↔ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
161159, 160mpbid 222 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (((log‘𝑍) / (log‘𝐾)) / 4)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
162158, 161eqbrtrrd 4826 . . . 4 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))
16342rpred 12063 . . . . 5 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
16451rpred 12063 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
165164, 63remulcld 10260 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ∈ ℝ)
166163, 165, 13lemul2d 12107 . . . 4 (𝜑 → ((((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ≤ ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)) ↔ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀)))))
167162, 166mpbid 222 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
16813rpcnd 12065 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℂ)
16951rpcnd 12065 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℂ)
17063recnd 10258 . . . 4 (𝜑 → (𝑁𝑀) ∈ ℂ)
171168, 169, 170mulassd 10253 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) = ((𝑈𝐸) · ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) · (𝑁𝑀))))
172167, 171breqtrrd 4830 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
173 fzfid 12964 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
17460nnzd 11671 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
17585, 174rpexpcld 13224 . . . . . . . . . . 11 (𝜑 → (𝐾𝑁) ∈ ℝ+)
17635, 175rpdivcld 12080 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝑁)) ∈ ℝ+)
177176rprege0d 12070 . . . . . . . . 9 (𝜑 → ((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))))
178 flge0nn0 12813 . . . . . . . . 9 (((𝑍 / (𝐾𝑁)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑁))) → (⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0)
179 nn0p1nn 11522 . . . . . . . . 9 ((⌊‘(𝑍 / (𝐾𝑁))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
180177, 178, 1793syl 18 . . . . . . . 8 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ ℕ)
181 nnuz 11914 . . . . . . . 8 ℕ = (ℤ‘1)
182180, 181syl6eleq 2847 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1))
183 fzss1 12571 . . . . . . 7 (((⌊‘(𝑍 / (𝐾𝑁))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
184182, 183syl 17 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
185184sselda 3742 . . . . 5 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
186185, 82syldan 488 . . . 4 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
187173, 186fsumrecl 14662 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
188 eluzfz2 12540 . . . . 5 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
18958, 188syl 17 . . . 4 (𝜑𝑁 ∈ (𝑀...𝑁))
190 oveq1 6818 . . . . . . . 8 (𝑚 = 𝑀 → (𝑚𝑀) = (𝑀𝑀))
191190oveq2d 6827 . . . . . . 7 (𝑚 = 𝑀 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)))
192 oveq2 6819 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝐾𝑚) = (𝐾𝑀))
193192oveq2d 6827 . . . . . . . . . . 11 (𝑚 = 𝑀 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑀)))
194193fveq2d 6354 . . . . . . . . . 10 (𝑚 = 𝑀 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑀))))
195194oveq1d 6826 . . . . . . . . 9 (𝑚 = 𝑀 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑀))) + 1))
196195oveq1d 6826 . . . . . . . 8 (𝑚 = 𝑀 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))))
197196sumeq1d 14628 . . . . . . 7 (𝑚 = 𝑀 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
198191, 197breq12d 4815 . . . . . 6 (𝑚 = 𝑀 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
199198imbi2d 329 . . . . 5 (𝑚 = 𝑀 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
200 oveq1 6818 . . . . . . . 8 (𝑚 = 𝑗 → (𝑚𝑀) = (𝑗𝑀))
201200oveq2d 6827 . . . . . . 7 (𝑚 = 𝑗 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)))
202 oveq2 6819 . . . . . . . . . . . 12 (𝑚 = 𝑗 → (𝐾𝑚) = (𝐾𝑗))
203202oveq2d 6827 . . . . . . . . . . 11 (𝑚 = 𝑗 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑗)))
204203fveq2d 6354 . . . . . . . . . 10 (𝑚 = 𝑗 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑗))))
205204oveq1d 6826 . . . . . . . . 9 (𝑚 = 𝑗 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
206205oveq1d 6826 . . . . . . . 8 (𝑚 = 𝑗 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
207206sumeq1d 14628 . . . . . . 7 (𝑚 = 𝑗 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
208201, 207breq12d 4815 . . . . . 6 (𝑚 = 𝑗 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
209208imbi2d 329 . . . . 5 (𝑚 = 𝑗 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
210 oveq1 6818 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (𝑚𝑀) = ((𝑗 + 1) − 𝑀))
211210oveq2d 6827 . . . . . . 7 (𝑚 = (𝑗 + 1) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
212 oveq2 6819 . . . . . . . . . . . 12 (𝑚 = (𝑗 + 1) → (𝐾𝑚) = (𝐾↑(𝑗 + 1)))
213212oveq2d 6827 . . . . . . . . . . 11 (𝑚 = (𝑗 + 1) → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾↑(𝑗 + 1))))
214213fveq2d 6354 . . . . . . . . . 10 (𝑚 = (𝑗 + 1) → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))))
215214oveq1d 6826 . . . . . . . . 9 (𝑚 = (𝑗 + 1) → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1))
216215oveq1d 6826 . . . . . . . 8 (𝑚 = (𝑗 + 1) → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
217216sumeq1d 14628 . . . . . . 7 (𝑚 = (𝑗 + 1) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
218211, 217breq12d 4815 . . . . . 6 (𝑚 = (𝑗 + 1) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
219218imbi2d 329 . . . . 5 (𝑚 = (𝑗 + 1) → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
220 oveq1 6818 . . . . . . . 8 (𝑚 = 𝑁 → (𝑚𝑀) = (𝑁𝑀))
221220oveq2d 6827 . . . . . . 7 (𝑚 = 𝑁 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)))
222 oveq2 6819 . . . . . . . . . . . 12 (𝑚 = 𝑁 → (𝐾𝑚) = (𝐾𝑁))
223222oveq2d 6827 . . . . . . . . . . 11 (𝑚 = 𝑁 → (𝑍 / (𝐾𝑚)) = (𝑍 / (𝐾𝑁)))
224223fveq2d 6354 . . . . . . . . . 10 (𝑚 = 𝑁 → (⌊‘(𝑍 / (𝐾𝑚))) = (⌊‘(𝑍 / (𝐾𝑁))))
225224oveq1d 6826 . . . . . . . . 9 (𝑚 = 𝑁 → ((⌊‘(𝑍 / (𝐾𝑚))) + 1) = ((⌊‘(𝑍 / (𝐾𝑁))) + 1))
226225oveq1d 6826 . . . . . . . 8 (𝑚 = 𝑁 → (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌))) = (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌))))
227226sumeq1d 14628 . . . . . . 7 (𝑚 = 𝑁 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
228221, 227breq12d 4815 . . . . . 6 (𝑚 = 𝑁 → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
229228imbi2d 329 . . . . 5 (𝑚 = 𝑁 → ((𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑚𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑚))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ↔ (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
23057nncnd 11226 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
231230subidd 10570 . . . . . . . . 9 (𝜑 → (𝑀𝑀) = 0)
232231oveq2d 6827 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0))
23352rpcnd 12065 . . . . . . . . 9 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
234233mul01d 10425 . . . . . . . 8 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 0) = 0)
235232, 234eqtrd 2792 . . . . . . 7 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) = 0)
236 fzfid 12964 . . . . . . . 8 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
23757nnzd 11671 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
23885, 237rpexpcld 13224 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾𝑀) ∈ ℝ+)
23935, 238rpdivcld 12080 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / (𝐾𝑀)) ∈ ℝ+)
240239rprege0d 12070 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))))
241 flge0nn0 12813 . . . . . . . . . . . . 13 (((𝑍 / (𝐾𝑀)) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾𝑀))) → (⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0)
242 nn0p1nn 11522 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / (𝐾𝑀))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
243240, 241, 2423syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ ℕ)
244243, 181syl6eleq 2847 . . . . . . . . . . 11 (𝜑 → ((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1))
245 fzss1 12571 . . . . . . . . . . 11 (((⌊‘(𝑍 / (𝐾𝑀))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
246244, 245syl 17 . . . . . . . . . 10 (𝜑 → (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
247246sselda 3742 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
248247, 82syldan 488 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
249 elfzle2 12536 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
250249adantl 473 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑌)))
25129simpld 477 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ+)
25235, 251rpdivcld 12080 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
253252rpred 12063 . . . . . . . . . . . . 13 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
254 elfzelz 12533 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℤ)
255 flge 12798 . . . . . . . . . . . . 13 (((𝑍 / 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
256253, 254, 255syl2an 495 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ≤ (𝑍 / 𝑌) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑌))))
257250, 256mpbird 247 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ≤ (𝑍 / 𝑌))
25871, 257jca 555 . . . . . . . . . 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 25486 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
261258, 260syldan 488 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
262247, 261syldan 488 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
263236, 248, 262fsumge0 14724 . . . . . . 7 (𝜑 → 0 ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
264235, 263eqbrtrd 4824 . . . . . 6 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
265264a1i 11 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑀𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑀))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
266 pntlem1.K . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
267 eqid 2758 . . . . . . . . . 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 25490 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
26952adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
270269rpred 12063 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
271 elfzoelz 12662 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ ℤ)
272271adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ)
273272zred 11672 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℝ)
27457adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℕ)
275274nnred 11225 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
276273, 275resubcld 10648 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℝ)
277270, 276remulcld 10260 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ∈ ℝ)
278 fzfid 12964 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∈ Fin)
279 ssun1 3917 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
28036adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ)
28185adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ+)
282272peano2zd 11675 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ ℤ)
283281, 282rpexpcld 13224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾↑(𝑗 + 1)) ∈ ℝ+)
284280, 283rerpdivcld 12094 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ)
285281, 272rpexpcld 13224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ+)
286280, 285rerpdivcld 12094 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ∈ ℝ)
28786adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝐾 ∈ ℝ)
288 1re 10229 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
289 ltle 10316 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (1 < 𝐾 → 1 ≤ 𝐾))
290288, 86, 289sylancr 698 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 < 𝐾 → 1 ≤ 𝐾))
29187, 290mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐾)
292291adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ≤ 𝐾)
293 uzid 11892 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
294 peano2uz 11932 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
295272, 293, 2943syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗 + 1) ∈ (ℤ𝑗))
296287, 292, 295leexp2ad 13233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)))
29735adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑍 ∈ ℝ+)
298285, 283, 297lediv2d 12087 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝐾𝑗) ≤ (𝐾↑(𝑗 + 1)) ↔ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))))
299296, 298mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗)))
300 flword2 12806 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / (𝐾↑(𝑗 + 1))) ≤ (𝑍 / (𝐾𝑗))) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
301284, 286, 299, 300syl3anc 1477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))))
302 eluzp1p1 11903 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾𝑗))) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾↑(𝑗 + 1))))) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
303301, 302syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)))
304286flcld 12791 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ)
305252adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ+)
306305rpred 12063 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / 𝑌) ∈ ℝ)
307306flcld 12791 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ ℤ)
308251adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ+)
309308rpred 12063 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ)
310285rpred 12063 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝐾𝑗) ∈ ℝ)
31130simpld 477 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ+)
312311rpred 12063 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ)
313312adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)
31430simprd 482 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 < 𝑋)
315314adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < 𝑋)
316 elfzofz 12677 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (𝑀..^𝑁) → 𝑗 ∈ (𝑀...𝑁))
3171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemh 25485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
318316, 317sylan2 492 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑋 < (𝐾𝑗) ∧ (𝐾𝑗) ≤ (√‘𝑍)))
319318simpld 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑋 < (𝐾𝑗))
320309, 313, 310, 315, 319lttrd 10388 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 < (𝐾𝑗))
321309, 310, 320ltled 10375 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑌 ≤ (𝐾𝑗))
322308, 285, 297lediv2d 12087 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑌 ≤ (𝐾𝑗) ↔ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)))
323321, 322mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌))
324 flwordi 12805 . . . . . . . . . . . . . . . . . 18 (((𝑍 / (𝐾𝑗)) ∈ ℝ ∧ (𝑍 / 𝑌) ∈ ℝ ∧ (𝑍 / (𝐾𝑗)) ≤ (𝑍 / 𝑌)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
325286, 306, 323, 324syl3anc 1477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌)))
326 eluz2 11883 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))) ↔ ((⌊‘(𝑍 / (𝐾𝑗))) ∈ ℤ ∧ (⌊‘(𝑍 / 𝑌)) ∈ ℤ ∧ (⌊‘(𝑍 / (𝐾𝑗))) ≤ (⌊‘(𝑍 / 𝑌))))
327304, 307, 325, 326syl3anbrc 1429 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗)))))
328 fzsplit2 12557 . . . . . . . . . . . . . . . 16 ((((⌊‘(𝑍 / (𝐾𝑗))) + 1) ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)) ∧ (⌊‘(𝑍 / 𝑌)) ∈ (ℤ‘(⌊‘(𝑍 / (𝐾𝑗))))) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
329303, 327, 328syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) = ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))))
330279, 329syl5sseqr 3793 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
331297, 283rpdivcld 12080 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ+)
332331rprege0d 12070 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))))
333 flge0nn0 12813 . . . . . . . . . . . . . . . . 17 (((𝑍 / (𝐾↑(𝑗 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝑗 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0)
334 nn0p1nn 11522 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
335332, 333, 3343syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ ℕ)
336335, 181syl6eleq 2847 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1))
337 fzss1 12571 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1) ∈ (ℤ‘1) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
338336, 337syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
339330, 338sstrd 3752 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
340339sselda 3742 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
34182adantlr 753 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
342340, 341syldan 488 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
343278, 342fsumrecl 14662 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
344 fzfid 12964 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
345 ssun2 3918 . . . . . . . . . . . . . . 15 (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∪ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))))
346345, 329syl5sseqr 3793 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))))
347346, 338sstrd 3752 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌))) ⊆ (1...(⌊‘(𝑍 / 𝑌))))
348347sselda 3742 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
349348, 341syldan 488 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
350344, 349fsumrecl 14662 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
351 le2add 10700 . . . . . . . . . 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 1478 . . . . . . . . 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 713 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
354233adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℂ)
355 1cnd 10246 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ)
356272zcnd 11673 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ)
357230adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ)
358356, 357subcld 10582 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑗𝑀) ∈ ℂ)
359354, 355, 358adddid 10254 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
360355, 358addcomd 10428 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗𝑀) + 1))
361356, 355, 357addsubd 10603 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 + 1) − 𝑀) = ((𝑗𝑀) + 1))
362360, 361eqtr4d 2795 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (1 + (𝑗𝑀)) = ((𝑗 + 1) − 𝑀))
363362oveq2d 6827 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (1 + (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)))
364354mulid1d 10247 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) = ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))))
365364oveq1d 6826 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · 1) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
366359, 363, 3653eqtr3d 2800 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) = (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))))
367 reflcl 12789 . . . . . . . . . . . . 13 ((𝑍 / (𝐾𝑗)) ∈ ℝ → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
368286, 367syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) ∈ ℝ)
369368ltp1d 11144 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1))
370 fzdisj 12559 . . . . . . . . . . 11 ((⌊‘(𝑍 / (𝐾𝑗))) < ((⌊‘(𝑍 / (𝐾𝑗))) + 1) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
371369, 370syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗)))) ∩ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))) = ∅)
372 fzfid 12964 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
373338sselda 3742 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))))
374373, 341syldan 488 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
375374recnd 10258 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℂ)
376371, 329, 372, 375fsumsplit 14668 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
377366, 376breq12d 4815 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) + (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀))) ≤ (Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝑗))))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) + Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
378353, 377sylibrd 249 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → ((((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑗𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑗))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · ((𝑗 + 1) − 𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝑗 + 1)))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
379378expcom 450 . . . . . 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 12778 . . . 4 (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
382189, 381mpcom 38 . . 3 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38365, 82, 261, 184fsumless 14725 . . 3 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝑍 / (𝐾𝑁))) + 1)...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38464, 187, 83, 382, 383letrd 10384 . 2 (𝜑 → (((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) · (𝑁𝑀)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
38544, 64, 83, 172, 384letrd 10384 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1630  wcel 2137  wne 2930  wral 3048  wrex 3049  cun 3711  cin 3712  wss 3713  c0 4056   class class class wbr 4802  cmpt 4879  cfv 6047  (class class class)co 6811  cc 10124  cr 10125  0cc0 10126  1c1 10127   + caddc 10129   · cmul 10131  +∞cpnf 10261   < clt 10264  cle 10265  cmin 10456   / cdiv 10874  cn 11210  2c2 11260  3c3 11261  4c4 11262  8c8 11266  0cn0 11482  cz 11567  cdc 11683  cuz 11877  +crp 12023  (,)cioo 12366  [,)cico 12368  [,]cicc 12369  ...cfz 12517  ..^cfzo 12657  cfl 12783  cexp 13052  csqrt 14170  abscabs 14171  Σcsu 14613  expce 14989  eceu 14990  logclog 24498  ψcchp 25016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204  ax-addf 10205  ax-mulf 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-of 7060  df-om 7229  df-1st 7331  df-2nd 7332  df-supp 7462  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-ixp 8073  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fsupp 8439  df-fi 8480  df-sup 8511  df-inf 8512  df-oi 8578  df-card 8953  df-cda 9180  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276  df-n0 11483  df-z 11568  df-dec 11684  df-uz 11878  df-q 11980  df-rp 12024  df-xneg 12137  df-xadd 12138  df-xmul 12139  df-ioo 12370  df-ioc 12371  df-ico 12372  df-icc 12373  df-fz 12518  df-fzo 12658  df-fl 12785  df-mod 12861  df-seq 12994  df-exp 13053  df-fac 13253  df-bc 13282  df-hash 13310  df-shft 14004  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-limsup 14399  df-clim 14416  df-rlim 14417  df-sum 14614  df-ef 14995  df-e 14996  df-sin 14997  df-cos 14998  df-pi 15000  df-dvds 15181  df-gcd 15417  df-prm 15586  df-pc 15742  df-struct 16059  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16154  df-mulr 16155  df-starv 16156  df-sca 16157  df-vsca 16158  df-ip 16159  df-tset 16160  df-ple 16161  df-ds 16164  df-unif 16165  df-hom 16166  df-cco 16167  df-rest 16283  df-topn 16284  df-0g 16302  df-gsum 16303  df-topgen 16304  df-pt 16305  df-prds 16308  df-xrs 16362  df-qtop 16367  df-imas 16368  df-xps 16370  df-mre 16446  df-mrc 16447  df-acs 16449  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-submnd 17535  df-mulg 17740  df-cntz 17948  df-cmn 18393  df-psmet 19938  df-xmet 19939  df-met 19940  df-bl 19941  df-mopn 19942  df-fbas 19943  df-fg 19944  df-cnfld 19947  df-top 20899  df-topon 20916  df-topsp 20937  df-bases 20950  df-cld 21023  df-ntr 21024  df-cls 21025  df-nei 21102  df-lp 21140  df-perf 21141  df-cn 21231  df-cnp 21232  df-haus 21319  df-tx 21565  df-hmeo 21758  df-fil 21849  df-fm 21941  df-flim 21942  df-flf 21943  df-xms 22324  df-ms 22325  df-tms 22326  df-cncf 22880  df-limc 23827  df-dv 23828  df-log 24500  df-vma 25021  df-chp 25022
This theorem is referenced by:  pntlemo  25493
  Copyright terms: Public domain W3C validator