Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
2 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
3 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
4 | 3 | nnrpd 11746 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
5 | | rpdivcl 11732 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
6 | 2, 4, 5 | syl2an 493 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
7 | 6 | relogcld 24173 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
8 | | simpll 786 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) |
9 | 7, 8 | reexpcld 12887 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
10 | 1, 9 | fsumrecl 14312 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
11 | | relogcl 24126 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
12 | | id 22 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
13 | | reexpcl 12739 |
. . . . . . 7
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑁
∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
14 | 11, 12, 13 | syl2anr 494 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
15 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℕ) |
17 | 16 | nnred 10912 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℝ) |
18 | | fzfid 12634 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (0...𝑁) ∈ Fin) |
19 | 11 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (log‘𝑥) ∈ ℝ) |
20 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
21 | | reexpcl 12739 |
. . . . . . . . . 10
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
22 | 19, 20, 21 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
23 | 20 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
24 | | faccl 12932 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
26 | 22, 25 | nndivred 10946 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
27 | 18, 26 | fsumrecl 14312 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
28 | 17, 27 | remulcld 9949 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ) |
29 | 14, 28 | resubcld 10337 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ) |
30 | 10, 29 | resubcld 10337 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ) |
31 | 30, 2 | rerpdivcld 11779 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ) |
32 | | rerpdivcl 11737 |
. . . 4
⊢
(((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) |
33 | 29, 32 | sylancom 698 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) |
34 | | 1red 9934 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) |
35 | 15 | nncnd 10913 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
36 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → 𝑘 = 𝑁) |
37 | 36 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁)) |
38 | 37 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥)) |
39 | 38 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑁) / 𝑥))) |
40 | 39 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔
(𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0)) |
41 | 11 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
42 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) |
43 | | cxpexp 24214 |
. . . . . . . . 9
⊢
(((log‘𝑥)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) |
44 | 41, 42, 43 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) |
45 | | rpcn 11717 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
46 | 45 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
47 | 46 | cxp1d 24252 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝑐1) = 𝑥) |
48 | 44, 47 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)) =
(((log‘𝑥)↑𝑘) / 𝑥)) |
49 | 48 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+
↦ (((log‘𝑥)↑𝑘) / 𝑥))) |
50 | | nn0cn 11179 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
51 | | 1rp 11712 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
52 | | cxploglim2 24505 |
. . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℝ+) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) |
53 | 50, 51, 52 | sylancl 693 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) |
54 | 49, 53 | eqbrtrrd 4607 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) |
55 | 40, 54 | vtoclga 3245 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0) |
56 | | rerpdivcl 11737 |
. . . . . 6
⊢
((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
57 | 14, 56 | sylancom 698 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
58 | 57 | recnd 9947 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
59 | 10 | recnd 9947 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) |
60 | 14 | recnd 9947 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
61 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℂ) |
62 | 27 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
63 | 61, 62 | mulcld 9939 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) |
64 | 60, 63 | subcld 10271 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) |
65 | 59, 64 | subcld 10271 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ) |
66 | | rpcnne0 11726 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
67 | 66 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
68 | 67 | simpld 474 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
69 | 67 | simprd 478 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ≠ 0) |
70 | 65, 68, 69 | divcld 10680 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) |
71 | 70 | adantrr 749 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) |
72 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ) |
73 | 72 | nncnd 10913 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ) |
74 | 71, 73 | subcld 10271 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ) |
75 | 74 | abscld 14023 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ) |
76 | 57 | adantrr 749 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
77 | 76 | recnd 9947 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
78 | 77 | abscld 14023 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ) |
79 | | ioorp 12122 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
80 | 79 | eqcomi 2619 |
. . . . . . . . 9
⊢
ℝ+ = (0(,)+∞) |
81 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
82 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
83 | 82 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ) |
84 | | 1red 9934 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ) |
85 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
86 | | 1nn0 11185 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
87 | 85, 86 | nn0addge1i 11218 |
. . . . . . . . . 10
⊢ 1 ≤ (1
+ 1) |
88 | 87 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1)) |
89 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ) |
90 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) |
91 | 90 | nnred 10912 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℝ) |
92 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
93 | 92 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
94 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(0...𝑁) ∈
Fin) |
95 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
96 | | rpdivcl 11732 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) |
97 | 95, 96 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) |
98 | 97 | relogcld 24173 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(log‘(𝑥 / 𝑦)) ∈
ℝ) |
99 | | reexpcl 12739 |
. . . . . . . . . . . . . 14
⊢
(((log‘(𝑥 /
𝑦)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) |
100 | 98, 20, 99 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) |
101 | 20 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
102 | 101, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
103 | 100, 102 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
104 | 94, 103 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
105 | 93, 104 | remulcld 9949 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ) |
106 | 91, 105 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ) |
107 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈
ℕ0) |
108 | 98, 107 | reexpcld 12887 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) |
109 | | nnrp 11718 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
110 | 109, 108 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) |
111 | | reelprrecn 9907 |
. . . . . . . . . . . 12
⊢ ℝ
∈ {ℝ, ℂ} |
112 | 111 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ,
ℂ}) |
113 | 105 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
114 | 108, 90 | nndivred 10946 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ) |
115 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
116 | | advlogexp 24201 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) |
117 | 95, 115, 116 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) |
118 | 112, 113,
114, 117, 73 | dvmptcmul 23533 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))) |
119 | 108 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ) |
120 | 73 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℂ) |
121 | 72 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0) |
122 | 121 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ≠
0) |
123 | 119, 120,
122 | divcan2d 10682 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁)) |
124 | 123 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) |
125 | 118, 124 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) |
126 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛)) |
127 | 126 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛))) |
128 | 127 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁)) |
129 | 95 | rpxrd 11749 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*) |
130 | | simp1rl 1119 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
131 | | simp2r 1081 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+) |
132 | 130, 131 | rpdivcld 11765 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ∈
ℝ+) |
133 | 132 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
134 | | simp2l 1080 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ∈ ℝ+) |
135 | 130, 134 | rpdivcld 11765 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) |
136 | 135 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) |
137 | | simp1l 1078 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
138 | | log1 24136 |
. . . . . . . . . . 11
⊢
(log‘1) = 0 |
139 | 131 | rpcnd 11750 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℂ) |
140 | 139 | mulid2d 9937 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) = 𝑛) |
141 | | simp33 1092 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
142 | 140, 141 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) ≤ 𝑥) |
143 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ∈ ℝ) |
144 | 130 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
145 | 143, 144,
131 | lemuldivd 11797 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
146 | 142, 145 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑛)) |
147 | | logleb 24153 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) |
148 | 51, 132, 147 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) |
149 | 146, 148 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑛))) |
150 | 138, 149 | syl5eqbrr 4619 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛))) |
151 | | simp32 1091 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ≤ 𝑛) |
152 | 134, 131,
130 | lediv2d 11772 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑦 ≤ 𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))) |
153 | 151, 152 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)) |
154 | 132, 135 | logled 24177 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) |
155 | 153, 154 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))) |
156 | | leexp1a 12781 |
. . . . . . . . . 10
⊢
((((log‘(𝑥 /
𝑛)) ∈ ℝ ∧
(log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ (log‘(𝑥
/ 𝑛)) ∧
(log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
157 | 133, 136,
137, 150, 155, 156 | syl32anc 1326 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
158 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) |
159 | 97 | 3ad2antr1 1219 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) |
160 | 159 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) |
161 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
162 | | rpcn 11717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
163 | 162 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) |
164 | 163 | 3ad2antr1 1219 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℂ) |
165 | 164 | mulid2d 9937 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) = 𝑦) |
166 | | simpr3 1062 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ≤ 𝑥) |
167 | 165, 166 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) ≤ 𝑥) |
168 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ∈ ℝ) |
169 | 95 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
170 | 169 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
171 | | simpr1 1060 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℝ+) |
172 | 168, 170,
171 | lemuldivd 11797 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦))) |
173 | 167, 172 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑦)) |
174 | | logleb 24153 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) |
175 | 51, 159, 174 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) |
176 | 173, 175 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑦))) |
177 | 138, 176 | syl5eqbrr 4619 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦))) |
178 | 160, 161,
177 | expge0d 12888 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
179 | 51 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈
ℝ+) |
180 | | 1le1 10534 |
. . . . . . . . . 10
⊢ 1 ≤
1 |
181 | 180 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1) |
182 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
183 | 169 | leidd 10473 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≤ 𝑥) |
184 | 80, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183 | dvfsumlem4 23596 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ ⦋1 /
𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁)) |
185 | | fzfid 12634 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
186 | 95, 4, 5 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
187 | 186 | relogcld 24173 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
188 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) |
189 | 187, 188 | reexpcld 12887 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
190 | 185, 189 | fsumrecl 14312 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
191 | 190 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) |
192 | 95 | rpcnd 11750 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ) |
193 | 73, 192 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ) |
194 | 11 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ) |
195 | 194 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ) |
196 | 195, 115 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
197 | | fzfid 12634 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin) |
198 | 194, 20, 21 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
199 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
200 | 199, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
201 | 198, 200 | nndivred 10946 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
202 | 201 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
203 | 197, 202 | fsumcl 14311 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
204 | 73, 203 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) |
205 | 196, 204 | subcld 10271 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) |
206 | 191, 193,
205 | sub32d 10303 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
207 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))) |
208 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
209 | 208 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥)) |
210 | 209 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥))) |
211 | 210 | sumeq1d 14279 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁)) |
212 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥)) |
213 | 66 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
214 | | divid 10593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1) |
216 | 212, 215 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1) |
217 | 216 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1) |
218 | 217 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1)) |
219 | 218, 138 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0) |
220 | 219 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘)) |
221 | 220 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘))) |
222 | 221 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) |
223 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 = (ℤ≥‘0) |
224 | 115, 223 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
(ℤ≥‘0)) |
225 | | eluzfz1 12219 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁)) |
227 | 226 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁)) |
228 | 227 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁)) |
229 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ {0} → 𝑘 = 0) |
230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0) |
231 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) |
232 | | 0exp0e1 12727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0↑0) = 1 |
233 | 231, 232 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (0↑𝑘) = 1) |
234 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
235 | | fac0 12925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(!‘0) = 1 |
236 | 234, 235 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
237 | 233, 236 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1)) |
238 | | 1div1e1 10596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 / 1) =
1 |
239 | 237, 238 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1) |
240 | 230, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1) |
241 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
242 | 240, 241 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ) |
243 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁)) |
244 | 243 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁)) |
245 | 244, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0) |
246 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0) |
247 | 246 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0) |
248 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (ℕ0
∖ {0}) ↔ (𝑘
∈ ℕ0 ∧ 𝑘 ≠ 0)) |
249 | 245, 247,
248 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖
{0})) |
250 | | dfn2 11182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℕ0 ∖ {0}) |
251 | 249, 250 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ) |
252 | 251 | 0expd 12886 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0) |
253 | 252 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘))) |
254 | 245, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℕ) |
255 | 254 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℂ) |
256 | 254 | nnne0d 10942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0) |
257 | 255, 256 | div0d 10679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0) |
258 | 253, 257 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0) |
259 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin) |
260 | 228, 242,
258, 259 | fsumss 14303 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) |
261 | 222, 260 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘))) |
262 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
263 | 239 | sumsn 14319 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1) |
264 | 262, 241,
263 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑘 ∈ {0}
((0↑𝑘) /
(!‘𝑘)) =
1 |
265 | 261, 264 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1) |
266 | 208, 265 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1)) |
267 | 192 | mulid1d 9936 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥) |
268 | 267 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥) |
269 | 266, 268 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥) |
270 | 269 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥)) |
271 | 211, 270 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) |
272 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V |
273 | 272 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V) |
274 | 207, 271,
95, 273 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) |
275 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1) |
276 | 275 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) =
(⌊‘1)) |
277 | | flid 12471 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
278 | 82, 277 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(⌊‘1) = 1 |
279 | 276, 278 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1) |
280 | 279 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1)) |
281 | 280 | sumeq1d 14279 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁)) |
282 | 192 | div1d 10672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥) |
283 | 282 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥) |
284 | 283 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥)) |
285 | 284 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁)) |
286 | 196 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
287 | 285, 286 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) |
288 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1)) |
289 | 288 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1))) |
290 | 289 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
291 | 290 | fsum1 14320 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈
(1...1)((log‘(𝑥 /
𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
292 | 82, 287, 291 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
293 | 281, 292,
285 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁)) |
294 | 275 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1)) |
295 | 294, 283 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥) |
296 | 295 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) |
297 | 296 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) |
298 | 297 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘)) |
299 | 298 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘))) |
300 | 299 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
301 | 275, 300 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) |
302 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
303 | 302 | mulid2d 9937 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
304 | 301, 303 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
305 | 304 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) |
306 | 293, 305 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) |
307 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V |
308 | 307 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V) |
309 | 207, 306,
179, 308 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) |
310 | 274, 309 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) |
311 | 71, 73, 192 | subdird 10366 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥))) |
312 | 65 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ) |
313 | 213 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0) |
314 | 312, 192,
313 | divcan1d 10681 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) |
315 | 314 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
316 | 311, 315 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
317 | 206, 310,
316 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) |
318 | 317 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
(abs‘((((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))) |
319 | 74, 192 | absmuld 14041 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥))) |
320 | | rprege0 11723 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
321 | 320 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
322 | | absid 13884 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
323 | 321, 322 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥) |
324 | 323 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) |
325 | 318, 319,
324 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
((abs‘(((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) |
326 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ) |
327 | 296 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) |
328 | 326, 327 | csbied 3526 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) |
329 | 184, 325,
328 | 3brtr3d 4614 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁)) |
330 | 14 | adantrr 749 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
331 | 75, 330, 95 | lemuldivd 11797 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))) |
332 | 329, 331 | mpbid 221 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)) |
333 | 76 | leabsd 14001 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
334 | 75, 76, 78, 332, 333 | letrd 10073 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
335 | 58 | adantrr 749 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
336 | 335 | subid1d 10260 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥)) |
337 | 336 | fveq2d 6107 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
338 | 334, 337 | breqtrrd 4611 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0))) |
339 | 34, 35, 55, 58, 70, 338 | rlimsqzlem 14227 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁)) |
340 | | divsubdir 10600 |
. . . . . 6
⊢
((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) |
341 | 60, 63, 67, 340 | syl3anc 1318 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) |
342 | 341 | mpteq2dva 4672 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))) |
343 | | rerpdivcl 11737 |
. . . . . . 7
⊢
((((!‘𝑁)
· Σ𝑘 ∈
(0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) |
344 | 28, 343 | sylancom 698 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) |
345 | | divass 10582 |
. . . . . . . . . 10
⊢
(((!‘𝑁) ∈
ℂ ∧ Σ𝑘
∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) |
346 | 61, 62, 67, 345 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) |
347 | 26 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
348 | 18, 68, 347, 69 | fsumdivc 14360 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) |
349 | 22 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ) |
350 | 25 | nnrpd 11746 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ+) |
351 | 350 | rpcnne0d 11757 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0)) |
352 | 67 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
353 | | divdiv32 10612 |
. . . . . . . . . . . . 13
⊢
((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧
(!‘𝑘) ≠ 0) ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) →
((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
354 | 349, 351,
352, 353 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
355 | 354 | sumeq2dv 14281 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
356 | 348, 355 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
357 | 356 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) |
358 | 346, 357 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) |
359 | 358 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))) |
360 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+) |
361 | 22, 360 | rerpdivcld 11779 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) |
362 | 361, 25 | nndivred 10946 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
363 | 18, 362 | fsumrecl 14312 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
364 | | rpssre 11719 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
365 | | rlimconst 14123 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑁))
⇝𝑟 (!‘𝑁)) |
366 | 364, 35, 365 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (!‘𝑁)) ⇝𝑟
(!‘𝑁)) |
367 | 364 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ℝ+ ⊆ ℝ) |
368 | | fzfid 12634 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) ∈
Fin) |
369 | 362 | anasss 677 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 𝑘
∈ (0...𝑁))) →
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
370 | 361 | an32s 842 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) |
371 | 20 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
372 | 371, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℕ) |
373 | 372 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ) |
374 | 373 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ∈
ℝ) |
375 | 371, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) |
376 | 372 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℂ) |
377 | | rlimconst 14123 |
. . . . . . . . . . . . . 14
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) |
378 | 364, 376,
377 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) |
379 | 372 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) |
380 | 379 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ≠
0) |
381 | 370, 374,
375, 378, 379, 380 | rlimdiv 14224 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 /
(!‘𝑘))) |
382 | 376, 379 | div0d 10679 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0) |
383 | 381, 382 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) |
384 | 367, 368,
369, 383 | fsumrlim 14384 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0) |
385 | | fzfi 12633 |
. . . . . . . . . . . 12
⊢
(0...𝑁) ∈
Fin |
386 | 385 | olci 405 |
. . . . . . . . . . 11
⊢
((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) |
387 | | sumz 14300 |
. . . . . . . . . . 11
⊢
(((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0) |
388 | 386, 387 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)0 =
0 |
389 | 384, 388 | syl6breq 4624 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) |
390 | 17, 363, 366, 389 | rlimmul 14223 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
((!‘𝑁) ·
0)) |
391 | 35 | mul01d 10114 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 0) = 0) |
392 | 390, 391 | breqtrd 4609 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
0) |
393 | 359, 392 | eqbrtrd 4605 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟
0) |
394 | 57, 344, 55, 393 | rlimsub 14222 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 −
0)) |
395 | | 0m0e0 11007 |
. . . . 5
⊢ (0
− 0) = 0 |
396 | 394, 395 | syl6breq 4624 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟
0) |
397 | 342, 396 | eqbrtrd 4605 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟
0) |
398 | 31, 33, 339, 397 | rlimadd 14221 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟
((!‘𝑁) +
0)) |
399 | | divsubdir 10600 |
. . . . . 6
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
400 | 59, 64, 67, 399 | syl3anc 1318 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
401 | 400 | oveq1d 6564 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
402 | 10, 2 | rerpdivcld 11779 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ) |
403 | 402 | recnd 9947 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ) |
404 | 33 | recnd 9947 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ) |
405 | 403, 404 | npcand 10275 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) |
406 | 401, 405 | eqtrd 2644 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) |
407 | 406 | mpteq2dva 4672 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))) |
408 | 35 | addid1d 10115 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁) + 0) =
(!‘𝑁)) |
409 | 398, 407,
408 | 3brtr3d 4614 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁)) |