Step |
Hyp |
Ref |
Expression |
1 |
|
logdivsum.1 |
⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) |
2 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
3 |
2
|
eqcomi |
⊢ ℝ+ = ( 0 (,) +∞ ) |
4 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
5 |
|
1zzd |
⊢ ( ⊤ → 1 ∈ ℤ ) |
6 |
|
ere |
⊢ e ∈ ℝ |
7 |
6
|
a1i |
⊢ ( ⊤ → e ∈ ℝ ) |
8 |
|
0re |
⊢ 0 ∈ ℝ |
9 |
|
epos |
⊢ 0 < e |
10 |
8 6 9
|
ltleii |
⊢ 0 ≤ e |
11 |
10
|
a1i |
⊢ ( ⊤ → 0 ≤ e ) |
12 |
|
1re |
⊢ 1 ∈ ℝ |
13 |
|
addge02 |
⊢ ( ( 1 ∈ ℝ ∧ e ∈ ℝ ) → ( 0 ≤ e ↔ 1 ≤ ( e + 1 ) ) ) |
14 |
12 6 13
|
mp2an |
⊢ ( 0 ≤ e ↔ 1 ≤ ( e + 1 ) ) |
15 |
11 14
|
sylib |
⊢ ( ⊤ → 1 ≤ ( e + 1 ) ) |
16 |
8
|
a1i |
⊢ ( ⊤ → 0 ∈ ℝ ) |
17 |
|
relogcl |
⊢ ( 𝑦 ∈ ℝ+ → ( log ‘ 𝑦 ) ∈ ℝ ) |
18 |
17
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( log ‘ 𝑦 ) ∈ ℝ ) |
19 |
18
|
resqcld |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ 𝑦 ) ↑ 2 ) ∈ ℝ ) |
20 |
19
|
rehalfcld |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ∈ ℝ ) |
21 |
|
rerpdivcl |
⊢ ( ( ( log ‘ 𝑦 ) ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ ) |
22 |
17 21
|
mpancom |
⊢ ( 𝑦 ∈ ℝ+ → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ ) |
23 |
22
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ ) |
24 |
|
nnrp |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ ) |
25 |
24 23
|
sylan2 |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℕ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ ) |
26 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
27 |
26
|
a1i |
⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } ) |
28 |
|
cnelprrecn |
⊢ ℂ ∈ { ℝ , ℂ } |
29 |
28
|
a1i |
⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } ) |
30 |
18
|
recnd |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
31 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( 1 / 𝑦 ) ∈ V ) |
32 |
|
sqcl |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
33 |
32
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
34 |
33
|
halfcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) / 2 ) ∈ ℂ ) |
35 |
|
simpr |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ ) |
36 |
|
relogf1o |
⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ |
37 |
|
f1of |
⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
38 |
36 37
|
mp1i |
⊢ ( ⊤ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ) |
39 |
38
|
feqmptd |
⊢ ( ⊤ → ( log ↾ ℝ+ ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) ) |
40 |
|
fvres |
⊢ ( 𝑦 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑦 ) = ( log ‘ 𝑦 ) ) |
41 |
40
|
mpteq2ia |
⊢ ( 𝑦 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑦 ) ) = ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) |
42 |
39 41
|
eqtrdi |
⊢ ( ⊤ → ( log ↾ ℝ+ ) = ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) |
43 |
42
|
oveq2d |
⊢ ( ⊤ → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) ) |
44 |
|
dvrelog |
⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑦 ∈ ℝ+ ↦ ( 1 / 𝑦 ) ) |
45 |
43 44
|
eqtr3di |
⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( 1 / 𝑦 ) ) ) |
46 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ V ) |
47 |
|
2nn |
⊢ 2 ∈ ℕ |
48 |
|
dvexp |
⊢ ( 2 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) ) |
49 |
47 48
|
mp1i |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) ) |
50 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
51 |
50
|
oveq2i |
⊢ ( 𝑥 ↑ ( 2 − 1 ) ) = ( 𝑥 ↑ 1 ) |
52 |
|
exp1 |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 1 ) = 𝑥 ) |
53 |
52
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 1 ) = 𝑥 ) |
54 |
51 53
|
eqtrid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 2 − 1 ) ) = 𝑥 ) |
55 |
54
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) = ( 2 · 𝑥 ) ) |
56 |
55
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ) |
57 |
49 56
|
eqtrd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ) |
58 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
59 |
|
2ne0 |
⊢ 2 ≠ 0 |
60 |
59
|
a1i |
⊢ ( ⊤ → 2 ≠ 0 ) |
61 |
29 33 46 57 58 60
|
dvmptdivc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 2 ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) / 2 ) ) ) |
62 |
|
2cn |
⊢ 2 ∈ ℂ |
63 |
|
divcan3 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 ) |
64 |
62 59 63
|
mp3an23 |
⊢ ( 𝑥 ∈ ℂ → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 ) |
65 |
64
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 ) |
66 |
65
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) / 2 ) ) = ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) |
67 |
61 66
|
eqtrd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 2 ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) |
68 |
|
oveq1 |
⊢ ( 𝑥 = ( log ‘ 𝑦 ) → ( 𝑥 ↑ 2 ) = ( ( log ‘ 𝑦 ) ↑ 2 ) ) |
69 |
68
|
oveq1d |
⊢ ( 𝑥 = ( log ‘ 𝑦 ) → ( ( 𝑥 ↑ 2 ) / 2 ) = ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) |
70 |
|
id |
⊢ ( 𝑥 = ( log ‘ 𝑦 ) → 𝑥 = ( log ‘ 𝑦 ) ) |
71 |
27 29 30 31 34 35 45 67 69 70
|
dvmptco |
⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) ) ) |
72 |
|
rpcn |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ ) |
73 |
72
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℂ ) |
74 |
|
rpne0 |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≠ 0 ) |
75 |
74
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ≠ 0 ) |
76 |
30 73 75
|
divrecd |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ+ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) ) |
77 |
76
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) ) ) |
78 |
71 77
|
eqtr4d |
⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) |
79 |
|
fveq2 |
⊢ ( 𝑦 = 𝑖 → ( log ‘ 𝑦 ) = ( log ‘ 𝑖 ) ) |
80 |
|
id |
⊢ ( 𝑦 = 𝑖 → 𝑦 = 𝑖 ) |
81 |
79 80
|
oveq12d |
⊢ ( 𝑦 = 𝑖 → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝑖 ) / 𝑖 ) ) |
82 |
|
simp3r |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ≤ 𝑖 ) |
83 |
|
simp2l |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ∈ ℝ+ ) |
84 |
83
|
rpred |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ∈ ℝ ) |
85 |
|
simp3l |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ≤ 𝑦 ) |
86 |
|
simp2r |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑖 ∈ ℝ+ ) |
87 |
86
|
rpred |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑖 ∈ ℝ ) |
88 |
6
|
a1i |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ∈ ℝ ) |
89 |
88 84 87 85 82
|
letrd |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ≤ 𝑖 ) |
90 |
|
logdivle |
⊢ ( ( ( 𝑦 ∈ ℝ ∧ e ≤ 𝑦 ) ∧ ( 𝑖 ∈ ℝ ∧ e ≤ 𝑖 ) ) → ( 𝑦 ≤ 𝑖 ↔ ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) |
91 |
84 85 87 89 90
|
syl22anc |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → ( 𝑦 ≤ 𝑖 ↔ ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) |
92 |
82 91
|
mpbid |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑖 ∈ ℝ+ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) ) |
93 |
72
|
cxp1d |
⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 ↑𝑐 1 ) = 𝑦 ) |
94 |
93
|
oveq2d |
⊢ ( 𝑦 ∈ ℝ+ → ( ( log ‘ 𝑦 ) / ( 𝑦 ↑𝑐 1 ) ) = ( ( log ‘ 𝑦 ) / 𝑦 ) ) |
95 |
94
|
mpteq2ia |
⊢ ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑𝑐 1 ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) |
96 |
|
1rp |
⊢ 1 ∈ ℝ+ |
97 |
|
cxploglim |
⊢ ( 1 ∈ ℝ+ → ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑𝑐 1 ) ) ) ⇝𝑟 0 ) |
98 |
96 97
|
mp1i |
⊢ ( ⊤ → ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑𝑐 1 ) ) ) ⇝𝑟 0 ) |
99 |
95 98
|
eqbrtrrid |
⊢ ( ⊤ → ( 𝑦 ∈ ℝ+ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) ⇝𝑟 0 ) |
100 |
|
fveq2 |
⊢ ( 𝑦 = 𝐴 → ( log ‘ 𝑦 ) = ( log ‘ 𝐴 ) ) |
101 |
|
id |
⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 ) |
102 |
100 101
|
oveq12d |
⊢ ( 𝑦 = 𝐴 → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ) |
103 |
3 4 5 7 15 16 20 23 25 78 81 92 1 99 102
|
dvfsumrlim3 |
⊢ ( ⊤ → ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) ) ) |
104 |
103
|
mptru |
⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) ) |