Step | Hyp | Ref
| Expression |
1 | | oveq2 7151 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → (𝐵 / 𝑒) = (𝐵 / 𝐸)) |
2 | 1 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (exp‘(𝐵 / 𝑒)) = (exp‘(𝐵 / 𝐸))) |
3 | | pntlemp.k |
. . . . . . . 8
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) |
4 | 2, 3 | eqtr4di 2812 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → (exp‘(𝐵 / 𝑒)) = 𝐾) |
5 | 4 | oveq1d 7158 |
. . . . . 6
⊢ (𝑒 = 𝐸 → ((exp‘(𝐵 / 𝑒))[,)+∞) = (𝐾[,)+∞)) |
6 | | oveq2 7151 |
. . . . . . . . . . . . 13
⊢ (𝑒 = 𝐸 → (𝐿 · 𝑒) = (𝐿 · 𝐸)) |
7 | 6 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝐸 → (1 + (𝐿 · 𝑒)) = (1 + (𝐿 · 𝐸))) |
8 | 7 | oveq1d 7158 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → ((1 + (𝐿 · 𝑒)) · 𝑧) = ((1 + (𝐿 · 𝐸)) · 𝑧)) |
9 | 8 | breq1d 5035 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦) ↔ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦))) |
10 | 9 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ↔ (𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)))) |
11 | 8 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧)) = (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))) |
12 | | breq2 5029 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → ((abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒 ↔ (abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
13 | 11, 12 | raleqbidv 3317 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → (∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒 ↔ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
14 | 10, 13 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
15 | 14 | rexbidv 3219 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → (∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
16 | 15 | ralbidv 3124 |
. . . . . 6
⊢ (𝑒 = 𝐸 → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
17 | 5, 16 | raleqbidv 3317 |
. . . . 5
⊢ (𝑒 = 𝐸 → (∀𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
18 | 17 | rexbidv 3219 |
. . . 4
⊢ (𝑒 = 𝐸 → (∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
19 | | oveq1 7150 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → (𝑥(,)+∞) = (𝑡(,)+∞)) |
20 | 19 | raleqdv 3327 |
. . . . . 6
⊢ (𝑥 = 𝑡 → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
21 | 20 | ralbidv 3124 |
. . . . 5
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
22 | 21 | cbvrexvw 3360 |
. . . 4
⊢
(∃𝑥 ∈
ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∃𝑡 ∈ ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
23 | 18, 22 | bitrdi 290 |
. . 3
⊢ (𝑒 = 𝐸 → (∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∃𝑡 ∈ ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
24 | | pntlemp.K |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
25 | | pntlem3.r |
. . . . . 6
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
26 | | pntlem3.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
27 | | pntlemp.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
28 | | pntlemp.l |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
29 | | pntlemp.d |
. . . . . 6
⊢ 𝐷 = (𝐴 + 1) |
30 | | pntlemp.f |
. . . . . 6
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) |
31 | | pntlemp.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
32 | | pntlemp.u2 |
. . . . . 6
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
33 | | pntlemp.e |
. . . . . 6
⊢ 𝐸 = (𝑈 / 𝐷) |
34 | 25, 26, 27, 28, 29, 30, 31, 32, 33, 3 | pntlemc 26263 |
. . . . 5
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) |
35 | 34 | simp3d 1142 |
. . . 4
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) |
36 | 35 | simp1d 1140 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
37 | 23, 24, 36 | rspcdva 3541 |
. 2
⊢ (𝜑 → ∃𝑡 ∈ ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
38 | | pntlemp.y |
. . . . 5
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
39 | 38 | simpld 499 |
. . . 4
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
40 | 39 | rpred 12457 |
. . 3
⊢ (𝜑 → 𝑌 ∈ ℝ) |
41 | 38 | simprd 500 |
. . 3
⊢ (𝜑 → 1 ≤ 𝑌) |
42 | 25 | pntrlog2bnd 26252 |
. . 3
⊢ ((𝑌 ∈ ℝ ∧ 1 ≤
𝑌) → ∃𝑐 ∈ ℝ+
∀𝑧 ∈
(1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) |
43 | 40, 41, 42 | syl2anc 588 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑧 ∈
(1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) |
44 | | reeanv 3283 |
. . 3
⊢
(∃𝑡 ∈
ℝ+ ∃𝑐 ∈ ℝ+ (∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) ↔ (∃𝑡 ∈ ℝ+ ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∃𝑐 ∈ ℝ+ ∀𝑧 ∈
(1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐)) |
45 | 26 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝐴 ∈
ℝ+) |
46 | 27 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝐵 ∈
ℝ+) |
47 | 28 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝐿 ∈ (0(,)1)) |
48 | 31 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝑈 ∈
ℝ+) |
49 | 32 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝑈 ≤ 𝐴) |
50 | 38 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
51 | | simpl 487 |
. . . . . . . . 9
⊢ ((𝑡 ∈ ℝ+
∧ 𝑐 ∈
ℝ+) → 𝑡 ∈ ℝ+) |
52 | | rpaddcl 12437 |
. . . . . . . . 9
⊢ ((𝑌 ∈ ℝ+
∧ 𝑡 ∈
ℝ+) → (𝑌 + 𝑡) ∈
ℝ+) |
53 | 39, 51, 52 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ (𝑌 + 𝑡) ∈
ℝ+) |
54 | | ltaddrp 12452 |
. . . . . . . . 9
⊢ ((𝑌 ∈ ℝ ∧ 𝑡 ∈ ℝ+)
→ 𝑌 < (𝑌 + 𝑡)) |
55 | 40, 51, 54 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑌 < (𝑌 + 𝑡)) |
56 | 53, 55 | jca 516 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ ((𝑌 + 𝑡) ∈ ℝ+
∧ 𝑌 < (𝑌 + 𝑡))) |
57 | 56 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ((𝑌 + 𝑡) ∈ ℝ+ ∧ 𝑌 < (𝑌 + 𝑡))) |
58 | | simprlr 780 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → 𝑐 ∈ ℝ+) |
59 | | eqid 2759 |
. . . . . 6
⊢ (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + ((((𝑌 + 𝑡) · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝑐))))) = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + ((((𝑌 + 𝑡) · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝑐))))) |
60 | | pntlemp.U |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) |
61 | 60 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) |
62 | | rpxr 12424 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ+
→ 𝑡 ∈
ℝ*) |
63 | 62 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑡 ∈
ℝ*) |
64 | | rpre 12423 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℝ+
→ 𝑡 ∈
ℝ) |
65 | 64 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑡 ∈
ℝ) |
66 | 53 | rpred 12457 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ (𝑌 + 𝑡) ∈
ℝ) |
67 | 39 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑌 ∈
ℝ+) |
68 | 65, 67 | ltaddrp2d 12491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑡 < (𝑌 + 𝑡)) |
69 | 65, 66, 68 | ltled 10811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ 𝑡 ≤ (𝑌 + 𝑡)) |
70 | | iooss1 12799 |
. . . . . . . . 9
⊢ ((𝑡 ∈ ℝ*
∧ 𝑡 ≤ (𝑌 + 𝑡)) → ((𝑌 + 𝑡)(,)+∞) ⊆ (𝑡(,)+∞)) |
71 | 63, 69, 70 | syl2anc 588 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ ((𝑌 + 𝑡)(,)+∞) ⊆ (𝑡(,)+∞)) |
72 | 71 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ((𝑌 + 𝑡)(,)+∞) ⊆ (𝑡(,)+∞)) |
73 | | simprrl 781 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
74 | | ssralv 3954 |
. . . . . . . 8
⊢ (((𝑌 + 𝑡)(,)+∞) ⊆ (𝑡(,)+∞) → (∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) → ∀𝑦 ∈ ((𝑌 + 𝑡)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
75 | 74 | ralimdv 3107 |
. . . . . . 7
⊢ (((𝑌 + 𝑡)(,)+∞) ⊆ (𝑡(,)+∞) → (∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) → ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ ((𝑌 + 𝑡)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
76 | 72, 73, 75 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ ((𝑌 + 𝑡)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
77 | | simprrr 782 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) |
78 | 25, 45, 46, 47, 29, 30, 48, 49, 33, 3, 50, 57, 58, 59, 61, 76, 77 | pntleme 26276 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+)
∧ (∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐))) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅‘𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3)))) |
79 | 78 | expr 461 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+))
→ ((∀𝑘 ∈
(𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅‘𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))) |
80 | 79 | rexlimdvva 3216 |
. . 3
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∃𝑐 ∈ ℝ+
(∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅‘𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))) |
81 | 44, 80 | syl5bir 246 |
. 2
⊢ (𝜑 → ((∃𝑡 ∈ ℝ+
∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑡(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ∧ ∃𝑐 ∈ ℝ+ ∀𝑧 ∈
(1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑛 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))) / 𝑧) ≤ 𝑐) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅‘𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))) |
82 | 37, 43, 81 | mp2and 699 |
1
⊢ (𝜑 → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅‘𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3)))) |