Theorem pntlemi 27567

Description: Lemma for pnt 27577. Eliminate some assumptions from pntlemj 27566. (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)...(⌊‘(𝑍 / (𝐾↑𝐽))))

Assertion

Ref	Expression
pntlemi	⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))

Distinct variable groups:   𝑧,𝐶   𝑦,𝑛,𝑧,𝐽   𝑢,𝑛,𝐿,𝑦,𝑧   𝑛,𝐾,𝑦,𝑧   𝑛,𝑀,𝑧   𝑛,𝑂,𝑧   𝜑,𝑛   𝑛,𝑁,𝑧   𝑅,𝑛,𝑢,𝑦,𝑧   𝑈,𝑛,𝑧   𝑛,𝑊,𝑧   𝑛,𝑋,𝑦,𝑧   𝑛,𝑌,𝑧   𝑛,𝑎,𝑢,𝑦,𝑧,𝐸   𝑛,𝑍,𝑢,𝑧

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑢,𝑎)   𝐴(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐵(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐶(𝑦,𝑢,𝑛,𝑎)   𝐷(𝑦,𝑧,𝑢,𝑛,𝑎)   𝑅(𝑎)   𝑈(𝑦,𝑢,𝑎)   𝐹(𝑦,𝑧,𝑢,𝑛,𝑎)   𝐽(𝑢,𝑎)   𝐾(𝑢,𝑎)   𝐿(𝑎)   𝑀(𝑦,𝑢,𝑎)   𝑁(𝑦,𝑢,𝑎)   𝑂(𝑦,𝑢,𝑎)   𝑊(𝑦,𝑢,𝑎)   𝑋(𝑢,𝑎)   𝑌(𝑦,𝑢,𝑎)   𝑍(𝑦,𝑎)

Proof of Theorem pntlemi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5089	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑥))
2		oveq2 7375	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((1 + (𝐿 · 𝐸)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑥))
3	2	breq1d 5095	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦) ↔ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)))
4	1, 3	anbi12d 633	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ↔ (𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦))))
5		id 22	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
6	5, 2	oveq12d 7385	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧)) = (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥)))
7	6	raleqdv 3295	. . . . . 6 ⊢ (𝑧 = 𝑥 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸 ↔ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
8	4, 7	anbi12d 633	. . . . 5 ⊢ (𝑧 = 𝑥 → (((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ((𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)))
9	8	cbvrexvw 3216	. . . 4 ⊢ (∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∃𝑥 ∈ ℝ+ ((𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
10		breq1 5088	. . . . . . 7 ⊢ (𝑦 = (𝐾↑𝐽) → (𝑦 < 𝑥 ↔ (𝐾↑𝐽) < 𝑥))
11		oveq2 7375	. . . . . . . 8 ⊢ (𝑦 = (𝐾↑𝐽) → (𝐾 · 𝑦) = (𝐾 · (𝐾↑𝐽)))
12	11	breq2d 5097	. . . . . . 7 ⊢ (𝑦 = (𝐾↑𝐽) → (((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦) ↔ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))))
13	10, 12	anbi12d 633	. . . . . 6 ⊢ (𝑦 = (𝐾↑𝐽) → ((𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)) ↔ ((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽)))))
14	13	anbi1d 632	. . . . 5 ⊢ (𝑦 = (𝐾↑𝐽) → (((𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)))
15	14	rexbidv 3161	. . . 4 ⊢ (𝑦 = (𝐾↑𝐽) → (∃𝑥 ∈ ℝ+ ((𝑦 < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∃𝑥 ∈ ℝ+ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)))
16	9, 15	bitrid 283	. . 3 ⊢ (𝑦 = (𝐾↑𝐽) → (∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∃𝑥 ∈ ℝ+ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)))
17		pntlem1.K	. . . 4 ⊢ (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
18	17	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
19		pntlem1.r	. . . . . . . 8 ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
20		pntlem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
21		pntlem1.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
22		pntlem1.l	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ (0(,)1))
23		pntlem1.d	. . . . . . . 8 ⊢ 𝐷 = (𝐴 + 1)
24		pntlem1.f	. . . . . . . 8 ⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)))
25		pntlem1.u	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ ℝ+)
26		pntlem1.u2	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ≤ 𝐴)
27		pntlem1.e	. . . . . . . 8 ⊢ 𝐸 = (𝑈 / 𝐷)
28		pntlem1.k	. . . . . . . 8 ⊢ 𝐾 = (exp‘(𝐵 / 𝐸))
29	19, 20, 21, 22, 23, 24, 25, 26, 27, 28	pntlemc 27558	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ+)))
30	29	simp2d 1144	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
31		elfzoelz 13613	. . . . . 6 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
32		rpexpcl 14042	. . . . . 6 ⊢ ((𝐾 ∈ ℝ+ ∧ 𝐽 ∈ ℤ) → (𝐾↑𝐽) ∈ ℝ+)
33	30, 31, 32	syl2an 597	. . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → (𝐾↑𝐽) ∈ ℝ+)
34	33	rpred 12986	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → (𝐾↑𝐽) ∈ ℝ)
35		elfzofz 13630	. . . . . 6 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (𝑀...𝑁))
36		pntlem1.y	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
37		pntlem1.x	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋))
38		pntlem1.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ+)
39		pntlem1.w	. . . . . . 7 ⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))
40		pntlem1.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞))
41		pntlem1.m	. . . . . . 7 ⊢ 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
42		pntlem1.n	. . . . . . 7 ⊢ 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
43	19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 36, 37, 38, 39, 40, 41, 42	pntlemh 27562	. . . . . 6 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍)))
44	35, 43	sylan2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍)))
45	44	simpld 494	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → 𝑋 < (𝐾↑𝐽))
46	37	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ+)
47	46	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ+)
48		rpxr 12952	. . . . 5 ⊢ (𝑋 ∈ ℝ+ → 𝑋 ∈ ℝ*)
49		elioopnf 13396	. . . . 5 ⊢ (𝑋 ∈ ℝ* → ((𝐾↑𝐽) ∈ (𝑋(,)+∞) ↔ ((𝐾↑𝐽) ∈ ℝ ∧ 𝑋 < (𝐾↑𝐽))))
50	47, 48, 49	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → ((𝐾↑𝐽) ∈ (𝑋(,)+∞) ↔ ((𝐾↑𝐽) ∈ ℝ ∧ 𝑋 < (𝐾↑𝐽))))
51	34, 45, 50	mpbir2and 714	. . 3 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → (𝐾↑𝐽) ∈ (𝑋(,)+∞))
52	16, 18, 51	rspcdva 3565	. 2 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → ∃𝑥 ∈ ℝ+ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
53	20	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝐴 ∈ ℝ+)
54	21	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝐵 ∈ ℝ+)
55	22	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝐿 ∈ (0(,)1))
56	25	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝑈 ∈ ℝ+)
57	26	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝑈 ≤ 𝐴)
58	36	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
59	37	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋))
60	38	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝐶 ∈ ℝ+)
61	40	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝑍 ∈ (𝑊[,)+∞))
62		pntlem1.U	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈)
63	62	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈)
64	17	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
65		pntlem1.o	. . 3 ⊢ 𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾↑𝐽))))
66		simprl 771	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝑥 ∈ ℝ+)
67		simprr 773	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
68		simplr 769	. . 3 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → 𝐽 ∈ (𝑀..^𝑁))
69		eqid 2736	. . 3 ⊢ (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑥))) + 1)...(⌊‘(𝑍 / 𝑥))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑥))) + 1)...(⌊‘(𝑍 / 𝑥)))
70	19, 53, 54, 55, 23, 24, 56, 57, 27, 28, 58, 59, 60, 39, 61, 41, 42, 63, 64, 65, 66, 67, 68, 69	pntlemj 27566	. 2 ⊢ (((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ ℝ+ ∧ (((𝐾↑𝐽) < 𝑥 ∧ ((1 + (𝐿 · 𝐸)) · 𝑥) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑥[,]((1 + (𝐿 · 𝐸)) · 𝑥))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
71	52, 70	rexlimddv 3144	1 ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀..^𝑁)) → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛 ∈ 𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061   class class class wbr 5085   ↦ cmpt 5166  ‘cfv 6498  (class class class)co 7367  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  +∞cpnf 11176  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180   − cmin 11377   / cdiv 11807  2c2 12236  3c3 12237  4c4 12238  8c8 12242  ℤcz 12524  ;cdc 12644  ℝ⁺crp 12942  (,)cioo 13298  [,)cico 13300  [,]cicc 13301  ...cfz 13461  ..^cfzo 13608  ⌊cfl 13749  ↑cexp 14023  √csqrt 15195  abscabs 15196  Σcsu 15648  expce 16026  logclog 26518  ψcchp 27056

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-oadd 8409  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-fi 9324  df-sup 9355  df-inf 9356  df-oi 9425  df-dju 9825  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ioc 13303  df-ico 13304  df-icc 13305  df-fz 13462  df-fzo 13609  df-fl 13751  df-mod 13829  df-seq 13964  df-exp 14024  df-fac 14236  df-bc 14265  df-hash 14293  df-shft 15029  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-limsup 15433  df-clim 15450  df-rlim 15451  df-sum 15649  df-ef 16032  df-e 16033  df-sin 16034  df-cos 16035  df-pi 16037  df-dvds 16222  df-gcd 16464  df-prm 16641  df-pc 16808  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-rest 17385  df-topn 17386  df-0g 17404  df-gsum 17405  df-topgen 17406  df-pt 17407  df-prds 17410  df-xrs 17466  df-qtop 17471  df-imas 17472  df-xps 17474  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-submnd 18752  df-mulg 19044  df-cntz 19292  df-cmn 19757  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-fbas 21349  df-fg 21350  df-cnfld 21353  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-perf 23102  df-cn 23192  df-cnp 23193  df-haus 23280  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-xms 24285  df-ms 24286  df-tms 24287  df-cncf 24845  df-limc 25833  df-dv 25834  df-log 26520  df-vma 27061  df-chp 27062

This theorem is referenced by:  pntlemf  27568