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

Theorem pntlemj 26286
 Description: Lemma for pnt 26297. The induction step. Using pntibnd 26276, 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 26278 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1141 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1141 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 26277 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1139 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1139 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1715, 16rpmulcld 12488 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
18 8nn 11769 . . . . . . 7 8 ∈ ℕ
19 nnrp 12441 . . . . . . 7 (8 ∈ ℕ → 8 ∈ ℝ+)
2018, 19ax-mp 5 . . . . . 6 8 ∈ ℝ+
21 rpdivcl 12455 . . . . . 6 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
2217, 20, 21sylancl 589 . . . . 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 26280 . . . . . . . 8 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
2928simp1d 1139 . . . . . . 7 (𝜑𝑍 ∈ ℝ+)
3029rpred 12472 . . . . . 6 (𝜑𝑍 ∈ ℝ)
3128simp2d 1140 . . . . . . 7 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3231simp1d 1139 . . . . . 6 (𝜑 → 1 < 𝑍)
3330, 32rplogcld 25319 . . . . 5 (𝜑 → (log‘𝑍) ∈ ℝ+)
3422, 33rpmulcld 12488 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
3513, 34rpmulcld 12488 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
3635rpred 12472 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
37 pntlem1.i . . . . . 6 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
38 fzfid 13390 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
3937, 38eqeltrid 2856 . . . . 5 (𝜑𝐼 ∈ Fin)
40 hashcl 13767 . . . . 5 (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ0)
4139, 40syl 17 . . . 4 (𝜑 → (♯‘𝐼) ∈ ℕ0)
4241nn0red 11995 . . 3 (𝜑 → (♯‘𝐼) ∈ ℝ)
4313rpred 12472 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ)
44 pntlem1.v . . . . . . 7 (𝜑𝑉 ∈ ℝ+)
4529, 44rpdivcld 12489 . . . . . 6 (𝜑 → (𝑍 / 𝑉) ∈ ℝ+)
4645relogcld 25313 . . . . 5 (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
4746, 45rerpdivcld 12503 . . . 4 (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
4843, 47remulcld 10709 . . 3 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
4942, 48remulcld 10709 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ∈ ℝ)
50 pntlem1.o . . . 4 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))
51 fzfid 13390 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) ∈ Fin)
5250, 51eqeltrid 2856 . . 3 (𝜑𝑂 ∈ Fin)
537rpred 12472 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
5453adantr 484 . . . . . 6 ((𝜑𝑛𝑂) → 𝑈 ∈ ℝ)
5511simp2d 1140 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℝ+)
56 pntlem1.j . . . . . . . . . . . . 13 (𝜑𝐽 ∈ (𝑀..^𝑁))
57 elfzoelz 13087 . . . . . . . . . . . . 13 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
5856, 57syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℤ)
5958peano2zd 12129 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℤ)
6055, 59rpexpcld 13658 . . . . . . . . . 10 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ+)
6129, 60rpdivcld 12489 . . . . . . . . 9 (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ+)
6261rprege0d 12479 . . . . . . . 8 (𝜑 → ((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))))
63 flge0nn0 13239 . . . . . . . 8 (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0)
64 nn0p1nn 11973 . . . . . . . 8 ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
6562, 63, 643syl 18 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
66 elfzuz 12952 . . . . . . . 8 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
6766, 50eleq2s 2870 . . . . . . 7 (𝑛𝑂𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
68 eluznn 12358 . . . . . . 7 ((((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) → 𝑛 ∈ ℕ)
6965, 67, 68syl2an 598 . . . . . 6 ((𝜑𝑛𝑂) → 𝑛 ∈ ℕ)
7054, 69nndivred 11728 . . . . 5 ((𝜑𝑛𝑂) → (𝑈 / 𝑛) ∈ ℝ)
7129adantr 484 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑍 ∈ ℝ+)
7269nnrpd 12470 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ+)
7371, 72rpdivcld 12489 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 26246 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelrni 6841 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛𝑂) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 71rerpdivcld 12503 . . . . . . 7 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 10707 . . . . . 6 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 14844 . . . . 5 ((𝜑𝑛𝑂) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8070, 79resubcld 11106 . . . 4 ((𝜑𝑛𝑂) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 25313 . . . 4 ((𝜑𝑛𝑂) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 10709 . . 3 ((𝜑𝑛𝑂) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8352, 82fsumrecl 15139 . 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 26285 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9048recnd 10707 . . . . 5 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
91 fsumconst 15193 . . . . 5 ((𝐼 ∈ Fin ∧ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9239, 90, 91syl2anc 587 . . . 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 26284 . . . . 5 (𝜑𝐼𝑂)
9490ralrimivw 3114 . . . . 5 (𝜑 → ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
9552olcd 871 . . . . 5 (𝜑 → (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin))
96 sumss2 15131 . . . . 5 (((𝐼𝑂 ∧ ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) ∧ (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin)) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9793, 94, 95, 96syl21anc 836 . . . 4 (𝜑 → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9892, 97eqtr3d 2795 . . 3 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9948adantr 484 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
10099adantlr 714 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
101 0red 10682 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ∈ ℝ)
102100, 101ifclda 4455 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ∈ ℝ)
103 breq1 5035 . . . . 5 (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
104 breq1 5035 . . . . 5 (0 = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
10513rpregt0d 12478 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
106105adantr 484 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
107106simpld 498 . . . . . . . 8 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
108 1rp 12434 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
109 rpaddcl 12452 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
110108, 17, 109sylancr 590 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
111110, 44rpmulcld 12488 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ+)
11229, 111rpdivcld 12489 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ+)
113112rprege0d 12479 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
114 flge0nn0 13239 . . . . . . . . . . . . 13 (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0)
115 nn0p1nn 11973 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
117 elfzuz 12952 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
118117, 37eleq2s 2870 . . . . . . . . . . . 12 (𝑛𝐼𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
119 eluznn 12358 . . . . . . . . . . . 12 ((((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) → 𝑛 ∈ ℕ)
120116, 118, 119syl2an 598 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℕ)
121120nnrpd 12470 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ+)
122121relogcld 25313 . . . . . . . . 9 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℝ)
123122, 120nndivred 11728 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘𝑛) / 𝑛) ∈ ℝ)
124107, 123remulcld 10709 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ∈ ℝ)
12593sselda 3892 . . . . . . . 8 ((𝜑𝑛𝐼) → 𝑛𝑂)
126125, 82syldan 594 . . . . . . 7 ((𝜑𝑛𝐼) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
127 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝑛𝐼)
128127, 37eleqtrdi 2862 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))))
129 elfzle2 12960 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
130128, 129syl 17 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
13145rpred 12472 . . . . . . . . . . . 12 (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
132131adantr 484 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / 𝑉) ∈ ℝ)
133 elfzelz 12956 . . . . . . . . . . . 12 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ ℤ)
134128, 133syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℤ)
135 flge 13224 . . . . . . . . . . 11 (((𝑍 / 𝑉) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
136132, 134, 135syl2anc 587 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
137130, 136mpbird 260 . . . . . . . . 9 ((𝜑𝑛𝐼) → 𝑛 ≤ (𝑍 / 𝑉))
138120nnred 11689 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ)
139 ere 15490 . . . . . . . . . . . 12 e ∈ ℝ
140139a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ∈ ℝ)
141112rpred 12472 . . . . . . . . . . . 12 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
142141adantr 484 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
143139a1i 11 . . . . . . . . . . . . 13 (𝜑 → e ∈ ℝ)
14429rpsqrtcld 14819 . . . . . . . . . . . . . 14 (𝜑 → (√‘𝑍) ∈ ℝ+)
145144rpred 12472 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ∈ ℝ)
14631simp2d 1140 . . . . . . . . . . . . 13 (𝜑 → e ≤ (√‘𝑍))
147111rpred 12472 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
14860rpred 12472 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
14988simpld 498 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))))
150149simprd 499 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽)))
15155rpcnd 12474 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℂ)
15255, 58rpexpcld 13658 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝐽) ∈ ℝ+)
153152rpcnd 12474 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐾𝐽) ∈ ℂ)
154151, 153mulcomd 10700 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 · (𝐾𝐽)) = ((𝐾𝐽) · 𝐾))
1551, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 26281 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
156155simp1d 1139 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℕ)
157 elfzouz 13091 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ𝑀))
15856, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (ℤ𝑀))
159 eluznn 12358 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ𝑀)) → 𝐽 ∈ ℕ)
160156, 158, 159syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽 ∈ ℕ)
161160nnnn0d 11994 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℕ0)
162151, 161expp1d 13561 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾𝐽) · 𝐾))
163154, 162eqtr4d 2796 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐾 · (𝐾𝐽)) = (𝐾↑(𝐽 + 1)))
164150, 163breqtrd 5058 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
165147, 148, 164ltled 10826 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
166 fzofzp1 13183 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
16756, 166syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
1681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 26282 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
169167, 168mpdan 686 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
170169simprd 499 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
171147, 148, 145, 165, 170letrd 10835 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
172147, 145, 144lemul2d 12516 . . . . . . . . . . . . . . . 16 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
173171, 172mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
17429rprege0d 12479 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
175 remsqsqrt 14664 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
176174, 175syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
177173, 176breqtrd 5058 . . . . . . . . . . . . . 14 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
178145, 30, 111lemuldivd 12521 . . . . . . . . . . . . . 14 (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
179177, 178mpbid 235 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
180143, 145, 141, 146, 179letrd 10835 . . . . . . . . . . . 12 (𝜑 → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
181180adantr 484 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
182 reflcl 13215 . . . . . . . . . . . . . 14 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
183 peano2re 10851 . . . . . . . . . . . . . 14 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
184141, 182, 1833syl 18 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
185184adantr 484 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
186 fllep1 13220 . . . . . . . . . . . . 13 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
187142, 186syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
188 elfzle1 12959 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
189128, 188syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
190142, 185, 138, 187, 189letrd 10835 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛)
191140, 142, 138, 181, 190letrd 10835 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ 𝑛)
192140, 138, 132, 191, 137letrd 10835 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ (𝑍 / 𝑉))
193 logdivle 25312 . . . . . . . . . 10 (((𝑛 ∈ ℝ ∧ e ≤ 𝑛) ∧ ((𝑍 / 𝑉) ∈ ℝ ∧ e ≤ (𝑍 / 𝑉))) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
194138, 191, 132, 192, 193syl22anc 837 . . . . . . . . 9 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
195137, 194mpbid 235 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛))
19647adantr 484 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
197 lemul2 11531 . . . . . . . . 9 ((((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ ∧ ((log‘𝑛) / 𝑛) ∈ ℝ ∧ ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸))) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
198196, 123, 106, 197syl3anc 1368 . . . . . . . 8 ((𝜑𝑛𝐼) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
199195, 198mpbid 235 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20013rpcnd 12474 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
201200adantr 484 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℂ)
202122recnd 10707 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℂ)
203121rpcnne0d 12481 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
204 div23 11355 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
205201, 202, 203, 204syl3anc 1368 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
206 divass 11354 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
207201, 202, 203, 206syl3anc 1368 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
208205, 207eqtr3d 2795 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20943adantr 484 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
210209, 120nndivred 11728 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ∈ ℝ)
211125, 80syldan 594 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
212 log1 25276 . . . . . . . . . 10 (log‘1) = 0
213120nnge1d 11722 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 1 ≤ 𝑛)
214 logleb 25293 . . . . . . . . . . . 12 ((1 ∈ ℝ+𝑛 ∈ ℝ+) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
215108, 121, 214sylancr 590 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
216213, 215mpbid 235 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘1) ≤ (log‘𝑛))
217212, 216eqbrtrrid 5068 . . . . . . . . 9 ((𝜑𝑛𝐼) → 0 ≤ (log‘𝑛))
2187rpcnd 12474 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℂ)
219218adantr 484 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑈 ∈ ℂ)
22016rpred 12472 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
221220adantr 484 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝐸 ∈ ℝ)
222221recnd 10707 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝐸 ∈ ℂ)
223 divsubdir 11372 . . . . . . . . . . 11 ((𝑈 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
224219, 222, 203, 223syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
225125, 79syldan 594 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
226221, 120nndivred 11728 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝐸 / 𝑛) ∈ ℝ)
227125, 70syldan 594 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑈 / 𝑛) ∈ ℝ)
228125, 76syldan 594 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
229228recnd 10707 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
23029adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ+)
231230rpcnne0d 12481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
232 divdiv2 11390 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
233229, 231, 203, 232syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
234121rpcnd 12474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑛 ∈ ℂ)
235 div23 11355 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
236229, 234, 231, 235syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
237233, 236eqtrd 2793 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
238237fveq2d 6662 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)))
239125, 78syldan 594 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
240239, 234absmuld 14862 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)))
241121rprege0d 12479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
242 absid 14704 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) → (abs‘𝑛) = 𝑛)
243241, 242syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (abs‘𝑛) = 𝑛)
244243oveq2d 7166 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
245238, 240, 2443eqtrd 2797 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
246 fveq2 6658 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → (𝑅𝑢) = (𝑅‘(𝑍 / 𝑛)))
247 id 22 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → 𝑢 = (𝑍 / 𝑛))
248246, 247oveq12d 7168 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑍 / 𝑛) → ((𝑅𝑢) / 𝑢) = ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)))
249248fveq2d 6662 . . . . . . . . . . . . . . 15 (𝑢 = (𝑍 / 𝑛) → (abs‘((𝑅𝑢) / 𝑢)) = (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))))
250249breq1d 5042 . . . . . . . . . . . . . 14 (𝑢 = (𝑍 / 𝑛) → ((abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸))
25188simprd 499 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
252251adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
25330adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ)
254253, 120nndivred 11728 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ ℝ)
25544rpregt0d 12478 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
256255adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
257 lemuldiv2 11559 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ (𝑉 ∈ ℝ ∧ 0 < 𝑉)) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
258138, 253, 256, 257syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
259137, 258mpbird 260 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑉 · 𝑛) ≤ 𝑍)
260256simpld 498 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
261260, 253, 121lemuldivd 12521 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑉 ≤ (𝑍 / 𝑛)))
262259, 261mpbid 235 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → 𝑉 ≤ (𝑍 / 𝑛))
263111rpregt0d 12478 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
264263adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
265121rpregt0d 12478 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 < 𝑛))
266 lediv23 11570 . . . . . . . . . . . . . . . . 17 ((𝑍 ∈ ℝ ∧ (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
267253, 264, 265, 266syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
268190, 267mpbid 235 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))
26944rpred 12472 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 ∈ ℝ)
270269adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
271147adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
272 elicc2 12844 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
273270, 271, 272syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
274254, 262, 268, 273mpbir3and 1339 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)))
275250, 252, 274rspcdva 3543 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸)
276245, 275eqbrtrrd 5056 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸)
277225, 221, 121lemuldivd 12521 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛)))
278276, 277mpbid 235 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛))
279225, 226, 227, 278lesub2dd 11295 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (𝐸 / 𝑛)) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
280224, 279eqbrtrd 5054 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
281210, 211, 122, 217, 280lemul1ad 11617 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
282208, 281eqbrtrrd 5056 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28399, 124, 126, 199, 282letrd 10835 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
284283adantlr 714 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28569nnred 11689 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ)
28629, 152rpdivcld 12489 . . . . . . . . . . 11 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ+)
287286rpred 12472 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ)
288287adantr 484 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ∈ ℝ)
28923simpld 498 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ+)
29029, 289rpdivcld 12489 . . . . . . . . . . 11 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
291290rpred 12472 . . . . . . . . . 10 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
292291adantr 484 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑌) ∈ ℝ)
293 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑛𝑂) → 𝑛𝑂)
294293, 50eleqtrdi 2862 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))))
295 elfzle2 12960 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
296294, 295syl 17 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
29769nnzd 12125 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ ℤ)
298 flge 13224 . . . . . . . . . . 11 (((𝑍 / (𝐾𝐽)) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
299288, 297, 298syl2anc 587 . . . . . . . . . 10 ((𝜑𝑛𝑂) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
300296, 299mpbird 260 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / (𝐾𝐽)))
301289rpred 12472 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
30224simpld 498 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ ℝ+)
303302rpred 12472 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
304152rpred 12472 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐽) ∈ ℝ)
30524simprd 499 . . . . . . . . . . . . 13 (𝜑𝑌 < 𝑋)
306301, 303, 305ltled 10826 . . . . . . . . . . . 12 (𝜑𝑌𝑋)
307 elfzofz 13102 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (𝑀...𝑁))
30856, 307syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (𝑀...𝑁))
3091, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 26282 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
310308, 309mpdan 686 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
311310simpld 498 . . . . . . . . . . . . 13 (𝜑𝑋 < (𝐾𝐽))
312303, 304, 311ltled 10826 . . . . . . . . . . . 12 (𝜑𝑋 ≤ (𝐾𝐽))
313301, 303, 304, 306, 312letrd 10835 . . . . . . . . . . 11 (𝜑𝑌 ≤ (𝐾𝐽))
314289, 152, 29lediv2d 12496 . . . . . . . . . . 11 (𝜑 → (𝑌 ≤ (𝐾𝐽) ↔ (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌)))
315313, 314mpbid 235 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
316315adantr 484 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
317285, 288, 292, 300, 316letrd 10835 . . . . . . . 8 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / 𝑌))
31869, 317jca 515 . . . . . . 7 ((𝜑𝑛𝑂) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌)))
3191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 26283 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
320318, 319syldan 594 . . . . . 6 ((𝜑𝑛𝑂) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
321320adantr 484 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
322103, 104, 284, 321ifbothda 4458 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32352, 102, 82, 322fsumle 15202 . . 3 (𝜑 → Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32498, 323eqbrtrd 5054 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32536, 49, 83, 89, 324letrd 10835 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071   ⊆ wss 3858  ifcif 4420   class class class wbr 5032   ↦ cmpt 5112  ‘cfv 6335  (class class class)co 7150  Fincfn 8527  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578   · cmul 10580  +∞cpnf 10710   < clt 10713   ≤ cle 10714   − cmin 10908   / cdiv 11335  ℕcn 11674  2c2 11729  3c3 11730  4c4 11731  8c8 11735  ℕ0cn0 11934  ℤcz 12020  ;cdc 12137  ℤ≥cuz 12282  ℝ+crp 12430  (,)cioo 12779  [,)cico 12781  [,]cicc 12782  ...cfz 12939  ..^cfzo 13082  ⌊cfl 13209  ↑cexp 13479  ♯chash 13740  √csqrt 14640  abscabs 14641  Σcsu 15090  expce 15463  eceu 15464  logclog 25245  ψcchp 25777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-supp 7836  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-er 8299  df-map 8418  df-pm 8419  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-fsupp 8867  df-fi 8908  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-z 12021  df-dec 12138  df-uz 12283  df-q 12389  df-rp 12431  df-xneg 12548  df-xadd 12549  df-xmul 12550  df-ioo 12783  df-ioc 12784  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-fac 13684  df-bc 13713  df-hash 13741  df-shft 14474  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-limsup 14876  df-clim 14893  df-rlim 14894  df-sum 15091  df-ef 15469  df-e 15470  df-sin 15471  df-cos 15472  df-pi 15474  df-dvds 15656  df-gcd 15894  df-prm 16068  df-pc 16229  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-starv 16638  df-sca 16639  df-vsca 16640  df-ip 16641  df-tset 16642  df-ple 16643  df-ds 16645  df-unif 16646  df-hom 16647  df-cco 16648  df-rest 16754  df-topn 16755  df-0g 16773  df-gsum 16774  df-topgen 16775  df-pt 16776  df-prds 16779  df-xrs 16833  df-qtop 16838  df-imas 16839  df-xps 16841  df-mre 16915  df-mrc 16916  df-acs 16918  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-submnd 18023  df-mulg 18292  df-cntz 18514  df-cmn 18975  df-psmet 20158  df-xmet 20159  df-met 20160  df-bl 20161  df-mopn 20162  df-fbas 20163  df-fg 20164  df-cnfld 20167  df-top 21594  df-topon 21611  df-topsp 21633  df-bases 21646  df-cld 21719  df-ntr 21720  df-cls 21721  df-nei 21798  df-lp 21836  df-perf 21837  df-cn 21927  df-cnp 21928  df-haus 22015  df-tx 22262  df-hmeo 22455  df-fil 22546  df-fm 22638  df-flim 22639  df-flf 22640  df-xms 23022  df-ms 23023  df-tms 23024  df-cncf 23579  df-limc 24565  df-dv 24566  df-log 25247  df-vma 25782  df-chp 25783 This theorem is referenced by:  pntlemi  26287
 Copyright terms: Public domain W3C validator