| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2re 12341 | . . 3
⊢ 2 ∈
ℝ | 
| 2 |  | 1le2 12476 | . . 3
⊢ 1 ≤
2 | 
| 3 |  | chpdifbnd 27600 | . . 3
⊢ ((2
∈ ℝ ∧ 1 ≤ 2) → ∃𝑡 ∈ ℝ+ ∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣))))) | 
| 4 | 1, 2, 3 | mp2an 692 | . 2
⊢
∃𝑡 ∈
ℝ+ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))) | 
| 5 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 ∈
ℝ+) | 
| 6 |  | ioossre 13449 | . . . . . . . . . . . . 13
⊢ (0(,)1)
⊆ ℝ | 
| 7 |  | pntibndlem3.4 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) | 
| 8 | 6, 7 | sselid 3980 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 9 |  | eliooord 13447 | . . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) | 
| 10 | 7, 9 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) | 
| 11 | 10 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐸) | 
| 12 | 8, 11 | elrpd 13075 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 13 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ∈
ℝ+) | 
| 14 |  | 4nn 12350 | . . . . . . . . . . 11
⊢ 4 ∈
ℕ | 
| 15 |  | nnrp 13047 | . . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . . . . . 10
⊢ 4 ∈
ℝ+ | 
| 17 |  | rpdivcl 13061 | . . . . . . . . . 10
⊢ ((𝐸 ∈ ℝ+
∧ 4 ∈ ℝ+) → (𝐸 / 4) ∈
ℝ+) | 
| 18 | 13, 16, 17 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 / 4) ∈
ℝ+) | 
| 19 | 5, 18 | rpdivcld 13095 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈
ℝ+) | 
| 20 | 19 | rpred 13078 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈ ℝ) | 
| 21 | 20 | rpefcld 16142 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝑡 / (𝐸 / 4))) ∈
ℝ+) | 
| 22 |  | pntibndlem3.6 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 23 | 22 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 ∈
ℝ+) | 
| 24 | 21, 23 | rpaddcld 13093 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈
ℝ+) | 
| 25 | 24 | adantrr 717 | . . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈
ℝ+) | 
| 26 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑛 → (𝑣 < 𝑖 ↔ 𝑣 < 𝑛)) | 
| 27 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑛 → (𝑖 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑣))) | 
| 28 | 26, 27 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑖 = 𝑛 → ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)))) | 
| 29 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (𝑅‘𝑖) = (𝑅‘𝑛)) | 
| 30 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → 𝑖 = 𝑛) | 
| 31 | 29, 30 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → ((𝑅‘𝑖) / 𝑖) = ((𝑅‘𝑛) / 𝑛)) | 
| 32 | 31 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑛 → (abs‘((𝑅‘𝑖) / 𝑖)) = (abs‘((𝑅‘𝑛) / 𝑛))) | 
| 33 | 32 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑖 = 𝑛 → ((abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2) ↔ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) | 
| 34 | 28, 33 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑖 = 𝑛 → (((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) | 
| 35 | 34 | cbvrexvw 3237 | . . . . . . . 8
⊢
(∃𝑖 ∈
ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) | 
| 36 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑣 = 𝑦 → (𝑣 < 𝑛 ↔ 𝑦 < 𝑛)) | 
| 37 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑣 = 𝑦 → ((𝑘 / 2) · 𝑣) = ((𝑘 / 2) · 𝑦)) | 
| 38 | 37 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑣 = 𝑦 → (𝑛 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑦))) | 
| 39 | 36, 38 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑣 = 𝑦 → ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)))) | 
| 40 | 39 | anbi1d 631 | . . . . . . . . 9
⊢ (𝑣 = 𝑦 → (((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) | 
| 41 | 40 | rexbidv 3178 | . . . . . . . 8
⊢ (𝑣 = 𝑦 → (∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) | 
| 42 | 35, 41 | bitrid 283 | . . . . . . 7
⊢ (𝑣 = 𝑦 → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) | 
| 43 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 / 2) → (𝑚 · 𝑣) = ((𝑘 / 2) · 𝑣)) | 
| 44 | 43 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 / 2) → (𝑖 ≤ (𝑚 · 𝑣) ↔ 𝑖 ≤ ((𝑘 / 2) · 𝑣))) | 
| 45 | 44 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑘 / 2) → ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ↔ (𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)))) | 
| 46 | 45 | anbi1d 631 | . . . . . . . . . 10
⊢ (𝑚 = (𝑘 / 2) → (((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) | 
| 47 | 46 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑚 = (𝑘 / 2) → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) | 
| 48 | 47 | ralbidv 3177 | . . . . . . . 8
⊢ (𝑚 = (𝑘 / 2) → (∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) | 
| 49 |  | pntibndlem3.5 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) | 
| 50 | 49 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) | 
| 51 |  | pntibndlem3.c | . . . . . . . . . . . . . . . . 17
⊢ 𝐶 = ((2 · 𝐵) +
(log‘2)) | 
| 52 |  | pntibndlem3.3 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℝ+) | 
| 54 | 53 | rpred 13078 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℝ) | 
| 55 |  | remulcl 11241 | . . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) | 
| 56 | 1, 54, 55 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) ∈
ℝ) | 
| 57 |  | 2rp 13040 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ | 
| 58 |  | relogcl 26618 | . . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) | 
| 59 | 57, 58 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢
(log‘2) ∈ ℝ | 
| 60 |  | readdcl 11239 | . . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝐵) ∈ ℝ
∧ (log‘2) ∈ ℝ) → ((2 · 𝐵) + (log‘2)) ∈
ℝ) | 
| 61 | 56, 59, 60 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) +
(log‘2)) ∈ ℝ) | 
| 62 | 51, 61 | eqeltrid 2844 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐶 ∈
ℝ) | 
| 63 | 62, 13 | rerpdivcld 13109 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) ∈ ℝ) | 
| 64 | 63 | reefcld 16125 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝐶 / 𝐸)) ∈
ℝ) | 
| 65 |  | elicopnf 13486 | . . . . . . . . . . . . . 14
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝑘 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝑘))) | 
| 66 | 64, 65 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝑘))) | 
| 67 | 66 | simprbda 498 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝑘 ∈ ℝ) | 
| 68 | 67 | rehalfcld 12515 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ ℝ) | 
| 69 |  | pntibndlem3.k | . . . . . . . . . . . 12
⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2))) | 
| 70 | 13 | rphalfcld 13090 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 / 2) ∈
ℝ+) | 
| 71 | 54, 70 | rerpdivcld 13109 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℝ) | 
| 72 | 71 | reefcld 16125 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝐵 / (𝐸 / 2))) ∈
ℝ) | 
| 73 |  | remulcl 11241 | . . . . . . . . . . . . . . . 16
⊢
(((exp‘(𝐵 /
(𝐸 / 2))) ∈ ℝ
∧ 2 ∈ ℝ) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) | 
| 74 | 72, 1, 73 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) | 
| 76 | 64 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ∈ ℝ) | 
| 77 | 71 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℂ) | 
| 78 | 59 | recni 11276 | . . . . . . . . . . . . . . . . . 18
⊢
(log‘2) ∈ ℂ | 
| 79 |  | efadd 16131 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 / (𝐸 / 2)) ∈ ℂ ∧ (log‘2)
∈ ℂ) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
(exp‘(log‘2)))) | 
| 80 | 77, 78, 79 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
(exp‘(log‘2)))) | 
| 81 |  | reeflog 26623 | . . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℝ+ → (exp‘(log‘2)) = 2) | 
| 82 | 57, 81 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢
(exp‘(log‘2)) = 2 | 
| 83 | 82 | oveq2i 7443 | . . . . . . . . . . . . . . . . 17
⊢
((exp‘(𝐵 /
(𝐸 / 2))) ·
(exp‘(log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · 2) | 
| 84 | 80, 83 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
2)) | 
| 85 | 59 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ∈ ℝ) | 
| 86 |  | rerpdivcl 13066 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((log‘2) ∈ ℝ ∧ 𝐸 ∈ ℝ+) →
((log‘2) / 𝐸) ∈
ℝ) | 
| 87 | 59, 13, 86 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) / 𝐸) ∈
ℝ) | 
| 88 | 78 | div1i 11996 | . . . . . . . . . . . . . . . . . . . 20
⊢
((log‘2) / 1) = (log‘2) | 
| 89 | 10 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 < 1) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 < 1) | 
| 91 | 8 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ∈
ℝ) | 
| 92 |  | 1re 11262 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ | 
| 93 |  | ltle 11350 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐸 < 1
→ 𝐸 ≤
1)) | 
| 94 | 91, 92, 93 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 < 1 → 𝐸 ≤ 1)) | 
| 95 | 90, 94 | mpd 15 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ≤ 1) | 
| 96 | 13 | rpregt0d 13084 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ∈ ℝ ∧ 0 <
𝐸)) | 
| 97 |  | 1rp 13039 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ | 
| 98 |  | rpregt0 13050 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℝ+ → (1 ∈ ℝ ∧ 0 < 1)) | 
| 99 | 97, 98 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 ∈
ℝ ∧ 0 < 1)) | 
| 100 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 <
2 | 
| 101 |  | rplogcl 26647 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℝ ∧ 1 < 2) → (log‘2) ∈
ℝ+) | 
| 102 | 1, 100, 101 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(log‘2) ∈ ℝ+ | 
| 103 |  | rpregt0 13050 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((log‘2) ∈ ℝ+ → ((log‘2) ∈
ℝ ∧ 0 < (log‘2))) | 
| 104 | 102, 103 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) | 
| 105 |  | lediv2 12159 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐸 ∈ ℝ ∧ 0 <
𝐸) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ ((log‘2) ∈ ℝ ∧ 0 <
(log‘2))) → (𝐸
≤ 1 ↔ ((log‘2) / 1) ≤ ((log‘2) / 𝐸))) | 
| 106 | 96, 99, 104, 105 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ≤ 1 ↔ ((log‘2) /
1) ≤ ((log‘2) / 𝐸))) | 
| 107 | 95, 106 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) / 1) ≤ ((log‘2) / 𝐸)) | 
| 108 | 88, 107 | eqbrtrrid 5178 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ≤ ((log‘2) / 𝐸)) | 
| 109 | 85, 87, 71, 108 | leadd2dd 11879 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) | 
| 110 | 51 | oveq1i 7442 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐶 / 𝐸) = (((2 · 𝐵) + (log‘2)) / 𝐸) | 
| 111 | 56 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) ∈
ℂ) | 
| 112 | 78 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ∈ ℂ) | 
| 113 |  | rpcnne0 13054 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸 ∈ ℝ+
→ (𝐸 ∈ ℂ
∧ 𝐸 ≠
0)) | 
| 114 | 13, 113 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) | 
| 115 |  | divdir 11948 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝐵) ∈ ℂ
∧ (log‘2) ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → (((2 · 𝐵) + (log‘2)) / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸))) | 
| 116 | 111, 112,
114, 115 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((2
· 𝐵) +
(log‘2)) / 𝐸) = (((2
· 𝐵) / 𝐸) + ((log‘2) / 𝐸))) | 
| 117 | 110, 116 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸))) | 
| 118 | 1 | recni 11276 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℂ | 
| 119 | 54 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℂ) | 
| 120 |  | mulcom 11242 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℂ) → (2 · 𝐵) = (𝐵 · 2)) | 
| 121 | 118, 119,
120 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) = (𝐵 · 2)) | 
| 122 | 121 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) / 𝐸) = ((𝐵 · 2) / 𝐸)) | 
| 123 |  | rpcnne0 13054 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) | 
| 124 | 57, 123 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2 ∈
ℂ ∧ 2 ≠ 0)) | 
| 125 |  | divdiv2 11980 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (𝐵
/ (𝐸 / 2)) = ((𝐵 · 2) / 𝐸)) | 
| 126 | 119, 114,
124, 125 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) = ((𝐵 · 2) / 𝐸)) | 
| 127 | 122, 126 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) / 𝐸) = (𝐵 / (𝐸 / 2))) | 
| 128 | 127 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((2
· 𝐵) / 𝐸) + ((log‘2) / 𝐸)) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) | 
| 129 | 117, 128 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) | 
| 130 | 109, 129 | breqtrrd 5170 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸)) | 
| 131 |  | readdcl 11239 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 / (𝐸 / 2)) ∈ ℝ ∧ (log‘2)
∈ ℝ) → ((𝐵
/ (𝐸 / 2)) + (log‘2))
∈ ℝ) | 
| 132 | 71, 59, 131 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ∈
ℝ) | 
| 133 |  | efle 16155 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 / (𝐸 / 2)) + (log‘2)) ∈ ℝ ∧
(𝐶 / 𝐸) ∈ ℝ) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸)))) | 
| 134 | 132, 63, 133 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸)))) | 
| 135 | 130, 134 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸))) | 
| 136 | 84, 135 | eqbrtrrd 5166 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤
(exp‘(𝐶 / 𝐸))) | 
| 137 | 136 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ (exp‘(𝐶 / 𝐸))) | 
| 138 | 66 | simplbda 499 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ≤ 𝑘) | 
| 139 | 75, 76, 67, 137, 138 | letrd 11419 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘) | 
| 140 | 72 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ) | 
| 141 |  | rpregt0 13050 | . . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ+ → (2 ∈ ℝ ∧ 0 < 2)) | 
| 142 | 57, 141 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (2 ∈ ℝ
∧ 0 < 2)) | 
| 143 |  | lemuldiv 12149 | . . . . . . . . . . . . . 14
⊢
(((exp‘(𝐵 /
(𝐸 / 2))) ∈ ℝ
∧ 𝑘 ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2))) | 
| 144 | 140, 67, 142, 143 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2))) | 
| 145 | 139, 144 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2)) | 
| 146 | 69, 145 | eqbrtrid 5177 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ≤ (𝑘 / 2)) | 
| 147 | 69, 140 | eqeltrid 2844 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ∈ ℝ) | 
| 148 |  | elicopnf 13486 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ ℝ → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2)))) | 
| 149 | 147, 148 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2)))) | 
| 150 | 68, 146, 149 | mpbir2and 713 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ (𝐾[,)+∞)) | 
| 151 | 150 | adantrr 717 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞)) | 
| 152 | 151 | adantlrr 721 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞)) | 
| 153 | 48, 50, 152 | rspcdva 3622 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) | 
| 154 |  | elioore 13418 | . . . . . . . . . 10
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → 𝑦 ∈ ℝ) | 
| 155 | 154 | ad2antll 729 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ ℝ) | 
| 156 | 23 | rpred 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 ∈
ℝ) | 
| 157 | 156 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈ ℝ) | 
| 158 | 20 | reefcld 16125 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝑡 / (𝐸 / 4))) ∈
ℝ) | 
| 159 | 158, 156 | readdcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ) | 
| 160 | 159 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ) | 
| 161 | 156, 21 | ltaddrp2d 13112 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)) | 
| 162 | 161 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)) | 
| 163 |  | eliooord 13447 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦 ∧ 𝑦 < +∞)) | 
| 164 | 163 | simpld 494 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦) | 
| 165 | 164 | ad2antll 729 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦) | 
| 166 | 157, 160,
155, 162, 165 | lttrd 11423 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < 𝑦) | 
| 167 | 157 | rexrd 11312 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈
ℝ*) | 
| 168 |  | elioopnf 13484 | . . . . . . . . . 10
⊢ (𝑍 ∈ ℝ*
→ (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦))) | 
| 169 | 167, 168 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦))) | 
| 170 | 155, 166,
169 | mpbir2and 713 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞)) | 
| 171 | 170 | adantlrr 721 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞)) | 
| 172 | 42, 153, 171 | rspcdva 3622 | . . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) | 
| 173 |  | pntibnd.r | . . . . . . . 8
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 174 |  | pntibndlem1.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 175 | 174 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐴 ∈
ℝ+) | 
| 176 |  | pntibndlem1.l | . . . . . . . 8
⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) | 
| 177 |  | pntibndlem3.2 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) | 
| 178 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝑅‘𝑥) = (𝑅‘𝑣)) | 
| 179 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → 𝑥 = 𝑣) | 
| 180 | 178, 179 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑣) / 𝑣)) | 
| 181 | 180 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑣) / 𝑣))) | 
| 182 | 181 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴)) | 
| 183 | 182 | cbvralvw 3236 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) | 
| 184 | 177, 183 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) | 
| 185 | 184 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) | 
| 186 | 52 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐵 ∈
ℝ+) | 
| 187 | 7 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐸 ∈ (0(,)1)) | 
| 188 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑍 ∈
ℝ+) | 
| 189 |  | simprrl 780 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑛 ∈ ℕ) | 
| 190 |  | simplrl 776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑡 ∈ ℝ+) | 
| 191 |  | simplrr 777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣))))) | 
| 192 |  | eqid 2736 | . . . . . . . 8
⊢
((exp‘(𝑡 /
(𝐸 / 4))) + 𝑍) = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) | 
| 193 |  | simprll 778 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) | 
| 194 |  | simprlr 779 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) | 
| 195 |  | simprrr 781 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) | 
| 196 | 173, 175,
176, 185, 186, 69, 51, 187, 188, 189, 190, 191, 192, 193, 194, 195 | pntibndlem2 27636 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 197 | 196 | anassrs 467 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 198 | 172, 197 | rexlimddv 3160 | . . . . 5
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑧 ∈ ℝ+
((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 199 | 198 | ralrimivva 3201 | . . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 200 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (𝑥(,)+∞) = (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) | 
| 201 | 200 | raleqdv 3325 | . . . . . 6
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) | 
| 202 | 201 | ralbidv 3177 | . . . . 5
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) | 
| 203 | 202 | rspcev 3621 | . . . 4
⊢
((((exp‘(𝑡 /
(𝐸 / 4))) + 𝑍) ∈ ℝ+
∧ ∀𝑘 ∈
((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 204 | 25, 199, 203 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 205 | 204 | rexlimdvaa 3155 | . 2
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) | 
| 206 | 4, 205 | mpi 20 | 1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |