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

Theorem pntlemj 25514
Description: Lemma for pnt 25525. The induction step. Using pntibnd 25504, we find an interval in 𝐾𝐽...𝐾↑(𝐽 + 1) which is sufficiently large and has a much smaller value, 𝑅(𝑧) / 𝑧𝐸 (instead of our original bound 𝑅(𝑧) / 𝑧𝑈). (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‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
pntlem1.o 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))
pntlem1.v (𝜑𝑉 ∈ ℝ+)
pntlem1.V (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
pntlem1.j (𝜑𝐽 ∈ (𝑀..^𝑁))
pntlem1.i 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
Assertion
Ref Expression
pntlemj (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Distinct variable groups:   𝑧,𝐶   𝑛,𝐼   𝑦,𝑛,𝑧,𝐽   𝑢,𝑛,𝐿,𝑦,𝑧   𝑛,𝐾,𝑦,𝑧   𝑛,𝑀,𝑧   𝑛,𝑂,𝑧   𝜑,𝑛   𝑛,𝑁,𝑧   𝑅,𝑛,𝑢,𝑦,𝑧   𝑛,𝑉,𝑢   𝑈,𝑛,𝑧   𝑛,𝑊,𝑧   𝑛,𝑋,𝑦,𝑧   𝑛,𝑌,𝑧   𝑛,𝑎,𝑢,𝑦,𝑧,𝐸   𝑛,𝑍,𝑢,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑢,𝑎)   𝐴(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐵(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐶(𝑦,𝑢,𝑛,𝑎)   𝐷(𝑦,𝑧,𝑢,𝑛,𝑎)   𝑅(𝑎)   𝑈(𝑦,𝑢,𝑎)   𝐹(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐼(𝑦,𝑧,𝑢,𝑎)   𝐽(𝑢,𝑎)   𝐾(𝑢,𝑎)   𝐿(𝑎)   𝑀(𝑦,𝑢,𝑎)   𝑁(𝑦,𝑢,𝑎)   𝑂(𝑦,𝑢,𝑎)   𝑉(𝑦,𝑧,𝑎)   𝑊(𝑦,𝑢,𝑎)   𝑋(𝑢,𝑎)   𝑌(𝑦,𝑢,𝑎)   𝑍(𝑦,𝑎)

Proof of Theorem pntlemj
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 25506 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1138 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1138 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 25505 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1136 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1136 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1715, 16rpmulcld 12092 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
18 8nn 11394 . . . . . . 7 8 ∈ ℕ
19 nnrp 12046 . . . . . . 7 (8 ∈ ℕ → 8 ∈ ℝ+)
2018, 19ax-mp 5 . . . . . 6 8 ∈ ℝ+
21 rpdivcl 12060 . . . . . 6 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
2217, 20, 21sylancl 568 . . . . 5 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
23 pntlem1.y . . . . . . . . 9 (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
24 pntlem1.x . . . . . . . . 9 (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))
25 pntlem1.c . . . . . . . . 9 (𝜑𝐶 ∈ ℝ+)
26 pntlem1.w . . . . . . . . 9 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))
27 pntlem1.z . . . . . . . . 9 (𝜑𝑍 ∈ (𝑊[,)+∞))
281, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27pntlemb 25508 . . . . . . . 8 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
2928simp1d 1136 . . . . . . 7 (𝜑𝑍 ∈ ℝ+)
3029rpred 12076 . . . . . 6 (𝜑𝑍 ∈ ℝ)
3128simp2d 1137 . . . . . . 7 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3231simp1d 1136 . . . . . 6 (𝜑 → 1 < 𝑍)
3330, 32rplogcld 24597 . . . . 5 (𝜑 → (log‘𝑍) ∈ ℝ+)
3422, 33rpmulcld 12092 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
3513, 34rpmulcld 12092 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
3635rpred 12076 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
37 pntlem1.i . . . . . 6 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
38 fzfid 12981 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
3937, 38syl5eqel 2854 . . . . 5 (𝜑𝐼 ∈ Fin)
40 hashcl 13350 . . . . 5 (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ0)
4139, 40syl 17 . . . 4 (𝜑 → (♯‘𝐼) ∈ ℕ0)
4241nn0red 11555 . . 3 (𝜑 → (♯‘𝐼) ∈ ℝ)
4313rpred 12076 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ)
44 pntlem1.v . . . . . . 7 (𝜑𝑉 ∈ ℝ+)
4529, 44rpdivcld 12093 . . . . . 6 (𝜑 → (𝑍 / 𝑉) ∈ ℝ+)
4645relogcld 24591 . . . . 5 (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
4746, 45rerpdivcld 12107 . . . 4 (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
4843, 47remulcld 10273 . . 3 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
4942, 48remulcld 10273 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ∈ ℝ)
50 pntlem1.o . . . 4 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))
51 fzfid 12981 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) ∈ Fin)
5250, 51syl5eqel 2854 . . 3 (𝜑𝑂 ∈ Fin)
537rpred 12076 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
5453adantr 466 . . . . . 6 ((𝜑𝑛𝑂) → 𝑈 ∈ ℝ)
5511simp2d 1137 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℝ+)
56 pntlem1.j . . . . . . . . . . . . 13 (𝜑𝐽 ∈ (𝑀..^𝑁))
57 elfzoelz 12679 . . . . . . . . . . . . 13 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
5856, 57syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℤ)
5958peano2zd 11688 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℤ)
6055, 59rpexpcld 13240 . . . . . . . . . 10 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ+)
6129, 60rpdivcld 12093 . . . . . . . . 9 (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ+)
6261rprege0d 12083 . . . . . . . 8 (𝜑 → ((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))))
63 flge0nn0 12830 . . . . . . . 8 (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0)
64 nn0p1nn 11535 . . . . . . . 8 ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
6562, 63, 643syl 18 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
66 elfzuz 12546 . . . . . . . 8 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
6766, 50eleq2s 2868 . . . . . . 7 (𝑛𝑂𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
68 eluznn 11962 . . . . . . 7 ((((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) → 𝑛 ∈ ℕ)
6965, 67, 68syl2an 577 . . . . . 6 ((𝜑𝑛𝑂) → 𝑛 ∈ ℕ)
7054, 69nndivred 11272 . . . . 5 ((𝜑𝑛𝑂) → (𝑈 / 𝑛) ∈ ℝ)
7129adantr 466 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑍 ∈ ℝ+)
7269nnrpd 12074 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ+)
7371, 72rpdivcld 12093 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 25474 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelrni 6502 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛𝑂) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 71rerpdivcld 12107 . . . . . . 7 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 10271 . . . . . 6 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 14384 . . . . 5 ((𝜑𝑛𝑂) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8070, 79resubcld 10661 . . . 4 ((𝜑𝑛𝑂) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 24591 . . . 4 ((𝜑𝑛𝑂) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 10273 . . 3 ((𝜑𝑛𝑂) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8352, 82fsumrecl 14674 . 2 (𝜑 → Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
84 pntlem1.m . . 3 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
85 pntlem1.n . . 3 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
86 pntlem1.U . . 3 (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)
87 pntlem1.K . . 3 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
88 pntlem1.V . . 3 (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
891, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemr 25513 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9048recnd 10271 . . . . 5 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
91 fsumconst 14730 . . . . 5 ((𝐼 ∈ Fin ∧ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9239, 90, 91syl2anc 567 . . . 4 (𝜑 → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
931, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemq 25512 . . . . 5 (𝜑𝐼𝑂)
9490ralrimivw 3116 . . . . 5 (𝜑 → ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
9552olcd 855 . . . . 5 (𝜑 → (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin))
96 sumss2 14666 . . . . 5 (((𝐼𝑂 ∧ ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) ∧ (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin)) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9793, 94, 95, 96syl21anc 1475 . . . 4 (𝜑 → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9892, 97eqtr3d 2807 . . 3 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9948adantr 466 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
10099adantlr 688 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
101 0red 10244 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ∈ ℝ)
102100, 101ifclda 4260 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ∈ ℝ)
103 breq1 4790 . . . . 5 (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
104 breq1 4790 . . . . 5 (0 = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
10513rpregt0d 12082 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
106105adantr 466 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
107106simpld 478 . . . . . . . 8 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
108 1rp 12040 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
109 rpaddcl 12058 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
110108, 17, 109sylancr 569 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
111110, 44rpmulcld 12092 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ+)
11229, 111rpdivcld 12093 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ+)
113112rprege0d 12083 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
114 flge0nn0 12830 . . . . . . . . . . . . 13 (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0)
115 nn0p1nn 11535 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
117 elfzuz 12546 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
118117, 37eleq2s 2868 . . . . . . . . . . . 12 (𝑛𝐼𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
119 eluznn 11962 . . . . . . . . . . . 12 ((((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) → 𝑛 ∈ ℕ)
120116, 118, 119syl2an 577 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℕ)
121120nnrpd 12074 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ+)
122121relogcld 24591 . . . . . . . . 9 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℝ)
123122, 120nndivred 11272 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘𝑛) / 𝑛) ∈ ℝ)
124107, 123remulcld 10273 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ∈ ℝ)
12593sselda 3753 . . . . . . . 8 ((𝜑𝑛𝐼) → 𝑛𝑂)
126125, 82syldan 573 . . . . . . 7 ((𝜑𝑛𝐼) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
127 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝑛𝐼)
128127, 37syl6eleq 2860 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))))
129 elfzle2 12553 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
130128, 129syl 17 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
13145rpred 12076 . . . . . . . . . . . 12 (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
132131adantr 466 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / 𝑉) ∈ ℝ)
133 elfzelz 12550 . . . . . . . . . . . 12 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ ℤ)
134128, 133syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℤ)
135 flge 12815 . . . . . . . . . . 11 (((𝑍 / 𝑉) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
136132, 134, 135syl2anc 567 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
137130, 136mpbird 247 . . . . . . . . 9 ((𝜑𝑛𝐼) → 𝑛 ≤ (𝑍 / 𝑉))
138120nnred 11238 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ)
139 ere 15026 . . . . . . . . . . . 12 e ∈ ℝ
140139a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ∈ ℝ)
141112rpred 12076 . . . . . . . . . . . 12 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
142141adantr 466 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
143139a1i 11 . . . . . . . . . . . . 13 (𝜑 → e ∈ ℝ)
14429rpsqrtcld 14359 . . . . . . . . . . . . . 14 (𝜑 → (√‘𝑍) ∈ ℝ+)
145144rpred 12076 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ∈ ℝ)
14631simp2d 1137 . . . . . . . . . . . . 13 (𝜑 → e ≤ (√‘𝑍))
147111rpred 12076 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
14860rpred 12076 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
14988simpld 478 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))))
150149simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽)))
15155rpcnd 12078 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℂ)
15255, 58rpexpcld 13240 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝐽) ∈ ℝ+)
153152rpcnd 12078 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐾𝐽) ∈ ℂ)
154151, 153mulcomd 10264 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 · (𝐾𝐽)) = ((𝐾𝐽) · 𝐾))
1551, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 25509 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
156155simp1d 1136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℕ)
157 elfzouz 12683 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ𝑀))
15856, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (ℤ𝑀))
159 eluznn 11962 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ𝑀)) → 𝐽 ∈ ℕ)
160156, 158, 159syl2anc 567 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽 ∈ ℕ)
161160nnnn0d 11554 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℕ0)
162151, 161expp1d 13217 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾𝐽) · 𝐾))
163154, 162eqtr4d 2808 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐾 · (𝐾𝐽)) = (𝐾↑(𝐽 + 1)))
164150, 163breqtrd 4813 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
165147, 148, 164ltled 10388 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
166 fzofzp1 12774 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
16756, 166syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
1681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 25510 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
169167, 168mpdan 661 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
170169simprd 479 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
171147, 148, 145, 165, 170letrd 10397 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
172147, 145, 144lemul2d 12120 . . . . . . . . . . . . . . . 16 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
173171, 172mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
17429rprege0d 12083 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
175 remsqsqrt 14206 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
176174, 175syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
177173, 176breqtrd 4813 . . . . . . . . . . . . . 14 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
178145, 30, 111lemuldivd 12125 . . . . . . . . . . . . . 14 (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
179177, 178mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
180143, 145, 141, 146, 179letrd 10397 . . . . . . . . . . . 12 (𝜑 → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
181180adantr 466 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
182 reflcl 12806 . . . . . . . . . . . . . 14 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
183 peano2re 10412 . . . . . . . . . . . . . 14 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
184141, 182, 1833syl 18 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
185184adantr 466 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
186 fllep1 12811 . . . . . . . . . . . . 13 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
187142, 186syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
188 elfzle1 12552 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
189128, 188syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
190142, 185, 138, 187, 189letrd 10397 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛)
191140, 142, 138, 181, 190letrd 10397 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ 𝑛)
192140, 138, 132, 191, 137letrd 10397 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ (𝑍 / 𝑉))
193 logdivle 24590 . . . . . . . . . 10 (((𝑛 ∈ ℝ ∧ e ≤ 𝑛) ∧ ((𝑍 / 𝑉) ∈ ℝ ∧ e ≤ (𝑍 / 𝑉))) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
194138, 191, 132, 192, 193syl22anc 1477 . . . . . . . . 9 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
195137, 194mpbid 222 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛))
19647adantr 466 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
197 lemul2 11079 . . . . . . . . 9 ((((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ ∧ ((log‘𝑛) / 𝑛) ∈ ℝ ∧ ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸))) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
198196, 123, 106, 197syl3anc 1476 . . . . . . . 8 ((𝜑𝑛𝐼) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
199195, 198mpbid 222 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20013rpcnd 12078 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
201200adantr 466 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℂ)
202122recnd 10271 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℂ)
203121rpcnne0d 12085 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
204 div23 10907 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
205201, 202, 203, 204syl3anc 1476 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
206 divass 10906 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
207201, 202, 203, 206syl3anc 1476 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
208205, 207eqtr3d 2807 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20943adantr 466 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
210209, 120nndivred 11272 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ∈ ℝ)
211125, 80syldan 573 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
212 log1 24554 . . . . . . . . . 10 (log‘1) = 0
213120nnge1d 11266 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 1 ≤ 𝑛)
214 logleb 24571 . . . . . . . . . . . 12 ((1 ∈ ℝ+𝑛 ∈ ℝ+) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
215108, 121, 214sylancr 569 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
216213, 215mpbid 222 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘1) ≤ (log‘𝑛))
217212, 216syl5eqbrr 4823 . . . . . . . . 9 ((𝜑𝑛𝐼) → 0 ≤ (log‘𝑛))
2187rpcnd 12078 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℂ)
219218adantr 466 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑈 ∈ ℂ)
22016rpred 12076 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
221220adantr 466 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝐸 ∈ ℝ)
222221recnd 10271 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝐸 ∈ ℂ)
223 divsubdir 10924 . . . . . . . . . . 11 ((𝑈 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
224219, 222, 203, 223syl3anc 1476 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
225125, 79syldan 573 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
226221, 120nndivred 11272 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝐸 / 𝑛) ∈ ℝ)
227125, 70syldan 573 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑈 / 𝑛) ∈ ℝ)
228125, 76syldan 573 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
229228recnd 10271 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
23029adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ+)
231230rpcnne0d 12085 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
232 divdiv2 10940 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
233229, 231, 203, 232syl3anc 1476 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
234121rpcnd 12078 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑛 ∈ ℂ)
235 div23 10907 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
236229, 234, 231, 235syl3anc 1476 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
237233, 236eqtrd 2805 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
238237fveq2d 6337 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)))
239125, 78syldan 573 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
240239, 234absmuld 14402 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)))
241121rprege0d 12083 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
242 absid 14245 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) → (abs‘𝑛) = 𝑛)
243241, 242syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (abs‘𝑛) = 𝑛)
244243oveq2d 6810 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
245238, 240, 2443eqtrd 2809 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
246 fveq2 6333 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → (𝑅𝑢) = (𝑅‘(𝑍 / 𝑛)))
247 id 22 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → 𝑢 = (𝑍 / 𝑛))
248246, 247oveq12d 6812 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑍 / 𝑛) → ((𝑅𝑢) / 𝑢) = ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)))
249248fveq2d 6337 . . . . . . . . . . . . . . 15 (𝑢 = (𝑍 / 𝑛) → (abs‘((𝑅𝑢) / 𝑢)) = (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))))
250249breq1d 4797 . . . . . . . . . . . . . 14 (𝑢 = (𝑍 / 𝑛) → ((abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸))
25188simprd 479 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
252251adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
25330adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ)
254253, 120nndivred 11272 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ ℝ)
25544rpregt0d 12082 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
256255adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
257 lemuldiv2 11107 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ (𝑉 ∈ ℝ ∧ 0 < 𝑉)) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
258138, 253, 256, 257syl3anc 1476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
259137, 258mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑉 · 𝑛) ≤ 𝑍)
260256simpld 478 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
261260, 253, 121lemuldivd 12125 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑉 ≤ (𝑍 / 𝑛)))
262259, 261mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → 𝑉 ≤ (𝑍 / 𝑛))
263111rpregt0d 12082 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
264263adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
265121rpregt0d 12082 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 < 𝑛))
266 lediv23 11118 . . . . . . . . . . . . . . . . 17 ((𝑍 ∈ ℝ ∧ (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
267253, 264, 265, 266syl3anc 1476 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
268190, 267mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))
26944rpred 12076 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 ∈ ℝ)
270269adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
271147adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
272 elicc2 12444 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
273270, 271, 272syl2anc 567 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
274254, 262, 268, 273mpbir3and 1427 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)))
275250, 252, 274rspcdva 3467 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸)
276245, 275eqbrtrrd 4811 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸)
277225, 221, 121lemuldivd 12125 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛)))
278276, 277mpbid 222 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛))
279225, 226, 227, 278lesub2dd 10847 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (𝐸 / 𝑛)) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
280224, 279eqbrtrd 4809 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
281210, 211, 122, 217, 280lemul1ad 11166 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
282208, 281eqbrtrrd 4811 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28399, 124, 126, 199, 282letrd 10397 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
284283adantlr 688 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28569nnred 11238 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ)
28629, 152rpdivcld 12093 . . . . . . . . . . 11 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ+)
287286rpred 12076 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ)
288287adantr 466 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ∈ ℝ)
28923simpld 478 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ+)
29029, 289rpdivcld 12093 . . . . . . . . . . 11 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
291290rpred 12076 . . . . . . . . . 10 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
292291adantr 466 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑌) ∈ ℝ)
293 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑛𝑂) → 𝑛𝑂)
294293, 50syl6eleq 2860 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))))
295 elfzle2 12553 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
296294, 295syl 17 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
29769nnzd 11684 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ ℤ)
298 flge 12815 . . . . . . . . . . 11 (((𝑍 / (𝐾𝐽)) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
299288, 297, 298syl2anc 567 . . . . . . . . . 10 ((𝜑𝑛𝑂) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
300296, 299mpbird 247 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / (𝐾𝐽)))
301289rpred 12076 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
30224simpld 478 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ ℝ+)
303302rpred 12076 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
304152rpred 12076 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐽) ∈ ℝ)
30524simprd 479 . . . . . . . . . . . . 13 (𝜑𝑌 < 𝑋)
306301, 303, 305ltled 10388 . . . . . . . . . . . 12 (𝜑𝑌𝑋)
307 elfzofz 12694 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (𝑀...𝑁))
30856, 307syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (𝑀...𝑁))
3091, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 25510 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
310308, 309mpdan 661 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
311310simpld 478 . . . . . . . . . . . . 13 (𝜑𝑋 < (𝐾𝐽))
312303, 304, 311ltled 10388 . . . . . . . . . . . 12 (𝜑𝑋 ≤ (𝐾𝐽))
313301, 303, 304, 306, 312letrd 10397 . . . . . . . . . . 11 (𝜑𝑌 ≤ (𝐾𝐽))
314289, 152, 29lediv2d 12100 . . . . . . . . . . 11 (𝜑 → (𝑌 ≤ (𝐾𝐽) ↔ (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌)))
315313, 314mpbid 222 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
316315adantr 466 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
317285, 288, 292, 300, 316letrd 10397 . . . . . . . 8 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / 𝑌))
31869, 317jca 497 . . . . . . 7 ((𝜑𝑛𝑂) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌)))
3191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 25511 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
320318, 319syldan 573 . . . . . 6 ((𝜑𝑛𝑂) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
321320adantr 466 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
322103, 104, 284, 321ifbothda 4263 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32352, 102, 82, 322fsumle 14739 . . 3 (𝜑 → Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32498, 323eqbrtrd 4809 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32536, 49, 83, 89, 324letrd 10397 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 828  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  wss 3724  ifcif 4226   class class class wbr 4787  cmpt 4864  cfv 6032  (class class class)co 6794  Fincfn 8110  cc 10137  cr 10138  0cc0 10139  1c1 10140   + caddc 10142   · cmul 10144  +∞cpnf 10274   < clt 10277  cle 10278  cmin 10469   / cdiv 10887  cn 11223  2c2 11273  3c3 11274  4c4 11275  8c8 11279  0cn0 11495  cz 11580  cdc 11696  cuz 11889  +crp 12036  (,)cioo 12381  [,)cico 12383  [,]cicc 12384  ...cfz 12534  ..^cfzo 12674  cfl 12800  cexp 13068  chash 13322  csqrt 14182  abscabs 14183  Σcsu 14625  expce 14999  eceu 15000  logclog 24523  ψcchp 25041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217  ax-addf 10218  ax-mulf 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-of 7045  df-om 7214  df-1st 7316  df-2nd 7317  df-supp 7448  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-pm 8013  df-ixp 8064  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8966  df-cda 9193  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-q 11993  df-rp 12037  df-xneg 12152  df-xadd 12153  df-xmul 12154  df-ioo 12385  df-ioc 12386  df-ico 12387  df-icc 12388  df-fz 12535  df-fzo 12675  df-fl 12802  df-mod 12878  df-seq 13010  df-exp 13069  df-fac 13266  df-bc 13295  df-hash 13323  df-shft 14016  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-limsup 14411  df-clim 14428  df-rlim 14429  df-sum 14626  df-ef 15005  df-e 15006  df-sin 15007  df-cos 15008  df-pi 15010  df-dvds 15191  df-gcd 15426  df-prm 15594  df-pc 15750  df-struct 16067  df-ndx 16068  df-slot 16069  df-base 16071  df-sets 16072  df-ress 16073  df-plusg 16163  df-mulr 16164  df-starv 16165  df-sca 16166  df-vsca 16167  df-ip 16168  df-tset 16169  df-ple 16170  df-ds 16173  df-unif 16174  df-hom 16175  df-cco 16176  df-rest 16292  df-topn 16293  df-0g 16311  df-gsum 16312  df-topgen 16313  df-pt 16314  df-prds 16317  df-xrs 16371  df-qtop 16376  df-imas 16377  df-xps 16379  df-mre 16455  df-mrc 16456  df-acs 16458  df-mgm 17451  df-sgrp 17493  df-mnd 17504  df-submnd 17545  df-mulg 17750  df-cntz 17958  df-cmn 18403  df-psmet 19954  df-xmet 19955  df-met 19956  df-bl 19957  df-mopn 19958  df-fbas 19959  df-fg 19960  df-cnfld 19963  df-top 20920  df-topon 20937  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-limc 23851  df-dv 23852  df-log 24525  df-vma 25046  df-chp 25047
This theorem is referenced by:  pntlemi  25515
  Copyright terms: Public domain W3C validator