Proof of Theorem vmadivsum
Step | Hyp | Ref
| Expression |
1 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 4731 |
. . . . . 6
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
5 | | ovex 6577 |
. . . . . 6
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V |
6 | 5 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V) |
7 | | ovex 6577 |
. . . . . 6
⊢
((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V |
8 | 7 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V) |
9 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) |
10 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) |
11 | 4, 6, 8, 9, 10 | offval2 6812 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))))) |
12 | 11 | trud 1484 |
. . 3
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) |
13 | | fzfid 12634 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
14 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
16 | | vmacl 24644 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
18 | 17, 15 | nndivred 10946 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
19 | 13, 18 | fsumrecl 14312 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
20 | 19 | recnd 9947 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
21 | | relogcl 24126 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
22 | 21 | recnd 9947 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
23 | | rprege0 11723 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
24 | | flge0nn0 12483 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
25 | | faccl 12932 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ ℕ0 → (!‘(⌊‘𝑥)) ∈ ℕ) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (!‘(⌊‘𝑥)) ∈ ℕ) |
27 | 26 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (!‘(⌊‘𝑥)) ∈
ℝ+) |
28 | 27 | relogcld 24173 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘(!‘(⌊‘𝑥))) ∈ ℝ) |
29 | | rerpdivcl 11737 |
. . . . . . 7
⊢
(((log‘(!‘(⌊‘𝑥))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℝ) |
30 | 28, 29 | mpancom 700 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℂ) |
32 | 20, 22, 31 | nnncan2d 10306 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) |
33 | 32 | mpteq2ia 4668 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) |
34 | 12, 33 | eqtri 2632 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) |
35 | | 1red 9934 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℝ) |
36 | | chpo1ub 24969 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
37 | 36 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
38 | | rpre 11715 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
39 | | chpcl 24650 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
41 | | rerpdivcl 11737 |
. . . . . . . 8
⊢
(((ψ‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
42 | 40, 41 | mpancom 700 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℝ) |
43 | 42 | recnd 9947 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℂ) |
44 | 43 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℂ) |
45 | 20, 31 | subcld 10271 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ ℂ) |
46 | 45 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ ℂ) |
47 | 38 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
48 | 18, 47 | remulcld 9949 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · 𝑥) ∈
ℝ) |
49 | | nndivre 10933 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ) |
50 | 38, 14, 49 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
51 | | reflcl 12459 |
. . . . . . . . . . . . 13
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) |
53 | 17, 52 | remulcld 9949 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (⌊‘(𝑥
/ 𝑛))) ∈
ℝ) |
54 | 48, 53 | resubcld 10337 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ∈ ℝ) |
55 | 50, 52 | resubcld 10337 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℝ) |
56 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
57 | | vmage0 24647 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
58 | 15, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
59 | | fracle1 12466 |
. . . . . . . . . . . . 13
⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
60 | 50, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
61 | 55, 56, 17, 58, 60 | lemul2ad 10843 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) · 1)) |
62 | 17 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
63 | 50 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
64 | 52 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) |
65 | 62, 63, 64 | subdid 10365 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = (((Λ‘𝑛) · (𝑥 / 𝑛)) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
66 | | rpcn 11717 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
68 | 15 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
69 | | rpcnne0 11726 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
71 | | div23 10583 |
. . . . . . . . . . . . . . 15
⊢
(((Λ‘𝑛)
∈ ℂ ∧ 𝑥
∈ ℂ ∧ (𝑛
∈ ℂ ∧ 𝑛 ≠
0)) → (((Λ‘𝑛) · 𝑥) / 𝑛) = (((Λ‘𝑛) / 𝑛) · 𝑥)) |
72 | | divass 10582 |
. . . . . . . . . . . . . . 15
⊢
(((Λ‘𝑛)
∈ ℂ ∧ 𝑥
∈ ℂ ∧ (𝑛
∈ ℂ ∧ 𝑛 ≠
0)) → (((Λ‘𝑛) · 𝑥) / 𝑛) = ((Λ‘𝑛) · (𝑥 / 𝑛))) |
73 | 71, 72 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢
(((Λ‘𝑛)
∈ ℂ ∧ 𝑥
∈ ℂ ∧ (𝑛
∈ ℂ ∧ 𝑛 ≠
0)) → (((Λ‘𝑛) / 𝑛) · 𝑥) = ((Λ‘𝑛) · (𝑥 / 𝑛))) |
74 | 62, 67, 70, 73 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · 𝑥) = ((Λ‘𝑛) · (𝑥 / 𝑛))) |
75 | 74 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) = (((Λ‘𝑛) · (𝑥 / 𝑛)) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
76 | 65, 75 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
77 | 62 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· 1) = (Λ‘𝑛)) |
78 | 61, 76, 77 | 3brtr3d 4614 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ≤ (Λ‘𝑛)) |
79 | 13, 54, 17, 78 | fsumle 14372 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)) |
80 | 18 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
81 | 13, 66, 80 | fsummulc1 14359 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥)) |
82 | | logfac2 24742 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(log‘(!‘(⌊‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) |
83 | 23, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘(!‘(⌊‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) |
84 | 81, 83 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
85 | 48 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · 𝑥) ∈
ℂ) |
86 | 53 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (⌊‘(𝑥
/ 𝑛))) ∈
ℂ) |
87 | 13, 85, 86 | fsumsub 14362 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
88 | 84, 87 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
89 | | chpval 24648 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) =
Σ𝑛 ∈
(1...(⌊‘𝑥))(Λ‘𝑛)) |
90 | 38, 89 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥) =
Σ𝑛 ∈
(1...(⌊‘𝑥))(Λ‘𝑛)) |
91 | 79, 88, 90 | 3brtr4d 4615 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥)) |
92 | 19, 38 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℝ) |
93 | 92, 28 | resubcld 10337 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ∈ ℝ) |
94 | | rpregt0 11722 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
95 | | lediv1 10767 |
. . . . . . . . 9
⊢
((((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ (ψ‘𝑥) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 <
𝑥)) → (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥) ↔ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥))) |
96 | 93, 40, 94, 95 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥) ↔ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥))) |
97 | 91, 96 | mpbid 221 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥)) |
98 | 92 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℂ) |
99 | 28 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘(!‘(⌊‘𝑥))) ∈ ℂ) |
100 | | rpcnne0 11726 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
101 | | divsubdir 10600 |
. . . . . . . . . . 11
⊢
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℂ ∧
(log‘(!‘(⌊‘𝑥))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) |
102 | 98, 99, 100, 101 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) |
103 | | rpne0 11724 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
104 | 20, 66, 103 | divcan4d 10686 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
105 | 104 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) |
106 | 102, 105 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) |
107 | 106 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (abs‘(Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥))) |
108 | | rerpdivcl 11737 |
. . . . . . . . . 10
⊢
((((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) ∈ ℝ) |
109 | 93, 108 | mpancom 700 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥) ∈ ℝ) |
110 | | flle 12462 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛)) |
111 | 50, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ≤ (𝑥 / 𝑛)) |
112 | 50, 52 | subge0d 10496 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 ≤ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ↔ (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))) |
113 | 111, 112 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) |
114 | 17, 55, 58, 113 | mulge0d 10483 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) · ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))) |
115 | 114, 76 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
116 | 13, 54, 115 | fsumge0 14368 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ Σ𝑛
∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))) |
117 | 116, 88 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ ((Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥))))) |
118 | | divge0 10771 |
. . . . . . . . . 10
⊢
(((((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ 0 ≤
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥))))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ (((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) |
119 | 93, 117, 94, 118 | syl21anc 1317 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ (((Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) |
120 | 109, 119 | absidd 14009 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) |
121 | 107, 120 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (abs‘(Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) −
(log‘(!‘(⌊‘𝑥)))) / 𝑥)) |
122 | | chpge0 24652 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
123 | 38, 122 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ (ψ‘𝑥)) |
124 | | divge0 10771 |
. . . . . . . . 9
⊢
((((ψ‘𝑥)
∈ ℝ ∧ 0 ≤ (ψ‘𝑥)) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤
((ψ‘𝑥) / 𝑥)) |
125 | 40, 123, 94, 124 | syl21anc 1317 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ ((ψ‘𝑥) / 𝑥)) |
126 | 42, 125 | absidd 14009 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (abs‘((ψ‘𝑥) / 𝑥)) = ((ψ‘𝑥) / 𝑥)) |
127 | 97, 121, 126 | 3brtr4d 4615 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (abs‘(Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ≤ (abs‘((ψ‘𝑥) / 𝑥))) |
128 | 127 | ad2antrl 760 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ≤ (abs‘((ψ‘𝑥) / 𝑥))) |
129 | 35, 37, 44, 46, 128 | o1le 14231 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)) |
130 | 129 | trud 1484 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1) |
131 | | logfacrlim 24749 |
. . . 4
⊢ (𝑥 ∈ ℝ+
↦ ((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟
1 |
132 | | rlimo1 14195 |
. . . 4
⊢ ((𝑥 ∈ ℝ+
↦ ((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝𝑟 1 →
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)) |
133 | 131, 132 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1) |
134 | | o1sub 14194 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ ((log‘𝑥)
− ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) ∈ 𝑂(1)) |
135 | 130, 133,
134 | mp2an 704 |
. 2
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) −
((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ ((log‘𝑥) −
((log‘(!‘(⌊‘𝑥))) / 𝑥)))) ∈ 𝑂(1) |
136 | 34, 135 | eqeltrri 2685 |
1
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |