Step | Hyp | Ref
| Expression |
1 | | rpre 11715 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
2 | | chpcl 24650 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
4 | 3 | recnd 9947 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
5 | | rprege0 11723 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
6 | | flge0nn0 12483 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
8 | | nn0p1nn 11209 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
10 | 9 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℝ+) |
11 | 10 | relogcld 24173 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℂ) |
13 | | relogcl 24126 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
14 | 13 | recnd 9947 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
15 | 12, 14 | subcld 10271 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ) |
16 | 4, 15 | mulcld 9939 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ) |
17 | | fzfid 12634 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
18 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
20 | 19 | nnrpd 11746 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
21 | | 1rp 11712 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
22 | | rpaddcl 11730 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑛 + 1) ∈
ℝ+) |
23 | 21, 22 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 + 1) ∈
ℝ+) |
24 | 23 | relogcld 24173 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘(𝑛 + 1))
∈ ℝ) |
25 | | relogcl 24126 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
26 | 24, 25 | resubcld 10337 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛))
∈ ℝ) |
27 | | rpre 11715 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
28 | | chpcl 24650 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ →
(ψ‘𝑛) ∈
ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℝ) |
30 | 26, 29 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
32 | 20, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
33 | 17, 32 | fsumcl 14311 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
34 | | rpcnne0 11726 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
35 | | divsubdir 10600 |
. . . . . 6
⊢
((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ ∧ Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((ψ‘𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
36 | 16, 33, 34, 35 | syl3anc 1318 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
37 | 4, 12 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) ∈ ℂ) |
38 | 4, 14 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘𝑥))
∈ ℂ) |
39 | 37, 38, 33 | sub32d 10303 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
40 | 4, 12, 14 | subdid 10365 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) −
((ψ‘𝑥) ·
(log‘𝑥)))) |
41 | 40 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
42 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (log‘𝑚) = (log‘𝑛)) |
43 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
45 | 42, 44 | jca 553 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((log‘𝑚) = (log‘𝑛) ∧ (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))) |
46 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (log‘𝑚) = (log‘(𝑛 + 1))) |
47 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
49 | 46, 48 | jca 553 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((log‘𝑚) = (log‘(𝑛 + 1)) ∧ (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1)))) |
50 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (log‘𝑚) =
(log‘1)) |
51 | | log1 24136 |
. . . . . . . . . . . 12
⊢
(log‘1) = 0 |
52 | 50, 51 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (log‘𝑚) = 0) |
53 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
54 | | 1m1e0 10966 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
55 | 53, 54 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
56 | 55 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
57 | | 2pos 10989 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
58 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
59 | | chpeq0 24733 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
61 | 57, 60 | mpbir 220 |
. . . . . . . . . . . 12
⊢
(ψ‘0) = 0 |
62 | 56, 61 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
63 | 52, 62 | jca 553 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((log‘𝑚) = 0 ∧ (ψ‘(𝑚 − 1)) =
0)) |
64 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (log‘𝑚) =
(log‘((⌊‘𝑥) + 1))) |
65 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
66 | 65 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
67 | 64, 66 | jca 553 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((log‘𝑚) =
(log‘((⌊‘𝑥) + 1)) ∧ (ψ‘(𝑚 − 1)) =
(ψ‘(((⌊‘𝑥) + 1) − 1)))) |
68 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
69 | 9, 68 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
70 | | elfznn 12241 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
72 | 71 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ+) |
73 | 72 | relogcld 24173 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℝ) |
74 | 73 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℂ) |
75 | 71 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
76 | | peano2rem 10227 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
78 | | chpcl 24650 |
. . . . . . . . . . . 12
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
80 | 79 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℂ) |
81 | 45, 49, 63, 67, 69, 74, 80 | fsumparts 14379 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) =
((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))))) |
82 | 7 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℤ) |
83 | | fzval3 12404 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
85 | 84 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) |
86 | 19 | nncnd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
87 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
88 | | pncan 10166 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
89 | 86, 87, 88 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
90 | | npcan 10169 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
91 | 86, 87, 90 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
92 | 89, 91 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= ((𝑛 − 1) +
1)) |
93 | 92 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘((𝑛 − 1) + 1))) |
94 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
95 | 19, 94 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
96 | | chpp1 24681 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
98 | 91 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
99 | 98 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
100 | 93, 97, 99 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (((ψ‘(𝑛 − 1)) +
(Λ‘𝑛)) −
(ψ‘(𝑛 −
1)))) |
102 | 95 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
103 | | chpcl 24650 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
105 | 104 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
106 | | vmacl 24644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
107 | 19, 106 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
108 | 107 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
109 | 105, 108 | pncan2d 10273 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘(𝑛
− 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
110 | 101, 109 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
111 | 110 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((log‘𝑛) · (Λ‘𝑛))) |
112 | 20 | relogcld 24173 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
113 | 112 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
114 | 108, 113 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (log‘𝑛)) =
((log‘𝑛) ·
(Λ‘𝑛))) |
115 | 111, 114 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((Λ‘𝑛) · (log‘𝑛))) |
116 | 85, 115 | sumeq12rdv 14285 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛))) |
117 | 7 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℂ) |
118 | | pncan 10166 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
119 | 117, 87, 118 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) − 1) = (⌊‘𝑥)) |
120 | 119 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
121 | | chpfl 24676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
122 | 1, 121 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
123 | 120, 122 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
124 | 123 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) =
((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥))) |
125 | 12, 4 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥)) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
126 | 124, 125 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
127 | | 0cn 9911 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
128 | 127 | mul01i 10105 |
. . . . . . . . . . . . 13
⊢ (0
· 0) = 0 |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (0 · 0) = 0) |
130 | 126, 129 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
(((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − 0)) |
131 | 37 | subid1d 10260 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − 0) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
132 | 130, 131 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
133 | 89 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘𝑛)) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
135 | 85, 134 | sumeq12rdv 14285 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
136 | 132, 135 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1)))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
137 | 81, 116, 136 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
138 | 137 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
139 | 39, 41, 138 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥)))) |
140 | 139 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
141 | | div23 10583 |
. . . . . . 7
⊢
(((ψ‘𝑥)
∈ ℂ ∧ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
142 | 4, 15, 34, 141 | syl3anc 1318 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
143 | 142 | oveq1d 6564 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
144 | 36, 140, 143 | 3eqtr3rd 2653 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥) /
𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
145 | 144 | mpteq2ia 4668 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((((ψ‘𝑥)
/ 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
146 | | ovex 6577 |
. . . . 5
⊢
(((ψ‘𝑥) /
𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ V |
147 | 146 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ V) |
148 | | ovex 6577 |
. . . . 5
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥) ∈ V |
149 | 148 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥) ∈ V) |
150 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
151 | | rpssre 11719 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
152 | 150, 151 | ssexi 4731 |
. . . . . . 7
⊢
ℝ+ ∈ V |
153 | 152 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ+ ∈ V) |
154 | | ovex 6577 |
. . . . . . 7
⊢
((ψ‘𝑥) /
𝑥) ∈
V |
155 | 154 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ V) |
156 | 15 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℂ) |
157 | | eqidd 2611 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
158 | | eqidd 2611 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
159 | 153, 155,
156, 157, 158 | offval2 6812 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))) |
160 | | chpo1ub 24969 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
161 | | 0red 9920 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℝ) |
162 | | 1red 9934 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
163 | | divrcnv 14423 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
164 | 87, 163 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
165 | | rpreccl 11733 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
166 | 165 | rpred 11748 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) |
167 | 166 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ ℝ) |
168 | 11, 13 | resubcld 10337 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℝ) |
169 | 168 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℝ) |
170 | | rpaddcl 11730 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
171 | 21, 170 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 + 1) ∈
ℝ+) |
172 | 171 | relogcld 24173 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘(𝑥 + 1))
∈ ℝ) |
173 | 172, 13 | resubcld 10337 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥))
∈ ℝ) |
174 | 7 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℝ) |
175 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 1 ∈ ℝ) |
176 | | flle 12462 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
177 | 1, 176 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
≤ 𝑥) |
178 | 174, 1, 175, 177 | leadd1dd 10520 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ≤ (𝑥 +
1)) |
179 | 10, 171 | logled 24177 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) ≤ (𝑥 + 1) ↔
(log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1)))) |
180 | 178, 179 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1))) |
181 | 11, 172, 13, 180 | lesub1dd 10522 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ ((log‘(𝑥 + 1)) − (log‘𝑥))) |
182 | | logdifbnd 24520 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥)) ≤
(1 / 𝑥)) |
183 | 168, 173,
166, 181, 182 | letrd 10073 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
184 | 183 | ad2antrl 760 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
185 | | fllep1 12464 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
186 | 1, 185 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≤
((⌊‘𝑥) +
1)) |
187 | | logleb 24153 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ ((⌊‘𝑥) +
1) ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
188 | 10, 187 | mpdan 699 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1)))) |
189 | 186, 188 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1))) |
190 | 11, 13 | subge0d 10496 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
191 | 189, 190 | mpbird 246 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
192 | 191 | ad2antrl 760 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
193 | 161, 162,
164, 167, 169, 184, 192 | rlimsqz2 14229 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟
0) |
194 | | rlimo1 14195 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟 0 →
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
195 | 193, 194 | syl 17 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
196 | | o1mul 14193 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥))
∘𝑓 · (𝑥 ∈ ℝ+ ↦
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
197 | 160, 195,
196 | sylancr 694 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
198 | 159, 197 | eqeltrrd 2689 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈
𝑂(1)) |
199 | | nnrp 11718 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
200 | 199 | ssriv 3572 |
. . . . . . . 8
⊢ ℕ
⊆ ℝ+ |
201 | 200 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℕ ⊆ ℝ+) |
202 | 201 | sselda 3568 |
. . . . . 6
⊢
((⊤ ∧ 𝑛
∈ ℕ) → 𝑛
∈ ℝ+) |
203 | 202, 31 | syl 17 |
. . . . 5
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
204 | | chpo1ub 24969 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
↦ ((ψ‘𝑛) /
𝑛)) ∈
𝑂(1) |
205 | 204 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ ((ψ‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
206 | | rerpdivcl 11737 |
. . . . . . . . 9
⊢
(((ψ‘𝑛)
∈ ℝ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
207 | 29, 206 | mpancom 700 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) ∈
ℝ) |
208 | 207 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
209 | 31 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
210 | | rpreccl 11733 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
211 | 210 | rpred 11748 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ) |
212 | | chpge0 24652 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → 0 ≤
(ψ‘𝑛)) |
213 | 27, 212 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (ψ‘𝑛)) |
214 | | logdifbnd 24520 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛)) ≤
(1 / 𝑛)) |
215 | 26, 211, 29, 213, 214 | lemul1ad 10842 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
≤ ((1 / 𝑛) ·
(ψ‘𝑛))) |
216 | 27 | lep1d 10834 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≤ (𝑛 + 1)) |
217 | | logleb 24153 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ+
∧ (𝑛 + 1) ∈
ℝ+) → (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
218 | 23, 217 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
219 | 216, 218 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ≤
(log‘(𝑛 +
1))) |
220 | 24, 25 | subge0d 10496 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛)) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
221 | 219, 220 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛))) |
222 | 26, 29, 221, 213 | mulge0d 10483 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
223 | 30, 222 | absidd 14009 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
224 | | rpregt0 11722 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) |
225 | | divge0 10771 |
. . . . . . . . . . . 12
⊢
((((ψ‘𝑛)
∈ ℝ ∧ 0 ≤ (ψ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤
((ψ‘𝑛) / 𝑛)) |
226 | 29, 213, 224, 225 | syl21anc 1317 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((ψ‘𝑛) / 𝑛)) |
227 | 207, 226 | absidd 14009 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((ψ‘𝑛) / 𝑛)) |
228 | 29 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℂ) |
229 | | rpcn 11717 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℂ) |
230 | | rpne0 11724 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≠
0) |
231 | 228, 229,
230 | divrec2d 10684 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) = ((1 / 𝑛) · (ψ‘𝑛))) |
232 | 227, 231 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((1 / 𝑛) · (ψ‘𝑛))) |
233 | 215, 223,
232 | 3brtr4d 4615 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤ (abs‘((ψ‘𝑛) / 𝑛))) |
234 | 233 | ad2antrl 760 |
. . . . . . 7
⊢
((⊤ ∧ (𝑛
∈ ℝ+ ∧ 1 ≤ 𝑛)) → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤
(abs‘((ψ‘𝑛)
/ 𝑛))) |
235 | 162, 205,
208, 209, 234 | o1le 14231 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ∈ 𝑂(1)) |
236 | 201, 235 | o1res2 14142 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛)))
∈ 𝑂(1)) |
237 | 203, 236 | o1fsum 14386 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) |
238 | 147, 149,
198, 237 | o1sub2 14204 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) ∈ 𝑂(1)) |
239 | 145, 238 | syl5eqelr 2693 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)) |
240 | 239 | trud 1484 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |