Step | Hyp | Ref
| Expression |
1 | | fzfid 13433 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
2 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
3 | | elfznn 13028 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
4 | 3 | nnrpd 12513 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
5 | | rpdivcl 12498 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
6 | 2, 4, 5 | syl2an 599 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
7 | 6 | relogcld 25366 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
8 | | simpll 767 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) |
9 | 7, 8 | reexpcld 13620 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
10 | 1, 9 | fsumrecl 15185 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
11 | | relogcl 25319 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
12 | | id 22 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
13 | | reexpcl 13539 |
. . . . . . 7
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑁
∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
14 | 11, 12, 13 | syl2anr 600 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
15 | | faccl 13736 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
16 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℕ) |
17 | 16 | nnred 11732 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℝ) |
18 | | fzfid 13433 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (0...𝑁) ∈ Fin) |
19 | 11 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (log‘𝑥) ∈ ℝ) |
20 | | elfznn0 13092 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
21 | | reexpcl 13539 |
. . . . . . . . . 10
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
22 | 19, 20, 21 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
23 | 20 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
24 | 23 | faccld 13737 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
25 | 22, 24 | nndivred 11771 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
26 | 18, 25 | fsumrecl 15185 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
27 | 17, 26 | remulcld 10750 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ) |
28 | 14, 27 | resubcld 11147 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ) |
29 | 10, 28 | resubcld 11147 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ) |
30 | 29, 2 | rerpdivcld 12546 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ) |
31 | | rerpdivcl 12503 |
. . . 4
⊢
(((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) |
32 | 28, 31 | sylancom 591 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) |
33 | | 1red 10721 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) |
34 | 15 | nncnd 11733 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
35 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → 𝑘 = 𝑁) |
36 | 35 | oveq2d 7187 |
. . . . . . . 8
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁)) |
37 | 36 | oveq1d 7186 |
. . . . . . 7
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥)) |
38 | 37 | mpteq2dva 5126 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑁) / 𝑥))) |
39 | 38 | breq1d 5041 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔
(𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0)) |
40 | 11 | recnd 10748 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
41 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) |
42 | | cxpexp 25411 |
. . . . . . . . 9
⊢
(((log‘𝑥)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) |
43 | 40, 41, 42 | syl2anr 600 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) |
44 | | rpcn 12483 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
45 | 44 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
46 | 45 | cxp1d 25449 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝑐1) = 𝑥) |
47 | 43, 46 | oveq12d 7189 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)) =
(((log‘𝑥)↑𝑘) / 𝑥)) |
48 | 47 | mpteq2dva 5126 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+
↦ (((log‘𝑥)↑𝑘) / 𝑥))) |
49 | | nn0cn 11987 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
50 | | 1rp 12477 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
51 | | cxploglim2 25716 |
. . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℝ+) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) |
52 | 49, 50, 51 | sylancl 589 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) |
53 | 48, 52 | eqbrtrrd 5055 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) |
54 | 39, 53 | vtoclga 3479 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0) |
55 | | rerpdivcl 12503 |
. . . . . 6
⊢
((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
56 | 14, 55 | sylancom 591 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
57 | 56 | recnd 10748 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
58 | 10 | recnd 10748 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) |
59 | 14 | recnd 10748 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
60 | 34 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℂ) |
61 | 26 | recnd 10748 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
62 | 60, 61 | mulcld 10740 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) |
63 | 59, 62 | subcld 11076 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) |
64 | 58, 63 | subcld 11076 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ) |
65 | | rpcnne0 12491 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
66 | 65 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
67 | 66 | simpld 498 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) |
68 | 66 | simprd 499 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ≠ 0) |
69 | 64, 67, 68 | divcld 11495 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) |
70 | 69 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) |
71 | 15 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ) |
72 | 71 | nncnd 11733 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ) |
73 | 70, 72 | subcld 11076 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ) |
74 | 73 | abscld 14887 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ) |
75 | 56 | adantrr 717 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) |
76 | 75 | recnd 10748 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
77 | 76 | abscld 14887 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ) |
78 | | ioorp 12900 |
. . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ |
79 | 78 | eqcomi 2747 |
. . . . . . . . 9
⊢
ℝ+ = (0(,)+∞) |
80 | | nnuz 12364 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
81 | | 1z 12094 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
82 | 81 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ) |
83 | | 1red 10721 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ) |
84 | | 1re 10720 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
85 | | 1nn0 11993 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
86 | 84, 85 | nn0addge1i 12025 |
. . . . . . . . . 10
⊢ 1 ≤ (1
+ 1) |
87 | 86 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1)) |
88 | | 0red 10723 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ) |
89 | 71 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) |
90 | 89 | nnred 11732 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℝ) |
91 | | rpre 12481 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
92 | 91 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
93 | | fzfid 13433 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(0...𝑁) ∈
Fin) |
94 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
95 | | rpdivcl 12498 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) |
96 | 94, 95 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) |
97 | 96 | relogcld 25366 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(log‘(𝑥 / 𝑦)) ∈
ℝ) |
98 | | reexpcl 13539 |
. . . . . . . . . . . . . 14
⊢
(((log‘(𝑥 /
𝑦)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) |
99 | 97, 20, 98 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) |
100 | 20 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
101 | 100 | faccld 13737 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
102 | 99, 101 | nndivred 11771 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
103 | 93, 102 | fsumrecl 15185 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
104 | 92, 103 | remulcld 10750 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ) |
105 | 90, 104 | remulcld 10750 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ) |
106 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈
ℕ0) |
107 | 97, 106 | reexpcld 13620 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) |
108 | | nnrp 12484 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
109 | 108, 107 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) |
110 | | reelprrecn 10708 |
. . . . . . . . . . . 12
⊢ ℝ
∈ {ℝ, ℂ} |
111 | 110 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ,
ℂ}) |
112 | 104 | recnd 10748 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
113 | 107, 89 | nndivred 11771 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ) |
114 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
115 | | advlogexp 25398 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) |
116 | 94, 114, 115 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) |
117 | 111, 112,
113, 116, 72 | dvmptcmul 24716 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))) |
118 | 107 | recnd 10748 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ) |
119 | 72 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℂ) |
120 | 71 | nnne0d 11767 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0) |
121 | 120 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ≠
0) |
122 | 118, 119,
121 | divcan2d 11497 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁)) |
123 | 122 | mpteq2dva 5126 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) |
124 | 117, 123 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) |
125 | | oveq2 7179 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛)) |
126 | 125 | fveq2d 6679 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛))) |
127 | 126 | oveq1d 7186 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁)) |
128 | 94 | rpxrd 12516 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*) |
129 | | simp1rl 1239 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
130 | | simp2r 1201 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+) |
131 | 129, 130 | rpdivcld 12532 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ∈
ℝ+) |
132 | 131 | relogcld 25366 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
133 | | simp2l 1200 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ∈ ℝ+) |
134 | 129, 133 | rpdivcld 12532 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) |
135 | 134 | relogcld 25366 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) |
136 | | simp1l 1198 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
137 | | log1 25329 |
. . . . . . . . . . 11
⊢
(log‘1) = 0 |
138 | 130 | rpcnd 12517 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℂ) |
139 | 138 | mulid2d 10738 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) = 𝑛) |
140 | | simp33 1212 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
141 | 139, 140 | eqbrtrd 5053 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) ≤ 𝑥) |
142 | | 1red 10721 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ∈ ℝ) |
143 | 129 | rpred 12515 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
144 | 142, 143,
130 | lemuldivd 12564 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
145 | 141, 144 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑛)) |
146 | | logleb 25346 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) |
147 | 50, 131, 146 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) |
148 | 145, 147 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑛))) |
149 | 137, 148 | eqbrtrrid 5067 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛))) |
150 | | simp32 1211 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ≤ 𝑛) |
151 | 133, 130,
129 | lediv2d 12539 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑦 ≤ 𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))) |
152 | 150, 151 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)) |
153 | 131, 134 | logled 25370 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) |
154 | 152, 153 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))) |
155 | | leexp1a 13632 |
. . . . . . . . . 10
⊢
((((log‘(𝑥 /
𝑛)) ∈ ℝ ∧
(log‘(𝑥 / 𝑦)) ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ (log‘(𝑥
/ 𝑛)) ∧
(log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
156 | 132, 135,
136, 149, 154, 155 | syl32anc 1379 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((log‘(𝑥 / 𝑛))↑𝑁) ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
157 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) |
158 | 96 | 3ad2antr1 1189 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) |
159 | 158 | relogcld 25366 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) |
160 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑁 ∈
ℕ0) |
161 | | rpcn 12483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
162 | 161 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) |
163 | 162 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℂ) |
164 | 163 | mulid2d 10738 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) = 𝑦) |
165 | | simpr3 1197 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ≤ 𝑥) |
166 | 164, 165 | eqbrtrd 5053 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) ≤ 𝑥) |
167 | | 1red 10721 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ∈ ℝ) |
168 | 94 | rpred 12515 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
169 | 168 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
170 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℝ+) |
171 | 167, 169,
170 | lemuldivd 12564 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦))) |
172 | 166, 171 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑦)) |
173 | | logleb 25346 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) |
174 | 50, 158, 173 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) |
175 | 172, 174 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑦))) |
176 | 137, 175 | eqbrtrrid 5067 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦))) |
177 | 159, 160,
176 | expge0d 13621 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) |
178 | 50 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈
ℝ+) |
179 | | 1le1 11347 |
. . . . . . . . . 10
⊢ 1 ≤
1 |
180 | 179 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1) |
181 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
182 | 168 | leidd 11285 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≤ 𝑥) |
183 | 79, 80, 82, 83, 87, 88, 105, 107, 109, 124, 127, 128, 156, 157, 177, 178, 94, 180, 181, 182 | dvfsumlem4 24781 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ ⦋1 /
𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁)) |
184 | | fzfid 13433 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
185 | 94, 4, 5 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
186 | 185 | relogcld 25366 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
187 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) |
188 | 186, 187 | reexpcld 13620 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
189 | 184, 188 | fsumrecl 15185 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) |
190 | 189 | recnd 10748 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) |
191 | 94 | rpcnd 12517 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ) |
192 | 72, 191 | mulcld 10740 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ) |
193 | 11 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ) |
194 | 193 | recnd 10748 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ) |
195 | 194, 114 | expcld 13603 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
196 | | fzfid 13433 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin) |
197 | 193, 20, 21 | syl2an 599 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) |
198 | 20 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
199 | 198 | faccld 13737 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
200 | 197, 199 | nndivred 11771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
201 | 200 | recnd 10748 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
202 | 196, 201 | fsumcl 15184 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
203 | 72, 202 | mulcld 10740 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) |
204 | 195, 203 | subcld 11076 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) |
205 | 190, 192,
204 | sub32d 11108 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
206 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))) |
207 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
208 | 207 | fveq2d 6679 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥)) |
209 | 208 | oveq2d 7187 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥))) |
210 | 209 | sumeq1d 15152 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁)) |
211 | | oveq2 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥)) |
212 | 65 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
213 | | divid 11406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1) |
215 | 211, 214 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1) |
216 | 215 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1) |
217 | 216 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1)) |
218 | 217, 137 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0) |
219 | 218 | oveq1d 7186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘)) |
220 | 219 | oveq1d 7186 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘))) |
221 | 220 | sumeq2dv 15154 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) |
222 | | nn0uz 12363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 = (ℤ≥‘0) |
223 | 114, 222 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
(ℤ≥‘0)) |
224 | | eluzfz1 13006 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
225 | 223, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁)) |
226 | 225 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁)) |
227 | 226 | snssd 4698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁)) |
228 | | elsni 4534 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ {0} → 𝑘 = 0) |
229 | 228 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0) |
230 | | oveq2 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) |
231 | | 0exp0e1 13527 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0↑0) = 1 |
232 | 230, 231 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (0↑𝑘) = 1) |
233 | | fveq2 6675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
234 | | fac0 13729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(!‘0) = 1 |
235 | 233, 234 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
236 | 232, 235 | oveq12d 7189 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1)) |
237 | | 1div1e1 11409 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 / 1) =
1 |
238 | 236, 237 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1) |
239 | 229, 238 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1) |
240 | | ax-1cn 10674 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
241 | 239, 240 | eqeltrdi 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ) |
242 | | eldifi 4018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁)) |
243 | 242 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁)) |
244 | 243, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0) |
245 | | eldifsni 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0) |
246 | 245 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0) |
247 | | eldifsn 4676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (ℕ0
∖ {0}) ↔ (𝑘
∈ ℕ0 ∧ 𝑘 ≠ 0)) |
248 | 244, 246,
247 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖
{0})) |
249 | | dfn2 11990 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℕ0 ∖ {0}) |
250 | 248, 249 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ) |
251 | 250 | 0expd 13596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0) |
252 | 251 | oveq1d 7186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘))) |
253 | 244 | faccld 13737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℕ) |
254 | 253 | nncnd 11733 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℂ) |
255 | 253 | nnne0d 11767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0) |
256 | 254, 255 | div0d 11494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0) |
257 | 252, 256 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0) |
258 | | fzfid 13433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin) |
259 | 227, 241,
257, 258 | fsumss 15176 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) |
260 | 221, 259 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘))) |
261 | | 0cn 10712 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
262 | 238 | sumsn 15195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1) |
263 | 261, 240,
262 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑘 ∈ {0}
((0↑𝑘) /
(!‘𝑘)) =
1 |
264 | 260, 263 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1) |
265 | 207, 264 | oveq12d 7189 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1)) |
266 | 191 | mulid1d 10737 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥) |
267 | 266 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥) |
268 | 265, 267 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥) |
269 | 268 | oveq2d 7187 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥)) |
270 | 210, 269 | oveq12d 7189 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) |
271 | | ovexd 7206 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V) |
272 | 206, 270,
94, 271 | fvmptd 6783 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) |
273 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1) |
274 | 273 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) =
(⌊‘1)) |
275 | | flid 13270 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
276 | 81, 275 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(⌊‘1) = 1 |
277 | 274, 276 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1) |
278 | 277 | oveq2d 7187 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1)) |
279 | 278 | sumeq1d 15152 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁)) |
280 | 191 | div1d 11487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥) |
281 | 280 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥) |
282 | 281 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥)) |
283 | 282 | oveq1d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁)) |
284 | 195 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ) |
285 | 283, 284 | eqeltrd 2833 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) |
286 | | oveq2 7179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1)) |
287 | 286 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1))) |
288 | 287 | oveq1d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
289 | 288 | fsum1 15196 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈
(1...1)((log‘(𝑥 /
𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
290 | 81, 285, 289 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) |
291 | 279, 290,
283 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁)) |
292 | 273 | oveq2d 7187 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1)) |
293 | 292, 281 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥) |
294 | 293 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) |
295 | 294 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) |
296 | 295 | oveq1d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘)) |
297 | 296 | oveq1d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘))) |
298 | 297 | sumeq2dv 15154 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
299 | 273, 298 | oveq12d 7189 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) |
300 | 202 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
301 | 300 | mulid2d 10738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
302 | 299, 301 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) |
303 | 302 | oveq2d 7187 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) |
304 | 291, 303 | oveq12d 7189 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) |
305 | | ovexd 7206 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V) |
306 | 206, 304,
178, 305 | fvmptd 6783 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) |
307 | 272, 306 | oveq12d 7189 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) |
308 | 70, 72, 191 | subdird 11176 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥))) |
309 | 64 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ) |
310 | 212 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0) |
311 | 309, 191,
310 | divcan1d 11496 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) |
312 | 311 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
313 | 308, 312 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) |
314 | 205, 307,
313 | 3eqtr4d 2783 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) |
315 | 314 | fveq2d 6679 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
(abs‘((((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))) |
316 | 73, 191 | absmuld 14905 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥))) |
317 | | rprege0 12488 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
318 | 317 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
319 | | absid 14747 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
320 | 318, 319 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥) |
321 | 320 | oveq2d 7187 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) |
322 | 315, 316,
321 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
((abs‘(((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) |
323 | | 1cnd 10715 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ) |
324 | 294 | oveq1d 7186 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) |
325 | 323, 324 | csbied 3827 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) |
326 | 183, 322,
325 | 3brtr3d 5062 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁)) |
327 | 14 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ) |
328 | 74, 327, 94 | lemuldivd 12564 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))) |
329 | 326, 328 | mpbid 235 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)) |
330 | 75 | leabsd 14865 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
331 | 74, 75, 77, 329, 330 | letrd 10876 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
332 | 57 | adantrr 717 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) |
333 | 332 | subid1d 11065 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥)) |
334 | 333 | fveq2d 6679 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) |
335 | 331, 334 | breqtrrd 5059 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0))) |
336 | 33, 34, 54, 57, 69, 335 | rlimsqzlem 15099 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁)) |
337 | | divsubdir 11413 |
. . . . . 6
⊢
((((log‘𝑥)↑𝑁) ∈ ℂ ∧ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) |
338 | 59, 62, 66, 337 | syl3anc 1372 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) = ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) |
339 | 338 | mpteq2dva 5126 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))) |
340 | | rerpdivcl 12503 |
. . . . . . 7
⊢
((((!‘𝑁)
· Σ𝑘 ∈
(0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) |
341 | 27, 340 | sylancom 591 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) |
342 | | divass 11395 |
. . . . . . . . . 10
⊢
(((!‘𝑁) ∈
ℂ ∧ Σ𝑘
∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) |
343 | 60, 61, 66, 342 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) |
344 | 25 | recnd 10748 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) |
345 | 18, 67, 344, 68 | fsumdivc 15235 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) |
346 | 22 | recnd 10748 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ) |
347 | 24 | nnrpd 12513 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ+) |
348 | 347 | rpcnne0d 12524 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0)) |
349 | 66 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
350 | | divdiv32 11427 |
. . . . . . . . . . . . 13
⊢
((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧
(!‘𝑘) ≠ 0) ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) →
((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
351 | 346, 348,
349, 350 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
352 | 351 | sumeq2dv 15154 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
353 | 345, 352 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) |
354 | 353 | oveq2d 7187 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) |
355 | 343, 354 | eqtrd 2773 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) |
356 | 355 | mpteq2dva 5126 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))) |
357 | 2 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+) |
358 | 22, 357 | rerpdivcld 12546 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) |
359 | 358, 24 | nndivred 11771 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
360 | 18, 359 | fsumrecl 15185 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
361 | | rpssre 12480 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ |
362 | | rlimconst 14992 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑁))
⇝𝑟 (!‘𝑁)) |
363 | 361, 34, 362 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (!‘𝑁)) ⇝𝑟
(!‘𝑁)) |
364 | 361 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ℝ+ ⊆ ℝ) |
365 | | fzfid 13433 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) ∈
Fin) |
366 | 359 | anasss 470 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 𝑘
∈ (0...𝑁))) →
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) |
367 | 358 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) |
368 | 20 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
369 | 368 | faccld 13737 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℕ) |
370 | 369 | nnred 11732 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ) |
371 | 370 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ∈
ℝ) |
372 | 368, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) |
373 | 369 | nncnd 11733 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℂ) |
374 | | rlimconst 14992 |
. . . . . . . . . . . . . 14
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) |
375 | 361, 373,
374 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) |
376 | 369 | nnne0d 11767 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) |
377 | 376 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ≠
0) |
378 | 367, 371,
372, 375, 376, 377 | rlimdiv 15096 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 /
(!‘𝑘))) |
379 | 373, 376 | div0d 11494 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0) |
380 | 378, 379 | breqtrd 5057 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) |
381 | 364, 365,
366, 380 | fsumrlim 15260 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0) |
382 | | fzfi 13432 |
. . . . . . . . . . . 12
⊢
(0...𝑁) ∈
Fin |
383 | 382 | olci 865 |
. . . . . . . . . . 11
⊢
((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) |
384 | | sumz 15173 |
. . . . . . . . . . 11
⊢
(((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0) |
385 | 383, 384 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)0 =
0 |
386 | 381, 385 | breqtrdi 5072 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) |
387 | 17, 360, 363, 386 | rlimmul 15094 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
((!‘𝑁) ·
0)) |
388 | 34 | mul01d 10918 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 0) = 0) |
389 | 387, 388 | breqtrd 5057 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
0) |
390 | 356, 389 | eqbrtrd 5053 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟
0) |
391 | 56, 341, 54, 390 | rlimsub 15093 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 −
0)) |
392 | | 0m0e0 11837 |
. . . . 5
⊢ (0
− 0) = 0 |
393 | 391, 392 | breqtrdi 5072 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟
0) |
394 | 339, 393 | eqbrtrd 5053 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟
0) |
395 | 30, 32, 336, 394 | rlimadd 15091 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟
((!‘𝑁) +
0)) |
396 | | divsubdir 11413 |
. . . . . 6
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ ∧ (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
397 | 58, 63, 66, 396 | syl3anc 1372 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
398 | 397 | oveq1d 7186 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) |
399 | 10, 2 | rerpdivcld 12546 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ) |
400 | 399 | recnd 10748 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ) |
401 | 32 | recnd 10748 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ) |
402 | 400, 401 | npcand 11080 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) |
403 | 398, 402 | eqtrd 2773 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) |
404 | 403 | mpteq2dva 5126 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))) |
405 | 34 | addid1d 10919 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁) + 0) =
(!‘𝑁)) |
406 | 395, 404,
405 | 3brtr3d 5062 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁)) |