Step | Hyp | Ref
| Expression |
1 | | rpre 12145 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
2 | | chpcl 25302 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
4 | 3 | recnd 10405 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
5 | | rprege0 12154 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
6 | | flge0nn0 12940 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
8 | | nn0p1nn 11683 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
10 | 9 | nnrpd 12179 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℝ+) |
11 | 10 | relogcld 24806 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℝ) |
12 | 11 | recnd 10405 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℂ) |
13 | | relogcl 24759 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
14 | 13 | recnd 10405 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
15 | 12, 14 | subcld 10734 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ) |
16 | 4, 15 | mulcld 10397 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ) |
17 | | fzfid 13091 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
18 | | elfznn 12687 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
19 | 18 | adantl 475 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
20 | 19 | nnrpd 12179 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
21 | | 1rp 12141 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
22 | | rpaddcl 12161 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑛 + 1) ∈
ℝ+) |
23 | 21, 22 | mpan2 681 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 + 1) ∈
ℝ+) |
24 | 23 | relogcld 24806 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘(𝑛 + 1))
∈ ℝ) |
25 | | relogcl 24759 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
26 | 24, 25 | resubcld 10803 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛))
∈ ℝ) |
27 | | rpre 12145 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
28 | | chpcl 25302 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ →
(ψ‘𝑛) ∈
ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℝ) |
30 | 26, 29 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℝ) |
31 | 30 | recnd 10405 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
32 | 20, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
33 | 17, 32 | fsumcl 14871 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
34 | | rpcnne0 12157 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
35 | | divsubdir 11069 |
. . . . . 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 1439 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
37 | 4, 12 | mulcld 10397 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) ∈ ℂ) |
38 | 4, 14 | mulcld 10397 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘𝑥))
∈ ℂ) |
39 | 37, 38, 33 | sub32d 10766 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
40 | 4, 12, 14 | subdid 10831 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) −
((ψ‘𝑥) ·
(log‘𝑥)))) |
41 | 40 | oveq1d 6937 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
42 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (log‘𝑚) = (log‘𝑛)) |
43 | | fvoveq1 6945 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
44 | 42, 43 | jca 507 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((log‘𝑚) = (log‘𝑛) ∧ (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))) |
45 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (log‘𝑚) = (log‘(𝑛 + 1))) |
46 | | fvoveq1 6945 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
47 | 45, 46 | jca 507 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((log‘𝑚) = (log‘(𝑛 + 1)) ∧ (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1)))) |
48 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (log‘𝑚) =
(log‘1)) |
49 | | log1 24769 |
. . . . . . . . . . . 12
⊢
(log‘1) = 0 |
50 | 48, 49 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (log‘𝑚) = 0) |
51 | | oveq1 6929 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
52 | | 1m1e0 11447 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
53 | 51, 52 | syl6eq 2829 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
54 | 53 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
55 | | 2pos 11485 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
56 | | 0re 10378 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
57 | | chpeq0 25385 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
59 | 55, 58 | mpbir 223 |
. . . . . . . . . . . 12
⊢
(ψ‘0) = 0 |
60 | 54, 59 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
61 | 50, 60 | jca 507 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((log‘𝑚) = 0 ∧ (ψ‘(𝑚 − 1)) =
0)) |
62 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (log‘𝑚) =
(log‘((⌊‘𝑥) + 1))) |
63 | | fvoveq1 6945 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
64 | 62, 63 | jca 507 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((log‘𝑚) =
(log‘((⌊‘𝑥) + 1)) ∧ (ψ‘(𝑚 − 1)) =
(ψ‘(((⌊‘𝑥) + 1) − 1)))) |
65 | | nnuz 12029 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
66 | 9, 65 | syl6eleq 2868 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
67 | | elfznn 12687 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
68 | 67 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
69 | 68 | nnrpd 12179 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ+) |
70 | 69 | relogcld 24806 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℝ) |
71 | 70 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℂ) |
72 | 68 | nnred 11391 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
73 | | peano2rem 10690 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
75 | | chpcl 25302 |
. . . . . . . . . . . 12
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
77 | 76 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℂ) |
78 | 44, 47, 61, 64, 66, 71, 77 | fsumparts 14942 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) =
((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))))) |
79 | 7 | nn0zd 11832 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℤ) |
80 | | fzval3 12856 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
82 | 81 | eqcomd 2783 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) |
83 | | nnm1nn0 11685 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
84 | 19, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
85 | 84 | nn0red 11703 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
86 | | chpcl 25302 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
88 | 87 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
89 | | vmacl 25296 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
90 | 19, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
91 | 90 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
92 | 19 | nncnd 11392 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
93 | | ax-1cn 10330 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
94 | | pncan 10628 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
95 | 92, 93, 94 | sylancl 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
96 | | npcan 10632 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
97 | 92, 93, 96 | sylancl 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
98 | 95, 97 | eqtr4d 2816 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= ((𝑛 − 1) +
1)) |
99 | 98 | fveq2d 6450 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘((𝑛 − 1) + 1))) |
100 | | chpp1 25333 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
101 | 84, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
102 | 97 | fveq2d 6450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
103 | 102 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
104 | 99, 101, 103 | 3eqtrd 2817 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
105 | 88, 91, 104 | mvrladdd 10788 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
106 | 105 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((log‘𝑛) · (Λ‘𝑛))) |
107 | 20 | relogcld 24806 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
108 | 107 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
109 | 91, 108 | mulcomd 10398 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (log‘𝑛)) =
((log‘𝑛) ·
(Λ‘𝑛))) |
110 | 106, 109 | eqtr4d 2816 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((Λ‘𝑛) · (log‘𝑛))) |
111 | 82, 110 | sumeq12rdv 14845 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛))) |
112 | 7 | nn0cnd 11704 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℂ) |
113 | | pncan 10628 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
114 | 112, 93, 113 | sylancl 580 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) − 1) = (⌊‘𝑥)) |
115 | 114 | fveq2d 6450 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
116 | | chpfl 25328 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
117 | 1, 116 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
118 | 115, 117 | eqtrd 2813 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
119 | 118 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) =
((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥))) |
120 | 12, 4 | mulcomd 10398 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥)) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
121 | 119, 120 | eqtrd 2813 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
122 | | 0cn 10368 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
123 | 122 | mul01i 10566 |
. . . . . . . . . . . . 13
⊢ (0
· 0) = 0 |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (0 · 0) = 0) |
125 | 121, 124 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
(((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − 0)) |
126 | 37 | subid1d 10723 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − 0) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
127 | 125, 126 | eqtrd 2813 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
128 | 95 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘𝑛)) |
129 | 128 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
130 | 82, 129 | sumeq12rdv 14845 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
131 | 127, 130 | oveq12d 6940 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1)))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
132 | 78, 111, 131 | 3eqtr3d 2821 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
133 | 132 | oveq1d 6937 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
134 | 39, 41, 133 | 3eqtr4d 2823 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥)))) |
135 | 134 | oveq1d 6937 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
136 | | div23 11052 |
. . . . . . 7
⊢
(((ψ‘𝑥)
∈ ℂ ∧ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
137 | 4, 15, 34, 136 | syl3anc 1439 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
138 | 137 | oveq1d 6937 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
139 | 36, 135, 138 | 3eqtr3rd 2822 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥) /
𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
140 | 139 | mpteq2ia 4975 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((((ψ‘𝑥)
/ 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
141 | | ovexd 6956 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ V) |
142 | | ovexd 6956 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥) ∈ V) |
143 | | reex 10363 |
. . . . . . . 8
⊢ ℝ
∈ V |
144 | | rpssre 12144 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
145 | 143, 144 | ssexi 5040 |
. . . . . . 7
⊢
ℝ+ ∈ V |
146 | 145 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ+ ∈ V) |
147 | | ovexd 6956 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ V) |
148 | 15 | adantl 475 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℂ) |
149 | | eqidd 2778 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
150 | | eqidd 2778 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
151 | 146, 147,
148, 149, 150 | offval2 7191 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))) |
152 | | chpo1ub 25621 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
153 | | 0red 10380 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℝ) |
154 | | 1red 10377 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
155 | | divrcnv 14988 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
156 | 93, 155 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
157 | | rpreccl 12165 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
158 | 157 | rpred 12181 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) |
159 | 158 | adantl 475 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ ℝ) |
160 | 11, 13 | resubcld 10803 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℝ) |
161 | 160 | adantl 475 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℝ) |
162 | | rpaddcl 12161 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
163 | 21, 162 | mpan2 681 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 + 1) ∈
ℝ+) |
164 | 163 | relogcld 24806 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘(𝑥 + 1))
∈ ℝ) |
165 | 164, 13 | resubcld 10803 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥))
∈ ℝ) |
166 | 7 | nn0red 11703 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℝ) |
167 | | 1red 10377 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 1 ∈ ℝ) |
168 | | flle 12919 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
169 | 1, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
≤ 𝑥) |
170 | 166, 1, 167, 169 | leadd1dd 10989 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ≤ (𝑥 +
1)) |
171 | 10, 163 | logled 24810 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) ≤ (𝑥 + 1) ↔
(log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1)))) |
172 | 170, 171 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1))) |
173 | 11, 164, 13, 172 | lesub1dd 10991 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ ((log‘(𝑥 + 1)) − (log‘𝑥))) |
174 | | logdifbnd 25172 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥)) ≤
(1 / 𝑥)) |
175 | 160, 165,
158, 173, 174 | letrd 10533 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
176 | 175 | ad2antrl 718 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
177 | | fllep1 12921 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
178 | 1, 177 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≤
((⌊‘𝑥) +
1)) |
179 | | logleb 24786 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ ((⌊‘𝑥) +
1) ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
180 | 10, 179 | mpdan 677 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1)))) |
181 | 178, 180 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1))) |
182 | 11, 13 | subge0d 10965 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
183 | 181, 182 | mpbird 249 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
184 | 183 | ad2antrl 718 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
185 | 153, 154,
156, 159, 161, 176, 184 | rlimsqz2 14789 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟
0) |
186 | | rlimo1 14755 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟 0 →
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
187 | 185, 186 | syl 17 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
188 | | o1mul 14753 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥))
∘𝑓 · (𝑥 ∈ ℝ+ ↦
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
189 | 152, 187,
188 | sylancr 581 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
190 | 151, 189 | eqeltrrd 2859 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈
𝑂(1)) |
191 | | nnrp 12150 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
192 | 191 | ssriv 3824 |
. . . . . . . 8
⊢ ℕ
⊆ ℝ+ |
193 | 192 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℕ ⊆ ℝ+) |
194 | 193 | sselda 3820 |
. . . . . 6
⊢
((⊤ ∧ 𝑛
∈ ℕ) → 𝑛
∈ ℝ+) |
195 | 194, 31 | syl 17 |
. . . . 5
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
196 | | chpo1ub 25621 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
↦ ((ψ‘𝑛) /
𝑛)) ∈
𝑂(1) |
197 | 196 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ ((ψ‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
198 | | rerpdivcl 12169 |
. . . . . . . . 9
⊢
(((ψ‘𝑛)
∈ ℝ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
199 | 29, 198 | mpancom 678 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) ∈
ℝ) |
200 | 199 | adantl 475 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
201 | 31 | adantl 475 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
202 | | rpreccl 12165 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
203 | 202 | rpred 12181 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ) |
204 | | chpge0 25304 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → 0 ≤
(ψ‘𝑛)) |
205 | 27, 204 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (ψ‘𝑛)) |
206 | | logdifbnd 25172 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛)) ≤
(1 / 𝑛)) |
207 | 26, 203, 29, 205, 206 | lemul1ad 11317 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
≤ ((1 / 𝑛) ·
(ψ‘𝑛))) |
208 | 27 | lep1d 11309 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≤ (𝑛 + 1)) |
209 | | logleb 24786 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ+
∧ (𝑛 + 1) ∈
ℝ+) → (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
210 | 23, 209 | mpdan 677 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
211 | 208, 210 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ≤
(log‘(𝑛 +
1))) |
212 | 24, 25 | subge0d 10965 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛)) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
213 | 211, 212 | mpbird 249 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛))) |
214 | 26, 29, 213, 205 | mulge0d 10952 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
215 | 30, 214 | absidd 14569 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
216 | | rpregt0 12153 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) |
217 | | divge0 11246 |
. . . . . . . . . . . 12
⊢
((((ψ‘𝑛)
∈ ℝ ∧ 0 ≤ (ψ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤
((ψ‘𝑛) / 𝑛)) |
218 | 29, 205, 216, 217 | syl21anc 828 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((ψ‘𝑛) / 𝑛)) |
219 | 199, 218 | absidd 14569 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((ψ‘𝑛) / 𝑛)) |
220 | 29 | recnd 10405 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℂ) |
221 | | rpcn 12149 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℂ) |
222 | | rpne0 12155 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≠
0) |
223 | 220, 221,
222 | divrec2d 11155 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) = ((1 / 𝑛) · (ψ‘𝑛))) |
224 | 219, 223 | eqtrd 2813 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((1 / 𝑛) · (ψ‘𝑛))) |
225 | 207, 215,
224 | 3brtr4d 4918 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤ (abs‘((ψ‘𝑛) / 𝑛))) |
226 | 225 | ad2antrl 718 |
. . . . . . 7
⊢
((⊤ ∧ (𝑛
∈ ℝ+ ∧ 1 ≤ 𝑛)) → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤
(abs‘((ψ‘𝑛)
/ 𝑛))) |
227 | 154, 197,
200, 201, 226 | o1le 14791 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ∈ 𝑂(1)) |
228 | 193, 227 | o1res2 14702 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛)))
∈ 𝑂(1)) |
229 | 195, 228 | o1fsum 14949 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) |
230 | 141, 142,
190, 229 | o1sub2 14764 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) ∈ 𝑂(1)) |
231 | 140, 230 | syl5eqelr 2863 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)) |
232 | 231 | mptru 1609 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |