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

Theorem pntlemj 25582
Description: Lemma for pnt 25593. The induction step. Using pntibnd 25572, 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 25574 . . . . . 6 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1211simp3d 1174 . . . . 5 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
1312simp3d 1174 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
141, 2, 3, 4, 5, 6pntlemd 25573 . . . . . . . 8 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
1514simp1d 1172 . . . . . . 7 (𝜑𝐿 ∈ ℝ+)
1611simp1d 1172 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1715, 16rpmulcld 12085 . . . . . 6 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
18 8nn 11371 . . . . . . 7 8 ∈ ℕ
19 nnrp 12040 . . . . . . 7 (8 ∈ ℕ → 8 ∈ ℝ+)
2018, 19ax-mp 5 . . . . . 6 8 ∈ ℝ+
21 rpdivcl 12053 . . . . . 6 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
2217, 20, 21sylancl 580 . . . . 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 25576 . . . . . . . 8 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
2928simp1d 1172 . . . . . . 7 (𝜑𝑍 ∈ ℝ+)
3029rpred 12069 . . . . . 6 (𝜑𝑍 ∈ ℝ)
3128simp2d 1173 . . . . . . 7 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
3231simp1d 1172 . . . . . 6 (𝜑 → 1 < 𝑍)
3330, 32rplogcld 24665 . . . . 5 (𝜑 → (log‘𝑍) ∈ ℝ+)
3422, 33rpmulcld 12085 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
3513, 34rpmulcld 12085 . . 3 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ+)
3635rpred 12069 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ∈ ℝ)
37 pntlem1.i . . . . . 6 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
38 fzfid 12979 . . . . . 6 (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
3937, 38syl5eqel 2847 . . . . 5 (𝜑𝐼 ∈ Fin)
40 hashcl 13348 . . . . 5 (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ0)
4139, 40syl 17 . . . 4 (𝜑 → (♯‘𝐼) ∈ ℕ0)
4241nn0red 11598 . . 3 (𝜑 → (♯‘𝐼) ∈ ℝ)
4313rpred 12069 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ)
44 pntlem1.v . . . . . . 7 (𝜑𝑉 ∈ ℝ+)
4529, 44rpdivcld 12086 . . . . . 6 (𝜑 → (𝑍 / 𝑉) ∈ ℝ+)
4645relogcld 24659 . . . . 5 (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
4746, 45rerpdivcld 12100 . . . 4 (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
4843, 47remulcld 10323 . . 3 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
4942, 48remulcld 10323 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ∈ ℝ)
50 pntlem1.o . . . 4 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))
51 fzfid 12979 . . . 4 (𝜑 → (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) ∈ Fin)
5250, 51syl5eqel 2847 . . 3 (𝜑𝑂 ∈ Fin)
537rpred 12069 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
5453adantr 472 . . . . . 6 ((𝜑𝑛𝑂) → 𝑈 ∈ ℝ)
5511simp2d 1173 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℝ+)
56 pntlem1.j . . . . . . . . . . . . 13 (𝜑𝐽 ∈ (𝑀..^𝑁))
57 elfzoelz 12677 . . . . . . . . . . . . 13 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
5856, 57syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℤ)
5958peano2zd 11731 . . . . . . . . . . 11 (𝜑 → (𝐽 + 1) ∈ ℤ)
6055, 59rpexpcld 13238 . . . . . . . . . 10 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ+)
6129, 60rpdivcld 12086 . . . . . . . . 9 (𝜑 → (𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ+)
6261rprege0d 12076 . . . . . . . 8 (𝜑 → ((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))))
63 flge0nn0 12828 . . . . . . . 8 (((𝑍 / (𝐾↑(𝐽 + 1))) ∈ ℝ ∧ 0 ≤ (𝑍 / (𝐾↑(𝐽 + 1)))) → (⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0)
64 nn0p1nn 11578 . . . . . . . 8 ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) ∈ ℕ0 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
6562, 63, 643syl 18 . . . . . . 7 (𝜑 → ((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ)
66 elfzuz 12544 . . . . . . . 8 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
6766, 50eleq2s 2861 . . . . . . 7 (𝑛𝑂𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)))
68 eluznn 11958 . . . . . . 7 ((((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1))) → 𝑛 ∈ ℕ)
6965, 67, 68syl2an 589 . . . . . 6 ((𝜑𝑛𝑂) → 𝑛 ∈ ℕ)
7054, 69nndivred 11325 . . . . 5 ((𝜑𝑛𝑂) → (𝑈 / 𝑛) ∈ ℝ)
7129adantr 472 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑍 ∈ ℝ+)
7269nnrpd 12067 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ+)
7371, 72rpdivcld 12086 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑛) ∈ ℝ+)
741pntrf 25542 . . . . . . . . . 10 𝑅:ℝ+⟶ℝ
7574ffvelrni 6547 . . . . . . . . 9 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7673, 75syl 17 . . . . . . . 8 ((𝜑𝑛𝑂) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
7776, 71rerpdivcld 12100 . . . . . . 7 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
7877recnd 10321 . . . . . 6 ((𝜑𝑛𝑂) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
7978abscld 14461 . . . . 5 ((𝜑𝑛𝑂) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
8070, 79resubcld 10711 . . . 4 ((𝜑𝑛𝑂) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
8172relogcld 24659 . . . 4 ((𝜑𝑛𝑂) → (log‘𝑛) ∈ ℝ)
8280, 81remulcld 10323 . . 3 ((𝜑𝑛𝑂) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
8352, 82fsumrecl 14751 . 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 25581 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9048recnd 10321 . . . . 5 (𝜑 → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
91 fsumconst 14807 . . . . 5 ((𝐼 ∈ Fin ∧ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
9239, 90, 91syl2anc 579 . . . 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 25580 . . . . 5 (𝜑𝐼𝑂)
9490ralrimivw 3113 . . . . 5 (𝜑 → ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ)
9552olcd 900 . . . . 5 (𝜑 → (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin))
96 sumss2 14743 . . . . 5 (((𝐼𝑂 ∧ ∀𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℂ) ∧ (𝑂 ⊆ (ℤ‘1) ∨ 𝑂 ∈ Fin)) → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9793, 94, 95, 96syl21anc 866 . . . 4 (𝜑 → Σ𝑛𝐼 ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9892, 97eqtr3d 2800 . . 3 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0))
9948adantr 472 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
10099adantlr 706 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
101 0red 10296 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ∈ ℝ)
102100, 101ifclda 4276 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ∈ ℝ)
103 breq1 4811 . . . . 5 (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
104 breq1 4811 . . . . 5 (0 = if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) → (0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
10513rpregt0d 12075 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
106105adantr 472 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸)))
107106simpld 488 . . . . . . . 8 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
108 1rp 12031 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ+
109 rpaddcl 12051 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
110108, 17, 109sylancr 581 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
111110, 44rpmulcld 12085 . . . . . . . . . . . . . . 15 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ+)
11229, 111rpdivcld 12086 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ+)
113112rprege0d 12076 . . . . . . . . . . . . 13 (𝜑 → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
114 flge0nn0 12828 . . . . . . . . . . . . 13 (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ 0 ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0)
115 nn0p1nn 11578 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℕ0 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
116113, 114, 1153syl 18 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ)
117 elfzuz 12544 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
118117, 37eleq2s 2861 . . . . . . . . . . . 12 (𝑛𝐼𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
119 eluznn 11958 . . . . . . . . . . . 12 ((((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) → 𝑛 ∈ ℕ)
120116, 118, 119syl2an 589 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℕ)
121120nnrpd 12067 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ+)
122121relogcld 24659 . . . . . . . . 9 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℝ)
123122, 120nndivred 11325 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘𝑛) / 𝑛) ∈ ℝ)
124107, 123remulcld 10323 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ∈ ℝ)
12593sselda 3760 . . . . . . . 8 ((𝜑𝑛𝐼) → 𝑛𝑂)
126125, 82syldan 585 . . . . . . 7 ((𝜑𝑛𝐼) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
127 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝑛𝐼)
128127, 37syl6eleq 2853 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))))
129 elfzle2 12551 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
130128, 129syl 17 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ≤ (⌊‘(𝑍 / 𝑉)))
13145rpred 12069 . . . . . . . . . . . 12 (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
132131adantr 472 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / 𝑉) ∈ ℝ)
133 elfzelz 12548 . . . . . . . . . . . 12 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → 𝑛 ∈ ℤ)
134128, 133syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑛 ∈ ℤ)
135 flge 12813 . . . . . . . . . . 11 (((𝑍 / 𝑉) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
136132, 134, 135syl2anc 579 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ 𝑛 ≤ (⌊‘(𝑍 / 𝑉))))
137130, 136mpbird 248 . . . . . . . . 9 ((𝜑𝑛𝐼) → 𝑛 ≤ (𝑍 / 𝑉))
138120nnred 11290 . . . . . . . . . 10 ((𝜑𝑛𝐼) → 𝑛 ∈ ℝ)
139 ere 15102 . . . . . . . . . . . 12 e ∈ ℝ
140139a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ∈ ℝ)
141112rpred 12069 . . . . . . . . . . . 12 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
142141adantr 472 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
143139a1i 11 . . . . . . . . . . . . 13 (𝜑 → e ∈ ℝ)
14429rpsqrtcld 14436 . . . . . . . . . . . . . 14 (𝜑 → (√‘𝑍) ∈ ℝ+)
145144rpred 12069 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ∈ ℝ)
14631simp2d 1173 . . . . . . . . . . . . 13 (𝜑 → e ≤ (√‘𝑍))
147111rpred 12069 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
14860rpred 12069 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
14988simpld 488 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))))
150149simprd 489 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽)))
15155rpcnd 12071 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℂ)
15255, 58rpexpcld 13238 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾𝐽) ∈ ℝ+)
153152rpcnd 12071 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐾𝐽) ∈ ℂ)
154151, 153mulcomd 10314 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 · (𝐾𝐽)) = ((𝐾𝐽) · 𝐾))
1551, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 25577 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
156155simp1d 1172 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℕ)
157 elfzouz 12681 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ𝑀))
15856, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (ℤ𝑀))
159 eluznn 11958 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ𝑀)) → 𝐽 ∈ ℕ)
160156, 158, 159syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐽 ∈ ℕ)
161160nnnn0d 11597 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℕ0)
162151, 161expp1d 13215 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾𝐽) · 𝐾))
163154, 162eqtr4d 2801 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐾 · (𝐾𝐽)) = (𝐾↑(𝐽 + 1)))
164150, 163breqtrd 4834 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
165147, 148, 164ltled 10438 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
166 fzofzp1 12772 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
16756, 166syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
1681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 25578 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
169167, 168mpdan 678 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
170169simprd 489 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
171147, 148, 145, 165, 170letrd 10447 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
172147, 145, 144lemul2d 12113 . . . . . . . . . . . . . . . 16 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
173171, 172mpbid 223 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
17429rprege0d 12076 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
175 remsqsqrt 14283 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
176174, 175syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
177173, 176breqtrd 4834 . . . . . . . . . . . . . 14 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
178145, 30, 111lemuldivd 12118 . . . . . . . . . . . . . 14 (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
179177, 178mpbid 223 . . . . . . . . . . . . 13 (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
180143, 145, 141, 146, 179letrd 10447 . . . . . . . . . . . 12 (𝜑 → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
181180adantr 472 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → e ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
182 reflcl 12804 . . . . . . . . . . . . . 14 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
183 peano2re 10462 . . . . . . . . . . . . . 14 ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
184141, 182, 1833syl 18 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
185184adantr 472 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ∈ ℝ)
186 fllep1 12809 . . . . . . . . . . . . 13 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
187142, 186syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))
188 elfzle1 12550 . . . . . . . . . . . . 13 (𝑛 ∈ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
189128, 188syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1) ≤ 𝑛)
190142, 185, 138, 187, 189letrd 10447 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛)
191140, 142, 138, 181, 190letrd 10447 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ 𝑛)
192140, 138, 132, 191, 137letrd 10447 . . . . . . . . . 10 ((𝜑𝑛𝐼) → e ≤ (𝑍 / 𝑉))
193 logdivle 24658 . . . . . . . . . 10 (((𝑛 ∈ ℝ ∧ e ≤ 𝑛) ∧ ((𝑍 / 𝑉) ∈ ℝ ∧ e ≤ (𝑍 / 𝑉))) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
194138, 191, 132, 192, 193syl22anc 867 . . . . . . . . 9 ((𝜑𝑛𝐼) → (𝑛 ≤ (𝑍 / 𝑉) ↔ ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛)))
195137, 194mpbid 223 . . . . . . . 8 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛))
19647adantr 472 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
197 lemul2 11129 . . . . . . . . 9 ((((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ ∧ ((log‘𝑛) / 𝑛) ∈ ℝ ∧ ((𝑈𝐸) ∈ ℝ ∧ 0 < (𝑈𝐸))) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
198196, 123, 106, 197syl3anc 1490 . . . . . . . 8 ((𝜑𝑛𝐼) → (((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ≤ ((log‘𝑛) / 𝑛) ↔ ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛))))
199195, 198mpbid 223 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20013rpcnd 12071 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
201200adantr 472 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℂ)
202122recnd 10321 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘𝑛) ∈ ℂ)
203121rpcnne0d 12078 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
204 div23 10957 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
205201, 202, 203, 204syl3anc 1490 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = (((𝑈𝐸) / 𝑛) · (log‘𝑛)))
206 divass 10956 . . . . . . . . . 10 (((𝑈𝐸) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
207201, 202, 203, 206syl3anc 1490 . . . . . . . . 9 ((𝜑𝑛𝐼) → (((𝑈𝐸) · (log‘𝑛)) / 𝑛) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
208205, 207eqtr3d 2800 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) = ((𝑈𝐸) · ((log‘𝑛) / 𝑛)))
20943adantr 472 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (𝑈𝐸) ∈ ℝ)
210209, 120nndivred 11325 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ∈ ℝ)
211125, 80syldan 585 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
212 log1 24622 . . . . . . . . . 10 (log‘1) = 0
213120nnge1d 11319 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 1 ≤ 𝑛)
214 logleb 24639 . . . . . . . . . . . 12 ((1 ∈ ℝ+𝑛 ∈ ℝ+) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
215108, 121, 214sylancr 581 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (1 ≤ 𝑛 ↔ (log‘1) ≤ (log‘𝑛)))
216213, 215mpbid 223 . . . . . . . . . 10 ((𝜑𝑛𝐼) → (log‘1) ≤ (log‘𝑛))
217212, 216syl5eqbrr 4844 . . . . . . . . 9 ((𝜑𝑛𝐼) → 0 ≤ (log‘𝑛))
2187rpcnd 12071 . . . . . . . . . . . 12 (𝜑𝑈 ∈ ℂ)
219218adantr 472 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝑈 ∈ ℂ)
22016rpred 12069 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
221220adantr 472 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → 𝐸 ∈ ℝ)
222221recnd 10321 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → 𝐸 ∈ ℂ)
223 divsubdir 10974 . . . . . . . . . . 11 ((𝑈 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
224219, 222, 203, 223syl3anc 1490 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) = ((𝑈 / 𝑛) − (𝐸 / 𝑛)))
225125, 79syldan 585 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
226221, 120nndivred 11325 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝐸 / 𝑛) ∈ ℝ)
227125, 70syldan 585 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (𝑈 / 𝑛) ∈ ℝ)
228125, 76syldan 585 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
229228recnd 10321 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
23029adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ+)
231230rpcnne0d 12078 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
232 divdiv2 10990 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
233229, 231, 203, 232syl3anc 1490 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍))
234121rpcnd 12071 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑛 ∈ ℂ)
235 div23 10957 . . . . . . . . . . . . . . . . 17 (((𝑅‘(𝑍 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
236229, 234, 231, 235syl3anc 1490 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (((𝑅‘(𝑍 / 𝑛)) · 𝑛) / 𝑍) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
237233, 236eqtrd 2798 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)) = (((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛))
238237fveq2d 6378 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)))
239125, 78syldan 585 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
240239, 234absmuld 14479 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (abs‘(((𝑅‘(𝑍 / 𝑛)) / 𝑍) · 𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)))
241121rprege0d 12076 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
242 absid 14322 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) → (abs‘𝑛) = 𝑛)
243241, 242syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (abs‘𝑛) = 𝑛)
244243oveq2d 6857 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (abs‘𝑛)) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
245238, 240, 2443eqtrd 2802 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) = ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛))
246 fveq2 6374 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → (𝑅𝑢) = (𝑅‘(𝑍 / 𝑛)))
247 id 22 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑍 / 𝑛) → 𝑢 = (𝑍 / 𝑛))
248246, 247oveq12d 6859 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑍 / 𝑛) → ((𝑅𝑢) / 𝑢) = ((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛)))
249248fveq2d 6378 . . . . . . . . . . . . . . 15 (𝑢 = (𝑍 / 𝑛) → (abs‘((𝑅𝑢) / 𝑢)) = (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))))
250249breq1d 4818 . . . . . . . . . . . . . 14 (𝑢 = (𝑍 / 𝑛) → ((abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸))
25188simprd 489 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
252251adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸)
25330adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑍 ∈ ℝ)
254253, 120nndivred 11325 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ ℝ)
25544rpregt0d 12075 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
256255adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝐼) → (𝑉 ∈ ℝ ∧ 0 < 𝑉))
257 lemuldiv2 11157 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ (𝑉 ∈ ℝ ∧ 0 < 𝑉)) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
258138, 253, 256, 257syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑛 ≤ (𝑍 / 𝑉)))
259137, 258mpbird 248 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → (𝑉 · 𝑛) ≤ 𝑍)
260256simpld 488 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
261260, 253, 121lemuldivd 12118 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑉 · 𝑛) ≤ 𝑍𝑉 ≤ (𝑍 / 𝑛)))
262259, 261mpbid 223 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → 𝑉 ≤ (𝑍 / 𝑛))
263111rpregt0d 12075 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
264263adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)))
265121rpregt0d 12075 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝐼) → (𝑛 ∈ ℝ ∧ 0 < 𝑛))
266 lediv23 11168 . . . . . . . . . . . . . . . . 17 ((𝑍 ∈ ℝ ∧ (((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ ∧ 0 < ((1 + (𝐿 · 𝐸)) · 𝑉)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
267253, 264, 265, 266syl3anc 1490 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑛 ↔ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉)))
268190, 267mpbid 223 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))
26944rpred 12069 . . . . . . . . . . . . . . . . 17 (𝜑𝑉 ∈ ℝ)
270269adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → 𝑉 ∈ ℝ)
271147adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝐼) → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
272 elicc2 12439 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
273270, 271, 272syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝐼) → ((𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)) ↔ ((𝑍 / 𝑛) ∈ ℝ ∧ 𝑉 ≤ (𝑍 / 𝑛) ∧ (𝑍 / 𝑛) ≤ ((1 + (𝐿 · 𝐸)) · 𝑉))))
274254, 262, 268, 273mpbir3and 1442 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐼) → (𝑍 / 𝑛) ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉)))
275250, 252, 274rspcdva 3466 . . . . . . . . . . . . 13 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / (𝑍 / 𝑛))) ≤ 𝐸)
276245, 275eqbrtrrd 4832 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸)
277225, 221, 121lemuldivd 12118 . . . . . . . . . . . 12 ((𝜑𝑛𝐼) → (((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · 𝑛) ≤ 𝐸 ↔ (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛)))
278276, 277mpbid 223 . . . . . . . . . . 11 ((𝜑𝑛𝐼) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ≤ (𝐸 / 𝑛))
279225, 226, 227, 278lesub2dd 10897 . . . . . . . . . 10 ((𝜑𝑛𝐼) → ((𝑈 / 𝑛) − (𝐸 / 𝑛)) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
280224, 279eqbrtrd 4830 . . . . . . . . 9 ((𝜑𝑛𝐼) → ((𝑈𝐸) / 𝑛) ≤ ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))))
281210, 211, 122, 217, 280lemul1ad 11216 . . . . . . . 8 ((𝜑𝑛𝐼) → (((𝑈𝐸) / 𝑛) · (log‘𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
282208, 281eqbrtrrd 4832 . . . . . . 7 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘𝑛) / 𝑛)) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28399, 124, 126, 199, 282letrd 10447 . . . . . 6 ((𝜑𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
284283adantlr 706 . . . . 5 (((𝜑𝑛𝑂) ∧ 𝑛𝐼) → ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
28569nnred 11290 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ∈ ℝ)
28629, 152rpdivcld 12086 . . . . . . . . . . 11 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ+)
287286rpred 12069 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ∈ ℝ)
288287adantr 472 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ∈ ℝ)
28923simpld 488 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ+)
29029, 289rpdivcld 12086 . . . . . . . . . . 11 (𝜑 → (𝑍 / 𝑌) ∈ ℝ+)
291290rpred 12069 . . . . . . . . . 10 (𝜑 → (𝑍 / 𝑌) ∈ ℝ)
292291adantr 472 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / 𝑌) ∈ ℝ)
293 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑛𝑂) → 𝑛𝑂)
294293, 50syl6eleq 2853 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))))
295 elfzle2 12551 . . . . . . . . . . 11 (𝑛 ∈ (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽)))) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
296294, 295syl 17 . . . . . . . . . 10 ((𝜑𝑛𝑂) → 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽))))
29769nnzd 11727 . . . . . . . . . . 11 ((𝜑𝑛𝑂) → 𝑛 ∈ ℤ)
298 flge 12813 . . . . . . . . . . 11 (((𝑍 / (𝐾𝐽)) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
299288, 297, 298syl2anc 579 . . . . . . . . . 10 ((𝜑𝑛𝑂) → (𝑛 ≤ (𝑍 / (𝐾𝐽)) ↔ 𝑛 ≤ (⌊‘(𝑍 / (𝐾𝐽)))))
300296, 299mpbird 248 . . . . . . . . 9 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / (𝐾𝐽)))
301289rpred 12069 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
30224simpld 488 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ ℝ+)
303302rpred 12069 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ)
304152rpred 12069 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐽) ∈ ℝ)
30524simprd 489 . . . . . . . . . . . . 13 (𝜑𝑌 < 𝑋)
306301, 303, 305ltled 10438 . . . . . . . . . . . 12 (𝜑𝑌𝑋)
307 elfzofz 12692 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (𝑀...𝑁))
30856, 307syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (𝑀...𝑁))
3091, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 25578 . . . . . . . . . . . . . . 15 ((𝜑𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
310308, 309mpdan 678 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))
311310simpld 488 . . . . . . . . . . . . 13 (𝜑𝑋 < (𝐾𝐽))
312303, 304, 311ltled 10438 . . . . . . . . . . . 12 (𝜑𝑋 ≤ (𝐾𝐽))
313301, 303, 304, 306, 312letrd 10447 . . . . . . . . . . 11 (𝜑𝑌 ≤ (𝐾𝐽))
314289, 152, 29lediv2d 12093 . . . . . . . . . . 11 (𝜑 → (𝑌 ≤ (𝐾𝐽) ↔ (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌)))
315313, 314mpbid 223 . . . . . . . . . 10 (𝜑 → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
316315adantr 472 . . . . . . . . 9 ((𝜑𝑛𝑂) → (𝑍 / (𝐾𝐽)) ≤ (𝑍 / 𝑌))
317285, 288, 292, 300, 316letrd 10447 . . . . . . . 8 ((𝜑𝑛𝑂) → 𝑛 ≤ (𝑍 / 𝑌))
31869, 317jca 507 . . . . . . 7 ((𝜑𝑛𝑂) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌)))
3191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 25579 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
320318, 319syldan 585 . . . . . 6 ((𝜑𝑛𝑂) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
321320adantr 472 . . . . 5 (((𝜑𝑛𝑂) ∧ ¬ 𝑛𝐼) → 0 ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
322103, 104, 284, 321ifbothda 4279 . . . 4 ((𝜑𝑛𝑂) → if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32352, 102, 82, 322fsumle 14816 . . 3 (𝜑 → Σ𝑛𝑂 if(𝑛𝐼, ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))), 0) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32498, 323eqbrtrd 4830 . 2 (𝜑 → ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
32536, 49, 83, 89, 324letrd 10447 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2936  wral 3054  wrex 3055  wss 3731  ifcif 4242   class class class wbr 4808  cmpt 4887  cfv 6067  (class class class)co 6841  Fincfn 8159  cc 10186  cr 10187  0cc0 10188  1c1 10189   + caddc 10191   · cmul 10193  +∞cpnf 10324   < clt 10327  cle 10328  cmin 10519   / cdiv 10937  cn 11273  2c2 11326  3c3 11327  4c4 11328  8c8 11332  0cn0 11537  cz 11623  cdc 11739  cuz 11885  +crp 12027  (,)cioo 12376  [,)cico 12378  [,]cicc 12379  ...cfz 12532  ..^cfzo 12672  cfl 12798  cexp 13066  chash 13320  csqrt 14259  abscabs 14260  Σcsu 14702  expce 15075  eceu 15076  logclog 24591  ψcchp 25109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-fi 8523  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-q 11989  df-rp 12028  df-xneg 12145  df-xadd 12146  df-xmul 12147  df-ioo 12380  df-ioc 12381  df-ico 12382  df-icc 12383  df-fz 12533  df-fzo 12673  df-fl 12800  df-mod 12876  df-seq 13008  df-exp 13067  df-fac 13264  df-bc 13293  df-hash 13321  df-shft 14093  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-limsup 14488  df-clim 14505  df-rlim 14506  df-sum 14703  df-ef 15081  df-e 15082  df-sin 15083  df-cos 15084  df-pi 15086  df-dvds 15267  df-gcd 15499  df-prm 15667  df-pc 15822  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-rest 16350  df-topn 16351  df-0g 16369  df-gsum 16370  df-topgen 16371  df-pt 16372  df-prds 16375  df-xrs 16429  df-qtop 16434  df-imas 16435  df-xps 16437  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-mulg 17809  df-cntz 18014  df-cmn 18460  df-psmet 20010  df-xmet 20011  df-met 20012  df-bl 20013  df-mopn 20014  df-fbas 20015  df-fg 20016  df-cnfld 20019  df-top 20977  df-topon 20994  df-topsp 21016  df-bases 21029  df-cld 21102  df-ntr 21103  df-cls 21104  df-nei 21181  df-lp 21219  df-perf 21220  df-cn 21310  df-cnp 21311  df-haus 21398  df-tx 21644  df-hmeo 21837  df-fil 21928  df-fm 22020  df-flim 22021  df-flf 22022  df-xms 22403  df-ms 22404  df-tms 22405  df-cncf 22959  df-limc 23920  df-dv 23921  df-log 24593  df-vma 25114  df-chp 25115
This theorem is referenced by:  pntlemi  25583
  Copyright terms: Public domain W3C validator