Step | Hyp | Ref
| Expression |
1 | | 2re 10967 |
. . 3
⊢ 2 ∈
ℝ |
2 | | 1le2 11118 |
. . 3
⊢ 1 ≤
2 |
3 | | chpdifbnd 25044 |
. . 3
⊢ ((2
∈ ℝ ∧ 1 ≤ 2) → ∃𝑡 ∈ ℝ+ ∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣))))) |
4 | 1, 2, 3 | mp2an 704 |
. 2
⊢
∃𝑡 ∈
ℝ+ ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))) |
5 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 ∈
ℝ+) |
6 | | ioossre 12106 |
. . . . . . . . . . . . 13
⊢ (0(,)1)
⊆ ℝ |
7 | | pntibndlem3.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
8 | 6, 7 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) |
9 | | eliooord 12104 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
11 | 10 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐸) |
12 | 8, 11 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ∈
ℝ+) |
14 | | 4nn 11064 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ |
15 | | nnrp 11718 |
. . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
17 | | rpdivcl 11732 |
. . . . . . . . . 10
⊢ ((𝐸 ∈ ℝ+
∧ 4 ∈ ℝ+) → (𝐸 / 4) ∈
ℝ+) |
18 | 13, 16, 17 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 / 4) ∈
ℝ+) |
19 | 5, 18 | rpdivcld 11765 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈
ℝ+) |
20 | 19 | rpred 11748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 / (𝐸 / 4)) ∈ ℝ) |
21 | 20 | rpefcld 14674 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝑡 / (𝐸 / 4))) ∈
ℝ+) |
22 | | pntibndlem3.6 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 ∈
ℝ+) |
24 | 21, 23 | rpaddcld 11763 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈
ℝ+) |
25 | 24 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈
ℝ+) |
26 | | elioore 12076 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → 𝑦 ∈ ℝ) |
27 | 26 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ ℝ) |
28 | 23 | rpred 11748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 ∈
ℝ) |
29 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈ ℝ) |
30 | 20 | reefcld 14657 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝑡 / (𝐸 / 4))) ∈
ℝ) |
31 | 30, 28 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ) |
32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) ∈ ℝ) |
33 | 28, 21 | ltaddrp2d 11782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)) |
35 | | eliooord 12104 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦 ∧ 𝑦 < +∞)) |
36 | 35 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦) |
37 | 36 | ad2antll 761 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) < 𝑦) |
38 | 29, 32, 27, 34, 37 | lttrd 10077 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 < 𝑦) |
39 | 29 | rexrd 9968 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑍 ∈
ℝ*) |
40 | | elioopnf 12138 |
. . . . . . . . . 10
⊢ (𝑍 ∈ ℝ*
→ (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦))) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑦 ∈ (𝑍(,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑍 < 𝑦))) |
42 | 27, 38, 41 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞)) |
43 | 42 | adantlrr 753 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → 𝑦 ∈ (𝑍(,)+∞)) |
44 | | pntibndlem3.c |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = ((2 · 𝐵) +
(log‘2)) |
45 | | pntibndlem3.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
47 | 46 | rpred 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℝ) |
48 | | remulcl 9900 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
49 | 1, 47, 48 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) ∈
ℝ) |
50 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
51 | | relogcl 24126 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(log‘2) ∈ ℝ |
53 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝐵) ∈ ℝ
∧ (log‘2) ∈ ℝ) → ((2 · 𝐵) + (log‘2)) ∈
ℝ) |
54 | 49, 52, 53 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) +
(log‘2)) ∈ ℝ) |
55 | 44, 54 | syl5eqel 2692 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐶 ∈
ℝ) |
56 | 55, 13 | rerpdivcld 11779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) ∈ ℝ) |
57 | 56 | reefcld 14657 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝐶 / 𝐸)) ∈
ℝ) |
58 | | elicopnf 12140 |
. . . . . . . . . . . . . 14
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝑘 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝑘))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝑘 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝑘))) |
60 | 59 | simprbda 651 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝑘 ∈ ℝ) |
61 | 60 | rehalfcld 11156 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ ℝ) |
62 | | pntibndlem3.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2))) |
63 | 13 | rphalfcld 11760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 / 2) ∈
ℝ+) |
64 | 47, 63 | rerpdivcld 11779 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℝ) |
65 | 64 | reefcld 14657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘(𝐵 / (𝐸 / 2))) ∈
ℝ) |
66 | | remulcl 9900 |
. . . . . . . . . . . . . . . 16
⊢
(((exp‘(𝐵 /
(𝐸 / 2))) ∈ ℝ
∧ 2 ∈ ℝ) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) |
67 | 65, 1, 66 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ∈
ℝ) |
69 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
70 | 64 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) ∈ ℂ) |
71 | 52 | recni 9931 |
. . . . . . . . . . . . . . . . . 18
⊢
(log‘2) ∈ ℂ |
72 | | efadd 14663 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 / (𝐸 / 2)) ∈ ℂ ∧ (log‘2)
∈ ℂ) → (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
(exp‘(log‘2)))) |
73 | 70, 71, 72 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
(exp‘(log‘2)))) |
74 | | reeflog 24131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℝ+ → (exp‘(log‘2)) = 2) |
75 | 50, 74 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(exp‘(log‘2)) = 2 |
76 | 75 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢
((exp‘(𝐵 /
(𝐸 / 2))) ·
(exp‘(log‘2))) = ((exp‘(𝐵 / (𝐸 / 2))) · 2) |
77 | 73, 76 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) =
((exp‘(𝐵 / (𝐸 / 2))) ·
2)) |
78 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ∈ ℝ) |
79 | | rerpdivcl 11737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((log‘2) ∈ ℝ ∧ 𝐸 ∈ ℝ+) →
((log‘2) / 𝐸) ∈
ℝ) |
80 | 52, 13, 79 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) / 𝐸) ∈
ℝ) |
81 | 71 | div1i 10632 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((log‘2) / 1) = (log‘2) |
82 | 10 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 < 1) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 < 1) |
84 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ∈
ℝ) |
85 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
86 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐸 < 1
→ 𝐸 ≤
1)) |
87 | 84, 85, 86 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 < 1 → 𝐸 ≤ 1)) |
88 | 83, 87 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐸 ≤ 1) |
89 | 13 | rpregt0d 11754 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ∈ ℝ ∧ 0 <
𝐸)) |
90 | | 1rp 11712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ |
91 | | rpregt0 11722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℝ+ → (1 ∈ ℝ ∧ 0 < 1)) |
92 | 90, 91 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 ∈
ℝ ∧ 0 < 1)) |
93 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 <
2 |
94 | | rplogcl 24154 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℝ ∧ 1 < 2) → (log‘2) ∈
ℝ+) |
95 | 1, 93, 94 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(log‘2) ∈ ℝ+ |
96 | | rpregt0 11722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((log‘2) ∈ ℝ+ → ((log‘2) ∈
ℝ ∧ 0 < (log‘2))) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) ∈ ℝ ∧ 0 < (log‘2))) |
98 | | lediv2 10792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐸 ∈ ℝ ∧ 0 <
𝐸) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ ((log‘2) ∈ ℝ ∧ 0 <
(log‘2))) → (𝐸
≤ 1 ↔ ((log‘2) / 1) ≤ ((log‘2) / 𝐸))) |
99 | 89, 92, 97, 98 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ≤ 1 ↔ ((log‘2) /
1) ≤ ((log‘2) / 𝐸))) |
100 | 88, 99 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((log‘2) / 1) ≤ ((log‘2) / 𝐸)) |
101 | 81, 100 | syl5eqbrr 4619 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ≤ ((log‘2) / 𝐸)) |
102 | 78, 80, 64, 101 | leadd2dd 10521 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) |
103 | 44 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐶 / 𝐸) = (((2 · 𝐵) + (log‘2)) / 𝐸) |
104 | 49 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) ∈
ℂ) |
105 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(log‘2) ∈ ℂ) |
106 | | rpcnne0 11726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸 ∈ ℝ+
→ (𝐸 ∈ ℂ
∧ 𝐸 ≠
0)) |
107 | 13, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) |
108 | | divdir 10589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝐵) ∈ ℂ
∧ (log‘2) ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → (((2 · 𝐵) + (log‘2)) / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸))) |
109 | 104, 105,
107, 108 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((2
· 𝐵) +
(log‘2)) / 𝐸) = (((2
· 𝐵) / 𝐸) + ((log‘2) / 𝐸))) |
110 | 103, 109 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = (((2 · 𝐵) / 𝐸) + ((log‘2) / 𝐸))) |
111 | 1 | recni 9931 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℂ |
112 | 47 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ∈
ℂ) |
113 | | mulcom 9901 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℂ) → (2 · 𝐵) = (𝐵 · 2)) |
114 | 111, 112,
113 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2
· 𝐵) = (𝐵 · 2)) |
115 | 114 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) / 𝐸) = ((𝐵 · 2) / 𝐸)) |
116 | | rpcnne0 11726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) |
117 | 50, 116 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (2 ∈
ℂ ∧ 2 ≠ 0)) |
118 | | divdiv2 10616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (𝐵
/ (𝐸 / 2)) = ((𝐵 · 2) / 𝐸)) |
119 | 112, 107,
117, 118 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐵 / (𝐸 / 2)) = ((𝐵 · 2) / 𝐸)) |
120 | 115, 119 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((2
· 𝐵) / 𝐸) = (𝐵 / (𝐸 / 2))) |
121 | 120 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((2
· 𝐵) / 𝐸) + ((log‘2) / 𝐸)) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) |
122 | 110, 121 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝐶 / 𝐸) = ((𝐵 / (𝐸 / 2)) + ((log‘2) / 𝐸))) |
123 | 102, 122 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸)) |
124 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 / (𝐸 / 2)) ∈ ℝ ∧ (log‘2)
∈ ℝ) → ((𝐵
/ (𝐸 / 2)) + (log‘2))
∈ ℝ) |
125 | 64, 52, 124 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝐵 / (𝐸 / 2)) + (log‘2)) ∈
ℝ) |
126 | | efle 14687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 / (𝐸 / 2)) + (log‘2)) ∈ ℝ ∧
(𝐶 / 𝐸) ∈ ℝ) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸)))) |
127 | 125, 56, 126 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((𝐵 / (𝐸 / 2)) + (log‘2)) ≤ (𝐶 / 𝐸) ↔ (exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸)))) |
128 | 123, 127 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(exp‘((𝐵 / (𝐸 / 2)) + (log‘2))) ≤
(exp‘(𝐶 / 𝐸))) |
129 | 77, 128 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤
(exp‘(𝐶 / 𝐸))) |
130 | 129 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ (exp‘(𝐶 / 𝐸))) |
131 | 59 | simplbda 652 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ≤ 𝑘) |
132 | 68, 69, 60, 130, 131 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘) |
133 | 65 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ∈ ℝ) |
134 | | rpregt0 11722 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ+ → (2 ∈ ℝ ∧ 0 < 2)) |
135 | 50, 134 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (2 ∈ ℝ
∧ 0 < 2)) |
136 | | lemuldiv 10782 |
. . . . . . . . . . . . . 14
⊢
(((exp‘(𝐵 /
(𝐸 / 2))) ∈ ℝ
∧ 𝑘 ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2))) |
137 | 133, 60, 135, 136 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (((exp‘(𝐵 / (𝐸 / 2))) · 2) ≤ 𝑘 ↔ (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2))) |
138 | 132, 137 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐵 / (𝐸 / 2))) ≤ (𝑘 / 2)) |
139 | 62, 138 | syl5eqbr 4618 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ≤ (𝑘 / 2)) |
140 | 62, 133 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → 𝐾 ∈ ℝ) |
141 | | elicopnf 12140 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℝ → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2)))) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → ((𝑘 / 2) ∈ (𝐾[,)+∞) ↔ ((𝑘 / 2) ∈ ℝ ∧ 𝐾 ≤ (𝑘 / 2)))) |
143 | 61, 139, 142 | mpbir2and 959 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (𝑘 / 2) ∈ (𝐾[,)+∞)) |
144 | 143 | adantrr 749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞)) |
145 | 144 | adantlrr 753 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → (𝑘 / 2) ∈ (𝐾[,)+∞)) |
146 | | pntibndlem3.5 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) |
147 | 146 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) |
148 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 / 2) → (𝑚 · 𝑣) = ((𝑘 / 2) · 𝑣)) |
149 | 148 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 / 2) → (𝑖 ≤ (𝑚 · 𝑣) ↔ 𝑖 ≤ ((𝑘 / 2) · 𝑣))) |
150 | 149 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 / 2) → ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ↔ (𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)))) |
151 | 150 | anbi1d 737 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 / 2) → (((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) |
152 | 151 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑘 / 2) → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) |
153 | 152 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑚 = (𝑘 / 2) → (∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) |
154 | 153 | rspcv 3278 |
. . . . . . . 8
⊢ ((𝑘 / 2) ∈ (𝐾[,)+∞) → (∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) → ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)))) |
155 | 145, 147,
154 | sylc 63 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2))) |
156 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (𝑣 < 𝑖 ↔ 𝑣 < 𝑛)) |
157 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (𝑖 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑣))) |
158 | 156, 157 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑛 → ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)))) |
159 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝑅‘𝑖) = (𝑅‘𝑛)) |
160 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → 𝑖 = 𝑛) |
161 | 159, 160 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → ((𝑅‘𝑖) / 𝑖) = ((𝑅‘𝑛) / 𝑛)) |
162 | 161 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (abs‘((𝑅‘𝑖) / 𝑖)) = (abs‘((𝑅‘𝑛) / 𝑛))) |
163 | 162 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑛 → ((abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2) ↔ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) |
164 | 158, 163 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) |
165 | 164 | cbvrexv 3148 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) |
166 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑦 → (𝑣 < 𝑛 ↔ 𝑦 < 𝑛)) |
167 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑦 → ((𝑘 / 2) · 𝑣) = ((𝑘 / 2) · 𝑦)) |
168 | 167 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑦 → (𝑛 ≤ ((𝑘 / 2) · 𝑣) ↔ 𝑛 ≤ ((𝑘 / 2) · 𝑦))) |
169 | 166, 168 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑦 → ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ↔ (𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)))) |
170 | 169 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑦 → (((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) |
171 | 170 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → (∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) |
172 | 165, 171 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) ↔ ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) |
173 | 172 | rspcv 3278 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑍(,)+∞) → (∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖 ∧ 𝑖 ≤ ((𝑘 / 2) · 𝑣)) ∧ (abs‘((𝑅‘𝑖) / 𝑖)) ≤ (𝐸 / 2)) → ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) |
174 | 43, 155, 173 | sylc 63 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑛 ∈ ℕ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) |
175 | | pntibnd.r |
. . . . . . . 8
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
176 | | pntibndlem1.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
177 | 176 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐴 ∈
ℝ+) |
178 | | pntibndlem1.l |
. . . . . . . 8
⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) |
179 | | pntibndlem3.2 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
180 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝑅‘𝑥) = (𝑅‘𝑣)) |
181 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → 𝑥 = 𝑣) |
182 | 180, 181 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑣) / 𝑣)) |
183 | 182 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑣) / 𝑣))) |
184 | 183 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴)) |
185 | 184 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) |
186 | 179, 185 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) |
187 | 186 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ ℝ+
(abs‘((𝑅‘𝑣) / 𝑣)) ≤ 𝐴) |
188 | 45 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐵 ∈
ℝ+) |
189 | 7 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝐸 ∈ (0(,)1)) |
190 | 22 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑍 ∈
ℝ+) |
191 | | simprrl 800 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑛 ∈ ℕ) |
192 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑡 ∈ ℝ+) |
193 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∀𝑣 ∈ (1(,)+∞)∀𝑤 ∈ (𝑣[,](2 · 𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣))))) |
194 | | eqid 2610 |
. . . . . . . 8
⊢
((exp‘(𝑡 /
(𝐸 / 4))) + 𝑍) = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) |
195 | | simprll 798 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
196 | | simprlr 799 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) |
197 | | simprrr 801 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))) |
198 | 175, 177,
178, 187, 188, 62, 44, 189, 190, 191, 192, 193, 194, 195, 196, 197 | pntibndlem2 25080 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ ((𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2))))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
199 | 198 | anassrs 678 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) ∧ (𝑛 ∈ ℕ ∧ ((𝑦 < 𝑛 ∧ 𝑛 ≤ ((𝑘 / 2) · 𝑦)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝐸 / 2)))) → ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
200 | 174, 199 | rexlimddv 3017 |
. . . . 5
⊢ (((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) ∧ (𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ∧ 𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞))) → ∃𝑧 ∈ ℝ+
((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
201 | 200 | ralrimivva 2954 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
202 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (𝑥(,)+∞) = (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)) |
203 | 202 | raleqdv 3121 |
. . . . . 6
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
204 | 203 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = ((exp‘(𝑡 / (𝐸 / 4))) + 𝑍) → (∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸) ↔ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
205 | 204 | rspcev 3282 |
. . . 4
⊢
((((exp‘(𝑡 /
(𝐸 / 4))) + 𝑍) ∈ ℝ+
∧ ∀𝑘 ∈
((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (((exp‘(𝑡 / (𝐸 / 4))) + 𝑍)(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
206 | 25, 201, 205 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ (𝑡 ∈ ℝ+ ∧
∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))))) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
207 | 206 | rexlimdvaa 3014 |
. 2
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑣 ∈
(1(,)+∞)∀𝑤
∈ (𝑣[,](2 ·
𝑣))((ψ‘𝑤) − (ψ‘𝑣)) ≤ ((2 · (𝑤 − 𝑣)) + (𝑡 · (𝑣 / (log‘𝑣)))) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))) |
208 | 4, 207 | mpi 20 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |