| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14015 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 2 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) | 
| 3 |  | elfznn 13594 | . . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 4 | 3 | nnrpd 13076 | . . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) | 
| 5 |  | rpdivcl 13061 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 6 | 2, 4, 5 | syl2an 596 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 7 | 6 | relogcld 26666 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 8 |  | simpll 766 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) | 
| 9 | 7, 8 | reexpcld 14204 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) | 
| 10 | 1, 9 | fsumrecl 15771 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) | 
| 11 |  | relogcl 26618 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) | 
| 12 |  | id 22 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) | 
| 13 |  | reexpcl 14120 | . . . . . . 7
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑁
∈ ℕ0) → ((log‘𝑥)↑𝑁) ∈ ℝ) | 
| 14 | 11, 12, 13 | syl2anr 597 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℝ) | 
| 15 |  | faccl 14323 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) | 
| 16 | 15 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℕ) | 
| 17 | 16 | nnred 12282 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℝ) | 
| 18 |  | fzfid 14015 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (0...𝑁) ∈ Fin) | 
| 19 | 11 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (log‘𝑥) ∈ ℝ) | 
| 20 |  | elfznn0 13661 | . . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 21 |  | reexpcl 14120 | . . . . . . . . . 10
⊢
(((log‘𝑥)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑘) ∈ ℝ) | 
| 22 | 19, 20, 21 | syl2an 596 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) | 
| 23 | 20 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 24 | 23 | faccld 14324 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) | 
| 25 | 22, 24 | nndivred 12321 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 26 | 18, 25 | fsumrecl 15771 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 27 | 17, 26 | remulcld 11292 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ) | 
| 28 | 14, 27 | resubcld 11692 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ) | 
| 29 | 10, 28 | resubcld 11692 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℝ) | 
| 30 | 29, 2 | rerpdivcld 13109 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℝ) | 
| 31 |  | rerpdivcl 13066 | . . . 4
⊢
(((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) | 
| 32 | 28, 31 | sylancom 588 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℝ) | 
| 33 |  | 1red 11263 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) | 
| 34 | 15 | nncnd 12283 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) | 
| 35 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) → 𝑘 = 𝑁) | 
| 36 | 35 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥)↑𝑘) = ((log‘𝑥)↑𝑁)) | 
| 37 | 36 | oveq1d 7447 | . . . . . . 7
⊢ ((𝑘 = 𝑁 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) = (((log‘𝑥)↑𝑁) / 𝑥)) | 
| 38 | 37 | mpteq2dva 5241 | . . . . . 6
⊢ (𝑘 = 𝑁 → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑁) / 𝑥))) | 
| 39 | 38 | breq1d 5152 | . . . . 5
⊢ (𝑘 = 𝑁 → ((𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟 0 ↔
(𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0)) | 
| 40 | 11 | recnd 11290 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) | 
| 41 |  | id 22 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) | 
| 42 |  | cxpexp 26711 | . . . . . . . . 9
⊢
(((log‘𝑥)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) | 
| 43 | 40, 41, 42 | syl2anr 597 | . . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑐𝑘) = ((log‘𝑥)↑𝑘)) | 
| 44 |  | rpcn 13046 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) | 
| 45 | 44 | adantl 481 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) | 
| 46 | 45 | cxp1d 26749 | . . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥↑𝑐1) = 𝑥) | 
| 47 | 43, 46 | oveq12d 7450 | . . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)) =
(((log‘𝑥)↑𝑘) / 𝑥)) | 
| 48 | 47 | mpteq2dva 5241 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1))) = (𝑥 ∈ ℝ+
↦ (((log‘𝑥)↑𝑘) / 𝑥))) | 
| 49 |  | nn0cn 12538 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 50 |  | 1rp 13039 | . . . . . . 7
⊢ 1 ∈
ℝ+ | 
| 51 |  | cxploglim2 27023 | . . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℝ+) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) | 
| 52 | 49, 50, 51 | sylancl 586 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑐𝑘) / (𝑥↑𝑐1)))
⇝𝑟 0) | 
| 53 | 48, 52 | eqbrtrrd 5166 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) | 
| 54 | 39, 53 | vtoclga 3576 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((log‘𝑥)↑𝑁) / 𝑥)) ⇝𝑟
0) | 
| 55 |  | rerpdivcl 13066 | . . . . . 6
⊢
((((log‘𝑥)↑𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) | 
| 56 | 14, 55 | sylancom 588 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) | 
| 57 | 56 | recnd 11290 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) | 
| 58 | 10 | recnd 11290 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) | 
| 59 | 14 | recnd 11290 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((log‘𝑥)↑𝑁) ∈ ℂ) | 
| 60 | 34 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (!‘𝑁) ∈ ℂ) | 
| 61 | 26 | recnd 11290 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 62 | 60, 61 | mulcld 11282 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) | 
| 63 | 59, 62 | subcld 11621 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) | 
| 64 | 58, 63 | subcld 11621 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) ∈ ℂ) | 
| 65 |  | rpcnne0 13054 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 66 | 65 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) | 
| 67 | 66 | simpld 494 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℂ) | 
| 68 | 66 | simprd 495 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → 𝑥 ≠ 0) | 
| 69 | 64, 67, 68 | divcld 12044 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) | 
| 70 | 69 | adantrr 717 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) ∈ ℂ) | 
| 71 | 15 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℕ) | 
| 72 | 71 | nncnd 12283 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ∈ ℂ) | 
| 73 | 70, 72 | subcld 11621 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) ∈ ℂ) | 
| 74 | 73 | abscld 15476 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ∈ ℝ) | 
| 75 | 56 | adantrr 717 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℝ) | 
| 76 | 75 | recnd 11290 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) | 
| 77 | 76 | abscld 15476 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((log‘𝑥)↑𝑁) / 𝑥)) ∈ ℝ) | 
| 78 |  | ioorp 13466 | . . . . . . . . . 10
⊢
(0(,)+∞) = ℝ+ | 
| 79 | 78 | eqcomi 2745 | . . . . . . . . 9
⊢
ℝ+ = (0(,)+∞) | 
| 80 |  | nnuz 12922 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 81 |  | 1z 12649 | . . . . . . . . . 10
⊢ 1 ∈
ℤ | 
| 82 | 81 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℤ) | 
| 83 |  | 1red 11263 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ) | 
| 84 |  | 1re 11262 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 85 |  | 1nn0 12544 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ0 | 
| 86 | 84, 85 | nn0addge1i 12576 | . . . . . . . . . 10
⊢ 1 ≤ (1
+ 1) | 
| 87 | 86 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ (1 + 1)) | 
| 88 |  | 0red 11265 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ ℝ) | 
| 89 | 71 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) | 
| 90 | 89 | nnred 12282 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℝ) | 
| 91 |  | rpre 13044 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) | 
| 92 | 91 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) | 
| 93 |  | fzfid 14015 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(0...𝑁) ∈
Fin) | 
| 94 |  | simprl 770 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+) | 
| 95 |  | rpdivcl 13061 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) | 
| 96 | 94, 95 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑥 / 𝑦) ∈
ℝ+) | 
| 97 | 96 | relogcld 26666 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(log‘(𝑥 / 𝑦)) ∈
ℝ) | 
| 98 |  | reexpcl 14120 | . . . . . . . . . . . . . 14
⊢
(((log‘(𝑥 /
𝑦)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) | 
| 99 | 97, 20, 98 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) ∈ ℝ) | 
| 100 | 20 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 101 | 100 | faccld 14324 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) | 
| 102 | 99, 101 | nndivred 12321 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 103 | 93, 102 | fsumrecl 15771 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 104 | 92, 103 | remulcld 11292 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℝ) | 
| 105 | 90, 104 | remulcld 11292 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) ∈ ℝ) | 
| 106 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑁 ∈
ℕ0) | 
| 107 | 97, 106 | reexpcld 14204 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) | 
| 108 |  | nnrp 13047 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) | 
| 109 | 108, 107 | sylan2 593 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℕ) → ((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℝ) | 
| 110 |  | reelprrecn 11248 | . . . . . . . . . . . 12
⊢ ℝ
∈ {ℝ, ℂ} | 
| 111 | 110 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ℝ ∈ {ℝ,
ℂ}) | 
| 112 | 104 | recnd 11290 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) ∈ ℂ) | 
| 113 | 107, 89 | nndivred 12321 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)) ∈ ℝ) | 
| 114 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
ℕ0) | 
| 115 |  | advlogexp 26698 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) | 
| 116 | 94, 114, 115 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦ (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (𝑦 ∈ ℝ+ ↦
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) | 
| 117 | 111, 112,
113, 116, 72 | dvmptcmul 26003 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))))) | 
| 118 | 107 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((log‘(𝑥 / 𝑦))↑𝑁) ∈ ℂ) | 
| 119 | 72 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ∈
ℂ) | 
| 120 | 71 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (!‘𝑁) ≠ 0) | 
| 121 | 120 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
(!‘𝑁) ≠
0) | 
| 122 | 118, 119,
121 | divcan2d 12046 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) →
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁))) = ((log‘(𝑥 / 𝑦))↑𝑁)) | 
| 123 | 122 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(((log‘(𝑥 / 𝑦))↑𝑁) / (!‘𝑁)))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) | 
| 124 | 117, 123 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (ℝ D (𝑦 ∈ ℝ+ ↦
((!‘𝑁) ·
(𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
((log‘(𝑥 / 𝑦))↑𝑁))) | 
| 125 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (𝑥 / 𝑦) = (𝑥 / 𝑛)) | 
| 126 | 125 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (log‘(𝑥 / 𝑦)) = (log‘(𝑥 / 𝑛))) | 
| 127 | 126 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑦 = 𝑛 → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘(𝑥 / 𝑛))↑𝑁)) | 
| 128 | 94 | rpxrd 13079 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ*) | 
| 129 |  | simp1rl 1238 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+) | 
| 130 |  | simp2r 1200 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+) | 
| 131 | 129, 130 | rpdivcld 13095 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 132 | 131 | relogcld 26666 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 133 |  | simp2l 1199 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ∈ ℝ+) | 
| 134 | 129, 133 | rpdivcld 13095 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) | 
| 135 | 134 | relogcld 26666 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) | 
| 136 |  | simp1l 1197 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑁 ∈
ℕ0) | 
| 137 |  | log1 26628 | . . . . . . . . . . 11
⊢
(log‘1) = 0 | 
| 138 | 130 | rpcnd 13080 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℂ) | 
| 139 | 138 | mullidd 11280 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) = 𝑛) | 
| 140 |  | simp33 1211 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) | 
| 141 | 139, 140 | eqbrtrd 5164 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 · 𝑛) ≤ 𝑥) | 
| 142 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ∈ ℝ) | 
| 143 | 129 | rpred 13078 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ) | 
| 144 | 142, 143,
130 | lemuldivd 13127 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) | 
| 145 | 141, 144 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑛)) | 
| 146 |  | logleb 26646 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) | 
| 147 | 50, 131, 146 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) | 
| 148 | 145, 147 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑛))) | 
| 149 | 137, 148 | eqbrtrrid 5178 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑛))) | 
| 150 |  | simp32 1210 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑦 ≤ 𝑛) | 
| 151 | 133, 130,
129 | lediv2d 13102 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑦 ≤ 𝑛 ↔ (𝑥 / 𝑛) ≤ (𝑥 / 𝑦))) | 
| 152 | 150, 151 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 / 𝑛) ≤ (𝑥 / 𝑦)) | 
| 153 | 131, 134 | logled 26670 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((𝑥 / 𝑛) ≤ (𝑥 / 𝑦) ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦)))) | 
| 154 | 152, 153 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+)
∧ (1 ≤ 𝑦 ∧ 𝑦 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (log‘(𝑥 / 𝑛)) ≤ (log‘(𝑥 / 𝑦))) | 
| 155 |  | leexp1a 14216 | . . . . . . . . . 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 2736 | . . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) | 
| 158 | 96 | 3ad2antr1 1188 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 / 𝑦) ∈
ℝ+) | 
| 159 | 158 | relogcld 26666 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘(𝑥 / 𝑦)) ∈ ℝ) | 
| 160 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑁 ∈
ℕ0) | 
| 161 |  | rpcn 13046 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) | 
| 162 | 161 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) | 
| 163 | 162 | 3ad2antr1 1188 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℂ) | 
| 164 | 163 | mullidd 11280 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) = 𝑦) | 
| 165 |  | simpr3 1196 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ≤ 𝑥) | 
| 166 | 164, 165 | eqbrtrd 5164 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 · 𝑦) ≤ 𝑥) | 
| 167 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ∈ ℝ) | 
| 168 | 94 | rpred 13078 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) | 
| 169 | 168 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 ∈ ℝ) | 
| 170 |  | simpr1 1194 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑦 ∈ ℝ+) | 
| 171 | 167, 169,
170 | lemuldivd 13127 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → ((1 · 𝑦) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑦))) | 
| 172 | 166, 171 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 1 ≤ (𝑥 / 𝑦)) | 
| 173 |  | logleb 26646 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑦) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) | 
| 174 | 50, 158, 173 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (1 ≤ (𝑥 / 𝑦) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑦)))) | 
| 175 | 172, 174 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → (log‘1) ≤
(log‘(𝑥 / 𝑦))) | 
| 176 | 137, 175 | eqbrtrrid 5178 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ (log‘(𝑥 / 𝑦))) | 
| 177 | 159, 160,
176 | expge0d 14205 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑦 ∈ ℝ+ ∧ 1 ≤
𝑦 ∧ 𝑦 ≤ 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑦))↑𝑁)) | 
| 178 | 50 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈
ℝ+) | 
| 179 |  | 1le1 11892 | . . . . . . . . . 10
⊢ 1 ≤
1 | 
| 180 | 179 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 1) | 
| 181 |  | simprr 772 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) | 
| 182 | 168 | leidd 11830 | . . . . . . . . 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 26071 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) ≤ ⦋1 /
𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁)) | 
| 184 |  | fzfid 14015 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 185 | 94, 4, 5 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 186 | 185 | relogcld 26666 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 187 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈
ℕ0) | 
| 188 | 186, 187 | reexpcld 14204 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) | 
| 189 | 184, 188 | fsumrecl 15771 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℝ) | 
| 190 | 189 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) ∈ ℂ) | 
| 191 | 94 | rpcnd 13080 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ) | 
| 192 | 72, 191 | mulcld 11282 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · 𝑥) ∈ ℂ) | 
| 193 | 11 | ad2antrl 728 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ) | 
| 194 | 193 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℂ) | 
| 195 | 194, 114 | expcld 14187 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℂ) | 
| 196 |  | fzfid 14015 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (0...𝑁) ∈ Fin) | 
| 197 | 193, 20, 21 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℝ) | 
| 198 | 20 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 199 | 198 | faccld 14324 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) | 
| 200 | 197, 199 | nndivred 12321 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 201 | 200 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 202 | 196, 201 | fsumcl 15770 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 203 | 72, 202 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℂ) | 
| 204 | 195, 203 | subcld 11621 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ ℂ) | 
| 205 | 190, 192,
204 | sub32d 11653 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) | 
| 206 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))))) = (𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))) | 
| 207 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) | 
| 208 | 207 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (⌊‘𝑦) = (⌊‘𝑥)) | 
| 209 | 208 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (1...(⌊‘𝑦)) = (1...(⌊‘𝑥))) | 
| 210 | 209 | sumeq1d 15737 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁)) | 
| 211 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (𝑥 / 𝑦) = (𝑥 / 𝑥)) | 
| 212 | 65 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) | 
| 213 |  | divid 11954 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) | 
| 214 | 212, 213 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 𝑥) = 1) | 
| 215 | 211, 214 | sylan9eqr 2798 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 / 𝑦) = 1) | 
| 216 | 215 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 / 𝑦) = 1) | 
| 217 | 216 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘1)) | 
| 218 | 217, 137 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = 0) | 
| 219 | 218 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = (0↑𝑘)) | 
| 220 | 219 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = ((0↑𝑘) / (!‘𝑘))) | 
| 221 | 220 | sumeq2dv 15739 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) | 
| 222 |  | nn0uz 12921 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 = (ℤ≥‘0) | 
| 223 | 114, 222 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑁 ∈
(ℤ≥‘0)) | 
| 224 |  | eluzfz1 13572 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) | 
| 225 | 223, 224 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 0 ∈ (0...𝑁)) | 
| 226 | 225 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → 0 ∈ (0...𝑁)) | 
| 227 | 226 | snssd 4808 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → {0} ⊆ (0...𝑁)) | 
| 228 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ {0} → 𝑘 = 0) | 
| 229 | 228 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → 𝑘 = 0) | 
| 230 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) | 
| 231 |  | 0exp0e1 14108 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0↑0) = 1 | 
| 232 | 230, 231 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (0↑𝑘) = 1) | 
| 233 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) | 
| 234 |  | fac0 14316 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(!‘0) = 1 | 
| 235 | 233, 234 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 0 → (!‘𝑘) = 1) | 
| 236 | 232, 235 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = (1 / 1)) | 
| 237 |  | 1div1e1 11959 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 / 1) =
1 | 
| 238 | 236, 237 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → ((0↑𝑘) / (!‘𝑘)) = 1) | 
| 239 | 229, 238 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) = 1) | 
| 240 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ | 
| 241 | 239, 240 | eqeltrdi 2848 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ {0}) → ((0↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 242 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ∈ (0...𝑁)) | 
| 243 | 242 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (0...𝑁)) | 
| 244 | 243, 20 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ0) | 
| 245 |  | eldifsni 4789 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0...𝑁) ∖ {0}) → 𝑘 ≠ 0) | 
| 246 | 245 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ≠ 0) | 
| 247 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (ℕ0
∖ {0}) ↔ (𝑘
∈ ℕ0 ∧ 𝑘 ≠ 0)) | 
| 248 | 244, 246,
247 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ (ℕ0 ∖
{0})) | 
| 249 |  | dfn2 12541 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℕ0 ∖ {0}) | 
| 250 | 248, 249 | eleqtrrdi 2851 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → 𝑘 ∈ ℕ) | 
| 251 | 250 | 0expd 14180 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0↑𝑘) = 0) | 
| 252 | 251 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = (0 / (!‘𝑘))) | 
| 253 | 244 | faccld 14324 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℕ) | 
| 254 | 253 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ∈
ℂ) | 
| 255 | 253 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (!‘𝑘) ≠ 0) | 
| 256 | 254, 255 | div0d 12043 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → (0 / (!‘𝑘)) = 0) | 
| 257 | 252, 256 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) ∧ 𝑘 ∈ ((0...𝑁) ∖ {0})) → ((0↑𝑘) / (!‘𝑘)) = 0) | 
| 258 |  | fzfid 14015 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (0...𝑁) ∈ Fin) | 
| 259 | 227, 241,
257, 258 | fsumss 15762 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((0↑𝑘) / (!‘𝑘))) | 
| 260 | 221, 259 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘))) | 
| 261 |  | 0cn 11254 | . . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ | 
| 262 | 238 | sumsn 15783 | . . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {0} ((0↑𝑘) / (!‘𝑘)) = 1) | 
| 263 | 261, 240,
262 | mp2an 692 | . . . . . . . . . . . . . . . . . 18
⊢
Σ𝑘 ∈ {0}
((0↑𝑘) /
(!‘𝑘)) =
1 | 
| 264 | 260, 263 | eqtrdi 2792 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = 1) | 
| 265 | 207, 264 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (𝑥 · 1)) | 
| 266 | 191 | mulridd 11279 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥) | 
| 267 | 266 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑥 · 1) = 𝑥) | 
| 268 | 265, 267 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = 𝑥) | 
| 269 | 268 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · 𝑥)) | 
| 270 | 210, 269 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) | 
| 271 |  | ovexd 7467 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) ∈ V) | 
| 272 | 206, 270,
94, 271 | fvmptd 7022 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥))) | 
| 273 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → 𝑦 = 1) | 
| 274 | 273 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) =
(⌊‘1)) | 
| 275 |  | flid 13849 | . . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (⌊‘1) = 1) | 
| 276 | 81, 275 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢
(⌊‘1) = 1 | 
| 277 | 274, 276 | eqtrdi 2792 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (⌊‘𝑦) = 1) | 
| 278 | 277 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1...(⌊‘𝑦)) = (1...1)) | 
| 279 | 278 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁)) | 
| 280 | 191 | div1d 12036 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 / 1) = 𝑥) | 
| 281 | 280 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 1) = 𝑥) | 
| 282 | 281 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 1)) = (log‘𝑥)) | 
| 283 | 282 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) = ((log‘𝑥)↑𝑁)) | 
| 284 | 195 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘𝑥)↑𝑁) ∈ ℂ) | 
| 285 | 283, 284 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) | 
| 286 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑥 / 𝑛) = (𝑥 / 1)) | 
| 287 | 286 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (log‘(𝑥 / 𝑛)) = (log‘(𝑥 / 1))) | 
| 288 | 287 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) | 
| 289 | 288 | fsum1 15784 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℤ ∧ ((log‘(𝑥 / 1))↑𝑁) ∈ ℂ) → Σ𝑛 ∈
(1...1)((log‘(𝑥 /
𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) | 
| 290 | 81, 285, 289 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...1)((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘(𝑥 / 1))↑𝑁)) | 
| 291 | 279, 290,
283 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) = ((log‘𝑥)↑𝑁)) | 
| 292 | 273 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = (𝑥 / 1)) | 
| 293 | 292, 281 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑥 / 𝑦) = 𝑥) | 
| 294 | 293 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) | 
| 295 | 294 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (log‘(𝑥 / 𝑦)) = (log‘𝑥)) | 
| 296 | 295 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝑥 / 𝑦))↑𝑘) = ((log‘𝑥)↑𝑘)) | 
| 297 | 296 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = (((log‘𝑥)↑𝑘) / (!‘𝑘))) | 
| 298 | 297 | sumeq2dv 15739 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) | 
| 299 | 273, 298 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) | 
| 300 | 202 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 301 | 300 | mullidd 11280 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (1 · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) | 
| 302 | 299, 301 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) | 
| 303 | 302 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) | 
| 304 | 291, 303 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) | 
| 305 |  | ovexd 7467 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) ∈ V) | 
| 306 | 206, 304,
178, 305 | fvmptd 7022 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1) = (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) | 
| 307 | 272, 306 | oveq12d 7450 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · 𝑥)) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) | 
| 308 | 70, 72, 191 | subdird 11721 | . . . . . . . . . . . 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 495 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ≠ 0) | 
| 311 | 309, 191,
310 | divcan1d 12045 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))))) | 
| 312 | 311 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) · 𝑥) − ((!‘𝑁) · 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) | 
| 313 | 308, 312 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) − ((!‘𝑁) · 𝑥))) | 
| 314 | 205, 307,
313 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1)) = ((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) | 
| 315 | 314 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
(abs‘((((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥))) | 
| 316 | 73, 191 | absmuld 15494 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁)) · 𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥))) | 
| 317 |  | rprege0 13051 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) | 
| 318 | 317 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) | 
| 319 |  | absid 15336 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) | 
| 320 | 318, 319 | syl 17 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘𝑥) = 𝑥) | 
| 321 | 320 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · (abs‘𝑥)) = ((abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) | 
| 322 | 315, 316,
321 | 3eqtrd 2780 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘𝑥) − ((𝑦 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑦))((log‘(𝑥 / 𝑛))↑𝑁) − ((!‘𝑁) · (𝑦 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝑥 / 𝑦))↑𝑘) / (!‘𝑘))))))‘1))) =
((abs‘(((Σ𝑛
∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥)) | 
| 323 |  | 1cnd 11257 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ ℂ) | 
| 324 | 294 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑦 = 1) → ((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) | 
| 325 | 323, 324 | csbied 3934 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ⦋1 / 𝑦⦌((log‘(𝑥 / 𝑦))↑𝑁) = ((log‘𝑥)↑𝑁)) | 
| 326 | 183, 322,
325 | 3brtr3d 5173 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁)) | 
| 327 | 14 | adantrr 717 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘𝑥)↑𝑁) ∈ ℝ) | 
| 328 | 74, 327, 94 | lemuldivd 13127 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) · 𝑥) ≤ ((log‘𝑥)↑𝑁) ↔ (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥))) | 
| 329 | 326, 328 | mpbid 232 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (((log‘𝑥)↑𝑁) / 𝑥)) | 
| 330 | 75 | leabsd 15454 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) | 
| 331 | 74, 75, 77, 329, 330 | letrd 11419 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) | 
| 332 | 57 | adantrr 717 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (((log‘𝑥)↑𝑁) / 𝑥) ∈ ℂ) | 
| 333 | 332 | subid1d 11610 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → ((((log‘𝑥)↑𝑁) / 𝑥) − 0) = (((log‘𝑥)↑𝑁) / 𝑥)) | 
| 334 | 333 | fveq2d 6909 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0)) = (abs‘(((log‘𝑥)↑𝑁) / 𝑥))) | 
| 335 | 331, 334 | breqtrrd 5170 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) − (!‘𝑁))) ≤ (abs‘((((log‘𝑥)↑𝑁) / 𝑥) − 0))) | 
| 336 | 33, 34, 54, 57, 69, 335 | rlimsqzlem 15686 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥)) ⇝𝑟 (!‘𝑁)) | 
| 337 |  | divsubdir 11962 | . . . . . 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 5241 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)))) | 
| 340 |  | rerpdivcl 13066 | . . . . . . 7
⊢
((((!‘𝑁)
· Σ𝑘 ∈
(0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ+) →
(((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) | 
| 341 | 27, 340 | sylancom 588 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) ∈ ℝ) | 
| 342 |  | divass 11941 | . . . . . . . . . 10
⊢
(((!‘𝑁) ∈
ℂ ∧ Σ𝑘
∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) | 
| 343 | 60, 61, 66, 342 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥))) | 
| 344 | 25 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 345 | 18, 67, 344, 68 | fsumdivc 15823 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) | 
| 346 | 22 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘𝑥)↑𝑘) ∈ ℂ) | 
| 347 | 24 | nnrpd 13076 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ+) | 
| 348 | 347 | rpcnne0d 13087 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((!‘𝑘) ∈ ℂ ∧ (!‘𝑘) ≠ 0)) | 
| 349 | 66 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) | 
| 350 |  | divdiv32 11976 | . . . . . . . . . . . . 13
⊢
((((log‘𝑥)↑𝑘) ∈ ℂ ∧ ((!‘𝑘) ∈ ℂ ∧
(!‘𝑘) ≠ 0) ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) →
((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) | 
| 351 | 346, 348,
349, 350 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) | 
| 352 | 351 | sumeq2dv 15739 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) | 
| 353 | 345, 352 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥) = Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) | 
| 354 | 353 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((!‘𝑁) · (Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)) / 𝑥)) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) | 
| 355 | 343, 354 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) | 
| 356 | 355 | mpteq2dva 5241 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))))) | 
| 357 | 2 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℝ+) | 
| 358 | 22, 357 | rerpdivcld 13109 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) | 
| 359 | 358, 24 | nndivred 12321 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) | 
| 360 | 18, 359 | fsumrecl 15771 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) | 
| 361 |  | rpssre 13043 | . . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ | 
| 362 |  | rlimconst 15581 | . . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑁))
⇝𝑟 (!‘𝑁)) | 
| 363 | 361, 34, 362 | sylancr 587 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (!‘𝑁)) ⇝𝑟
(!‘𝑁)) | 
| 364 | 361 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ℝ+ ⊆ ℝ) | 
| 365 |  | fzfid 14015 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) ∈
Fin) | 
| 366 | 359 | anasss 466 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈
ℝ+ ∧ 𝑘
∈ (0...𝑁))) →
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)) ∈ ℝ) | 
| 367 | 358 | an32s 652 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥)↑𝑘) / 𝑥) ∈ ℝ) | 
| 368 | 20 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 369 | 368 | faccld 14324 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℕ) | 
| 370 | 369 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℝ) | 
| 371 | 370 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ∈
ℝ) | 
| 372 | 368, 53 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(((log‘𝑥)↑𝑘) / 𝑥)) ⇝𝑟
0) | 
| 373 | 369 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈
ℂ) | 
| 374 |  | rlimconst 15581 | . . . . . . . . . . . . . 14
⊢
((ℝ+ ⊆ ℝ ∧ (!‘𝑘) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) | 
| 375 | 361, 373,
374 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
(!‘𝑘))
⇝𝑟 (!‘𝑘)) | 
| 376 | 369 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) | 
| 377 | 376 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑘) ≠
0) | 
| 378 | 367, 371,
372, 375, 376, 377 | rlimdiv 15683 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 (0 /
(!‘𝑘))) | 
| 379 | 373, 376 | div0d 12043 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (0 / (!‘𝑘)) = 0) | 
| 380 | 378, 379 | breqtrd 5168 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ (0...𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) | 
| 381 | 364, 365,
366, 380 | fsumrlim 15848 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟 Σ𝑘 ∈ (0...𝑁)0) | 
| 382 |  | fzfi 14014 | . . . . . . . . . . . 12
⊢
(0...𝑁) ∈
Fin | 
| 383 | 382 | olci 866 | . . . . . . . . . . 11
⊢
((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) | 
| 384 |  | sumz 15759 | . . . . . . . . . . 11
⊢
(((0...𝑁) ⊆
(ℤ≥‘0) ∨ (0...𝑁) ∈ Fin) → Σ𝑘 ∈ (0...𝑁)0 = 0) | 
| 385 | 383, 384 | ax-mp 5 | . . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)0 =
0 | 
| 386 | 381, 385 | breqtrdi 5183 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘))) ⇝𝑟
0) | 
| 387 | 17, 360, 363, 386 | rlimmul 15682 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
((!‘𝑁) ·
0)) | 
| 388 | 34 | mul01d 11461 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁)
· 0) = 0) | 
| 389 | 387, 388 | breqtrd 5168 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((((log‘𝑥)↑𝑘) / 𝑥) / (!‘𝑘)))) ⇝𝑟
0) | 
| 390 | 356, 389 | eqbrtrd 5164 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥)) ⇝𝑟
0) | 
| 391 | 56, 341, 54, 390 | rlimsub 15681 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟 (0 −
0)) | 
| 392 |  | 0m0e0 12387 | . . . . 5
⊢ (0
− 0) = 0 | 
| 393 | 391, 392 | breqtrdi 5183 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) / 𝑥) − (((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))) / 𝑥))) ⇝𝑟
0) | 
| 394 | 339, 393 | eqbrtrd 5164 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) ⇝𝑟
0) | 
| 395 | 30, 32, 336, 394 | rlimadd 15680 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) ⇝𝑟
((!‘𝑁) +
0)) | 
| 396 |  | divsubdir 11962 | . . . . . 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 7447 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) | 
| 399 | 10, 2 | rerpdivcld 13109 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℝ) | 
| 400 | 399 | recnd 11290 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) ∈ ℂ) | 
| 401 | 32 | recnd 11290 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥) ∈ ℂ) | 
| 402 | 400, 401 | npcand 11625 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥) − ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) | 
| 403 | 398, 402 | eqtrd 2776 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈
ℝ+) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) | 
| 404 | 403 | mpteq2dva 5241 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) − (((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘))))) / 𝑥) + ((((log‘𝑥)↑𝑁) − ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(((log‘𝑥)↑𝑘) / (!‘𝑘)))) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥))) | 
| 405 | 34 | addridd 11462 | . 2
⊢ (𝑁 ∈ ℕ0
→ ((!‘𝑁) + 0) =
(!‘𝑁)) | 
| 406 | 395, 404,
405 | 3brtr3d 5173 | 1
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑𝑁) / 𝑥)) ⇝𝑟 (!‘𝑁)) |