Step | Hyp | Ref
| Expression |
1 | | ioorp 12122 |
. . . 4
⊢
(0(,)+∞) = ℝ+ |
2 | 1 | eqcomi 2619 |
. . 3
⊢
ℝ+ = (0(,)+∞) |
3 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1zzd 11285 |
. . 3
⊢ (⊤
→ 1 ∈ ℤ) |
5 | | ere 14658 |
. . . 4
⊢ e ∈
ℝ |
6 | 5 | a1i 11 |
. . 3
⊢ (⊤
→ e ∈ ℝ) |
7 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
8 | | epos 14774 |
. . . . . 6
⊢ 0 <
e |
9 | 7, 5, 8 | ltleii 10039 |
. . . . 5
⊢ 0 ≤
e |
10 | 9 | a1i 11 |
. . . 4
⊢ (⊤
→ 0 ≤ e) |
11 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
12 | | addge02 10418 |
. . . . 5
⊢ ((1
∈ ℝ ∧ e ∈ ℝ) → (0 ≤ e ↔ 1 ≤ (e +
1))) |
13 | 11, 5, 12 | mp2an 704 |
. . . 4
⊢ (0 ≤ e
↔ 1 ≤ (e + 1)) |
14 | 10, 13 | sylib 207 |
. . 3
⊢ (⊤
→ 1 ≤ (e + 1)) |
15 | 7 | a1i 11 |
. . 3
⊢ (⊤
→ 0 ∈ ℝ) |
16 | | relogcl 24126 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (log‘𝑦) ∈
ℝ) |
17 | 16 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → (log‘𝑦) ∈ ℝ) |
18 | 17 | resqcld 12897 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → ((log‘𝑦)↑2) ∈ ℝ) |
19 | 18 | rehalfcld 11156 |
. . 3
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → (((log‘𝑦)↑2) / 2) ∈
ℝ) |
20 | | rerpdivcl 11737 |
. . . . 5
⊢
(((log‘𝑦)
∈ ℝ ∧ 𝑦
∈ ℝ+) → ((log‘𝑦) / 𝑦) ∈ ℝ) |
21 | 16, 20 | mpancom 700 |
. . . 4
⊢ (𝑦 ∈ ℝ+
→ ((log‘𝑦) /
𝑦) ∈
ℝ) |
22 | 21 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → ((log‘𝑦) / 𝑦) ∈ ℝ) |
23 | | nnrp 11718 |
. . . 4
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
24 | 23, 22 | sylan2 490 |
. . 3
⊢
((⊤ ∧ 𝑦
∈ ℕ) → ((log‘𝑦) / 𝑦) ∈ ℝ) |
25 | | reelprrecn 9907 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
26 | 25 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
27 | | cnelprrecn 9908 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
28 | 27 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
29 | 17 | recnd 9947 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → (log‘𝑦) ∈ ℂ) |
30 | | ovex 6577 |
. . . . . 6
⊢ (1 /
𝑦) ∈
V |
31 | 30 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → (1 / 𝑦) ∈ V) |
32 | | sqcl 12787 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
33 | 32 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
34 | 33 | halfcld 11154 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((𝑥↑2) / 2) ∈
ℂ) |
35 | | simpr 476 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
36 | | dvrelog 24183 |
. . . . . 6
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑦 ∈ ℝ+ ↦ (1 /
𝑦)) |
37 | | relogf1o 24117 |
. . . . . . . . . 10
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
38 | | f1of 6050 |
. . . . . . . . . 10
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
39 | 37, 38 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (log ↾
ℝ+):ℝ+⟶ℝ) |
40 | 39 | feqmptd 6159 |
. . . . . . . 8
⊢ (⊤
→ (log ↾ ℝ+) = (𝑦 ∈ ℝ+ ↦ ((log
↾ ℝ+)‘𝑦))) |
41 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑦) = (log‘𝑦)) |
42 | 41 | mpteq2ia 4668 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑦)) = (𝑦 ∈ ℝ+ ↦
(log‘𝑦)) |
43 | 40, 42 | syl6eq 2660 |
. . . . . . 7
⊢ (⊤
→ (log ↾ ℝ+) = (𝑦 ∈ ℝ+ ↦
(log‘𝑦))) |
44 | 43 | oveq2d 6565 |
. . . . . 6
⊢ (⊤
→ (ℝ D (log ↾ ℝ+)) = (ℝ D (𝑦 ∈ ℝ+
↦ (log‘𝑦)))) |
45 | 36, 44 | syl5reqr 2659 |
. . . . 5
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ+ ↦ (log‘𝑦))) = (𝑦 ∈ ℝ+ ↦ (1 /
𝑦))) |
46 | | ovex 6577 |
. . . . . . . 8
⊢ (2
· 𝑥) ∈
V |
47 | 46 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ V) |
48 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
49 | | dvexp 23522 |
. . . . . . . . 9
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
50 | 48, 49 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
51 | | 2m1e1 11012 |
. . . . . . . . . . . 12
⊢ (2
− 1) = 1 |
52 | 51 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
53 | | exp1 12728 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
54 | 53 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑1) = 𝑥) |
55 | 52, 54 | syl5eq 2656 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑(2 − 1)) = 𝑥) |
56 | 55 | oveq2d 6565 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥)) |
57 | 56 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) |
58 | 50, 57 | eqtrd 2644 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) |
59 | | 2cn 10968 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 2 ∈ ℂ) |
61 | | 2ne0 10990 |
. . . . . . . 8
⊢ 2 ≠
0 |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 2 ≠ 0) |
63 | 28, 33, 47, 58, 60, 62 | dvmptdivc 23534 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ ((𝑥↑2)
/ 2))) = (𝑥 ∈ ℂ
↦ ((2 · 𝑥) /
2))) |
64 | | divcan3 10590 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → ((2 · 𝑥) / 2) = 𝑥) |
65 | 59, 61, 64 | mp3an23 1408 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → ((2
· 𝑥) / 2) = 𝑥) |
66 | 65 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℂ) → ((2 · 𝑥) / 2) = 𝑥) |
67 | 66 | mpteq2dva 4672 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ ((2 · 𝑥) /
2)) = (𝑥 ∈ ℂ
↦ 𝑥)) |
68 | 63, 67 | eqtrd 2644 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ ((𝑥↑2)
/ 2))) = (𝑥 ∈ ℂ
↦ 𝑥)) |
69 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (log‘𝑦) → (𝑥↑2) = ((log‘𝑦)↑2)) |
70 | 69 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 = (log‘𝑦) → ((𝑥↑2) / 2) = (((log‘𝑦)↑2) / 2)) |
71 | | id 22 |
. . . . 5
⊢ (𝑥 = (log‘𝑦) → 𝑥 = (log‘𝑦)) |
72 | 26, 28, 29, 31, 34, 35, 45, 68, 70, 71 | dvmptco 23541 |
. . . 4
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ+ ↦ (((log‘𝑦)↑2) / 2))) = (𝑦 ∈ ℝ+ ↦
((log‘𝑦) · (1
/ 𝑦)))) |
73 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
74 | 73 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → 𝑦 ∈ ℂ) |
75 | | rpne0 11724 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
76 | 75 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → 𝑦 ≠ 0) |
77 | 29, 74, 76 | divrecd 10683 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ ℝ+) → ((log‘𝑦) / 𝑦) = ((log‘𝑦) · (1 / 𝑦))) |
78 | 77 | mpteq2dva 4672 |
. . . 4
⊢ (⊤
→ (𝑦 ∈
ℝ+ ↦ ((log‘𝑦) / 𝑦)) = (𝑦 ∈ ℝ+ ↦
((log‘𝑦) · (1
/ 𝑦)))) |
79 | 72, 78 | eqtr4d 2647 |
. . 3
⊢ (⊤
→ (ℝ D (𝑦 ∈
ℝ+ ↦ (((log‘𝑦)↑2) / 2))) = (𝑦 ∈ ℝ+ ↦
((log‘𝑦) / 𝑦))) |
80 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = 𝑖 → (log‘𝑦) = (log‘𝑖)) |
81 | | id 22 |
. . . 4
⊢ (𝑦 = 𝑖 → 𝑦 = 𝑖) |
82 | 80, 81 | oveq12d 6567 |
. . 3
⊢ (𝑦 = 𝑖 → ((log‘𝑦) / 𝑦) = ((log‘𝑖) / 𝑖)) |
83 | | simp3r 1083 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ≤ 𝑖) |
84 | | simp2l 1080 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ∈ ℝ+) |
85 | 84 | rpred 11748 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ∈ ℝ) |
86 | | simp3l 1082 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → e ≤ 𝑦) |
87 | | simp2r 1081 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑖 ∈ ℝ+) |
88 | 87 | rpred 11748 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑖 ∈ ℝ) |
89 | 5 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → e ∈ ℝ) |
90 | 89, 85, 88, 86, 83 | letrd 10073 |
. . . . 5
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → e ≤ 𝑖) |
91 | | logdivle 24172 |
. . . . 5
⊢ (((𝑦 ∈ ℝ ∧ e ≤
𝑦) ∧ (𝑖 ∈ ℝ ∧ e ≤
𝑖)) → (𝑦 ≤ 𝑖 ↔ ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦))) |
92 | 85, 86, 88, 90, 91 | syl22anc 1319 |
. . . 4
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → (𝑦 ≤ 𝑖 ↔ ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦))) |
93 | 83, 92 | mpbid 221 |
. . 3
⊢
((⊤ ∧ (𝑦
∈ ℝ+ ∧ 𝑖 ∈ ℝ+) ∧ (e ≤
𝑦 ∧ 𝑦 ≤ 𝑖)) → ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦)) |
94 | | logdivsum.1 |
. . 3
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦
(Σ𝑖 ∈
(1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) |
95 | 73 | cxp1d 24252 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ (𝑦↑𝑐1) = 𝑦) |
96 | 95 | oveq2d 6565 |
. . . . 5
⊢ (𝑦 ∈ ℝ+
→ ((log‘𝑦) /
(𝑦↑𝑐1)) =
((log‘𝑦) / 𝑦)) |
97 | 96 | mpteq2ia 4668 |
. . . 4
⊢ (𝑦 ∈ ℝ+
↦ ((log‘𝑦) /
(𝑦↑𝑐1))) = (𝑦 ∈ ℝ+
↦ ((log‘𝑦) /
𝑦)) |
98 | | 1rp 11712 |
. . . . 5
⊢ 1 ∈
ℝ+ |
99 | | cxploglim 24504 |
. . . . 5
⊢ (1 ∈
ℝ+ → (𝑦 ∈ ℝ+ ↦
((log‘𝑦) / (𝑦↑𝑐1)))
⇝𝑟 0) |
100 | 98, 99 | mp1i 13 |
. . . 4
⊢ (⊤
→ (𝑦 ∈
ℝ+ ↦ ((log‘𝑦) / (𝑦↑𝑐1)))
⇝𝑟 0) |
101 | 97, 100 | syl5eqbrr 4619 |
. . 3
⊢ (⊤
→ (𝑦 ∈
ℝ+ ↦ ((log‘𝑦) / 𝑦)) ⇝𝑟
0) |
102 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = 𝐴 → (log‘𝑦) = (log‘𝐴)) |
103 | | id 22 |
. . . 4
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
104 | 102, 103 | oveq12d 6567 |
. . 3
⊢ (𝑦 = 𝐴 → ((log‘𝑦) / 𝑦) = ((log‘𝐴) / 𝐴)) |
105 | 2, 3, 4, 6, 14, 15, 19, 22, 24, 79, 82, 93, 94, 101, 104 | dvfsumrlim3 23600 |
. 2
⊢ (⊤
→ (𝐹:ℝ+⟶ℝ ∧
𝐹 ∈ dom
⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤
𝐴) →
(abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)))) |
106 | 105 | trud 1484 |
1
⊢ (𝐹:ℝ+⟶ℝ ∧
𝐹 ∈ dom
⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤
𝐴) →
(abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴))) |