| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnnn0 12533 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 2 |  | faccl 14322 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ) | 
| 4 | 3 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℂ) | 
| 5 |  | ere 16125 | . . . . . . 7
⊢ e ∈
ℝ | 
| 6 | 5 | recni 11275 | . . . . . 6
⊢ e ∈
ℂ | 
| 7 |  | epos 16243 | . . . . . . 7
⊢ 0 <
e | 
| 8 | 5, 7 | gt0ne0ii 11799 | . . . . . 6
⊢ e ≠
0 | 
| 9 |  | divcl 11928 | . . . . . 6
⊢
(((!‘𝑁) ∈
ℂ ∧ e ∈ ℂ ∧ e ≠ 0) → ((!‘𝑁) / e) ∈
ℂ) | 
| 10 | 6, 8, 9 | mp3an23 1455 | . . . . 5
⊢
((!‘𝑁) ∈
ℂ → ((!‘𝑁)
/ e) ∈ ℂ) | 
| 11 | 4, 10 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) / e) ∈
ℂ) | 
| 12 |  | derang.d | . . . . . . . 8
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) | 
| 13 |  | subfac.n | . . . . . . . 8
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛))) | 
| 14 | 12, 13 | subfacf 35180 | . . . . . . 7
⊢ 𝑆:ℕ0⟶ℕ0 | 
| 15 | 14 | ffvelcdmi 7103 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) ∈
ℕ0) | 
| 16 | 1, 15 | syl 17 | . . . . 5
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈
ℕ0) | 
| 17 | 16 | nn0cnd 12589 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) ∈ ℂ) | 
| 18 | 11, 17 | subcld 11620 | . . 3
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) −
(𝑆‘𝑁)) ∈ ℂ) | 
| 19 | 18 | abscld 15475 | . 2
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) ∈
ℝ) | 
| 20 |  | peano2nn 12278 | . . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) | 
| 21 | 20 | peano2nnd 12283 | . . . 4
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) ∈
ℕ) | 
| 22 | 21 | nnred 12281 | . . 3
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) ∈
ℝ) | 
| 23 | 20, 20 | nnmulcld 12319 | . . 3
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · (𝑁 + 1)) ∈
ℕ) | 
| 24 | 22, 23 | nndivred 12320 | . 2
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1))) ∈ ℝ) | 
| 25 |  | nnrecre 12308 | . 2
⊢ (𝑁 ∈ ℕ → (1 /
𝑁) ∈
ℝ) | 
| 26 |  | eqid 2737 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ ((-1↑𝑛) /
(!‘𝑛))) = (𝑛 ∈ ℕ0
↦ ((-1↑𝑛) /
(!‘𝑛))) | 
| 27 |  | eqid 2737 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘-1)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘-1)↑𝑛) /
(!‘𝑛))) | 
| 28 |  | eqid 2737 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘-1)↑(𝑁 + 1)) / (!‘(𝑁 + 1))) · ((1 / ((𝑁 + 1) + 1))↑𝑛))) = (𝑛 ∈ ℕ0 ↦
((((abs‘-1)↑(𝑁 +
1)) / (!‘(𝑁 + 1)))
· ((1 / ((𝑁 + 1) +
1))↑𝑛))) | 
| 29 |  | neg1cn 12380 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 30 | 29 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℕ → -1 ∈
ℂ) | 
| 31 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 32 | 31 | absnegi 15439 | . . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) | 
| 33 |  | abs1 15336 | . . . . . . . . 9
⊢
(abs‘1) = 1 | 
| 34 | 32, 33 | eqtri 2765 | . . . . . . . 8
⊢
(abs‘-1) = 1 | 
| 35 |  | 1le1 11891 | . . . . . . . 8
⊢ 1 ≤
1 | 
| 36 | 34, 35 | eqbrtri 5164 | . . . . . . 7
⊢
(abs‘-1) ≤ 1 | 
| 37 | 36 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(abs‘-1) ≤ 1) | 
| 38 | 26, 27, 28, 20, 30, 37 | eftlub 16145 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))‘𝑘)) ≤
(((abs‘-1)↑(𝑁 +
1)) · (((𝑁 + 1) + 1)
/ ((!‘(𝑁 + 1))
· (𝑁 +
1))))) | 
| 39 | 20 | nnnn0d 12587 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) | 
| 40 |  | eluznn0 12959 | . . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) | 
| 41 | 39, 40 | sylan 580 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) | 
| 42 | 26 | eftval 16112 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) / (!‘𝑛)))‘𝑘) = ((-1↑𝑘) / (!‘𝑘))) | 
| 43 | 41, 42 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → ((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))‘𝑘) = ((-1↑𝑘) / (!‘𝑘))) | 
| 44 | 43 | sumeq2dv 15738 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) | 
| 45 | 44 | fveq2d 6910 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))‘𝑘)) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) | 
| 46 | 34 | oveq1i 7441 | . . . . . . . 8
⊢
((abs‘-1)↑(𝑁 + 1)) = (1↑(𝑁 + 1)) | 
| 47 | 20 | nnzd 12640 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℤ) | 
| 48 |  | 1exp 14132 | . . . . . . . . 9
⊢ ((𝑁 + 1) ∈ ℤ →
(1↑(𝑁 + 1)) =
1) | 
| 49 | 47, 48 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1↑(𝑁 + 1)) =
1) | 
| 50 | 46, 49 | eqtrid 2789 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((abs‘-1)↑(𝑁 +
1)) = 1) | 
| 51 | 50 | oveq1d 7446 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(((abs‘-1)↑(𝑁 +
1)) · (((𝑁 + 1) + 1)
/ ((!‘(𝑁 + 1))
· (𝑁 + 1)))) = (1
· (((𝑁 + 1) + 1) /
((!‘(𝑁 + 1)) ·
(𝑁 +
1))))) | 
| 52 |  | faccl 14322 | . . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℕ0
→ (!‘(𝑁 + 1))
∈ ℕ) | 
| 53 | 39, 52 | syl 17 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 + 1)) ∈
ℕ) | 
| 54 | 53, 20 | nnmulcld 12319 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) ·
(𝑁 + 1)) ∈
ℕ) | 
| 55 | 22, 54 | nndivred 12320 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))) ∈
ℝ) | 
| 56 | 55 | recnd 11289 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))) ∈
ℂ) | 
| 57 | 56 | mullidd 11279 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (1
· (((𝑁 + 1) + 1) /
((!‘(𝑁 + 1)) ·
(𝑁 + 1)))) = (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1)))) | 
| 58 | 51, 57 | eqtrd 2777 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(((abs‘-1)↑(𝑁 +
1)) · (((𝑁 + 1) + 1)
/ ((!‘(𝑁 + 1))
· (𝑁 + 1)))) =
(((𝑁 + 1) + 1) /
((!‘(𝑁 + 1)) ·
(𝑁 + 1)))) | 
| 59 | 38, 45, 58 | 3brtr3d 5174 | . . . 4
⊢ (𝑁 ∈ ℕ →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ≤ (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1)))) | 
| 60 |  | eqid 2737 | . . . . . . 7
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) | 
| 61 |  | eftcl 16109 | . . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 62 | 29, 61 | mpan 690 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((-1↑𝑘) /
(!‘𝑘)) ∈
ℂ) | 
| 63 | 41, 62 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 64 | 26 | eftlcvg 16142 | . . . . . . . 8
⊢ ((-1
∈ ℂ ∧ (𝑁 +
1) ∈ ℕ0) → seq(𝑁 + 1)( + , (𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))) ∈ dom
⇝ ) | 
| 65 | 29, 39, 64 | sylancr 587 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → seq(𝑁 + 1)( + , (𝑛 ∈ ℕ0 ↦
((-1↑𝑛) /
(!‘𝑛)))) ∈ dom
⇝ ) | 
| 66 | 60, 47, 43, 63, 65 | isumcl 15797 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 67 | 66 | abscld 15475 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ∈ ℝ) | 
| 68 | 3 | nnred 12281 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℝ) | 
| 69 | 3 | nngt0d 12315 | . . . . 5
⊢ (𝑁 ∈ ℕ → 0 <
(!‘𝑁)) | 
| 70 |  | lemul2 12120 | . . . . 5
⊢
(((abs‘Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ∈ ℝ ∧ (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))) ∈ ℝ ∧ ((!‘𝑁) ∈ ℝ ∧ 0 <
(!‘𝑁))) →
((abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ≤ (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))) ↔ ((!‘𝑁) · (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) ≤ ((!‘𝑁) · (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1)))))) | 
| 71 | 67, 55, 68, 69, 70 | syl112anc 1376 | . . . 4
⊢ (𝑁 ∈ ℕ →
((abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ≤ (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))) ↔ ((!‘𝑁) · (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) ≤ ((!‘𝑁) · (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1)))))) | 
| 72 | 59, 71 | mpbid 232 | . . 3
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) ≤ ((!‘𝑁) · (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))))) | 
| 73 | 12, 13 | subfacval2 35192 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))) | 
| 74 | 1, 73 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))) | 
| 75 |  | nncn 12274 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 76 |  | pncan 11514 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) | 
| 77 | 75, 31, 76 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) | 
| 78 | 77 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0...((𝑁 + 1) − 1)) =
(0...𝑁)) | 
| 79 | 78 | sumeq1d 15736 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) | 
| 80 | 79 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘))) =
((!‘𝑁) ·
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))) | 
| 81 | 74, 80 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...((𝑁 + 1) − 1))((-1↑𝑘) / (!‘𝑘)))) | 
| 82 | 81 | oveq1d 7446 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑆‘𝑁) + ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = (((!‘𝑁) · Σ𝑘 ∈ (0...((𝑁 + 1) − 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 83 |  | divrec 11938 | . . . . . . . . . 10
⊢
(((!‘𝑁) ∈
ℂ ∧ e ∈ ℂ ∧ e ≠ 0) → ((!‘𝑁) / e) = ((!‘𝑁) · (1 /
e))) | 
| 84 | 6, 8, 83 | mp3an23 1455 | . . . . . . . . 9
⊢
((!‘𝑁) ∈
ℂ → ((!‘𝑁)
/ e) = ((!‘𝑁)
· (1 / e))) | 
| 85 | 4, 84 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) / e) =
((!‘𝑁) · (1 /
e))) | 
| 86 |  | df-e 16104 | . . . . . . . . . . . 12
⊢ e =
(exp‘1) | 
| 87 | 86 | oveq2i 7442 | . . . . . . . . . . 11
⊢ (1 / e) =
(1 / (exp‘1)) | 
| 88 |  | efneg 16134 | . . . . . . . . . . . 12
⊢ (1 ∈
ℂ → (exp‘-1) = (1 / (exp‘1))) | 
| 89 | 31, 88 | ax-mp 5 | . . . . . . . . . . 11
⊢
(exp‘-1) = (1 / (exp‘1)) | 
| 90 |  | efval 16115 | . . . . . . . . . . . 12
⊢ (-1
∈ ℂ → (exp‘-1) = Σ𝑘 ∈ ℕ0 ((-1↑𝑘) / (!‘𝑘))) | 
| 91 | 29, 90 | ax-mp 5 | . . . . . . . . . . 11
⊢
(exp‘-1) = Σ𝑘 ∈ ℕ0 ((-1↑𝑘) / (!‘𝑘)) | 
| 92 | 87, 89, 91 | 3eqtr2i 2771 | . . . . . . . . . 10
⊢ (1 / e) =
Σ𝑘 ∈
ℕ0 ((-1↑𝑘) / (!‘𝑘)) | 
| 93 |  | nn0uz 12920 | . . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) | 
| 94 | 42 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) / (!‘𝑛)))‘𝑘) = ((-1↑𝑘) / (!‘𝑘))) | 
| 95 | 62 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ ((-1↑𝑘) /
(!‘𝑘)) ∈
ℂ) | 
| 96 |  | 0nn0 12541 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 97 | 26 | eftlcvg 16142 | . . . . . . . . . . . . 13
⊢ ((-1
∈ ℂ ∧ 0 ∈ ℕ0) → seq0( + , (𝑛 ∈ ℕ0
↦ ((-1↑𝑛) /
(!‘𝑛)))) ∈ dom
⇝ ) | 
| 98 | 29, 96, 97 | mp2an 692 | . . . . . . . . . . . 12
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ | 
| 99 | 98 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((-1↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ ) | 
| 100 | 93, 60, 39, 94, 95, 99 | isumsplit 15876 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈
ℕ0 ((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...((𝑁 + 1) − 1))((-1↑𝑘) / (!‘𝑘)) + Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) | 
| 101 | 92, 100 | eqtrid 2789 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (1 / e) =
(Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘)) + Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) | 
| 102 | 101 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) · (1 /
e)) = ((!‘𝑁) ·
(Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘)) + Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 103 |  | fzfid 14014 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0...((𝑁 + 1) − 1))
∈ Fin) | 
| 104 |  | elfznn0 13660 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...((𝑁 + 1) − 1)) → 𝑘 ∈ ℕ0) | 
| 105 | 104 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((𝑁 + 1) − 1))) → 𝑘 ∈ ℕ0) | 
| 106 | 29, 105, 61 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((𝑁 + 1) − 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 107 | 103, 106 | fsumcl 15769 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘)) ∈
ℂ) | 
| 108 | 4, 107, 66 | adddid 11285 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
(Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘)) + Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = (((!‘𝑁) · Σ𝑘 ∈ (0...((𝑁 + 1) − 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 109 | 85, 102, 108 | 3eqtrd 2781 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) / e) =
(((!‘𝑁) ·
Σ𝑘 ∈
(0...((𝑁 + 1) −
1))((-1↑𝑘) /
(!‘𝑘))) +
((!‘𝑁) ·
Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 110 | 82, 109 | eqtr4d 2780 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑆‘𝑁) + ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) / e)) | 
| 111 | 4, 66 | mulcld 11281 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ∈ ℂ) | 
| 112 | 11, 17, 111 | subaddd 11638 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
((((!‘𝑁) / e) −
(𝑆‘𝑁)) = ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ ((𝑆‘𝑁) + ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) / e))) | 
| 113 | 110, 112 | mpbird 257 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) / e) −
(𝑆‘𝑁)) = ((!‘𝑁) · Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) | 
| 114 | 113 | fveq2d 6910 | . . . 4
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) = (abs‘((!‘𝑁) · Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 115 | 4, 66 | absmuld 15493 | . . . 4
⊢ (𝑁 ∈ ℕ →
(abs‘((!‘𝑁)
· Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = ((abs‘(!‘𝑁)) · (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 116 | 3 | nnnn0d 12587 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ0) | 
| 117 | 116 | nn0ge0d 12590 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
(!‘𝑁)) | 
| 118 | 68, 117 | absidd 15461 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(abs‘(!‘𝑁)) =
(!‘𝑁)) | 
| 119 | 118 | oveq1d 7446 | . . . 4
⊢ (𝑁 ∈ ℕ →
((abs‘(!‘𝑁))
· (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))) = ((!‘𝑁) · (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 120 | 114, 115,
119 | 3eqtrd 2781 | . . 3
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) = ((!‘𝑁) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))) | 
| 121 |  | facp1 14317 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) | 
| 122 | 1, 121 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) | 
| 123 | 122 | oveq1d 7446 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) ·
(𝑁 + 1)) = (((!‘𝑁) · (𝑁 + 1)) · (𝑁 + 1))) | 
| 124 | 20 | nncnd 12282 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) | 
| 125 | 4, 124, 124 | mulassd 11284 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) ·
(𝑁 + 1)) · (𝑁 + 1)) = ((!‘𝑁) · ((𝑁 + 1) · (𝑁 + 1)))) | 
| 126 | 123, 125 | eqtr2d 2778 | . . . . 5
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
((𝑁 + 1) · (𝑁 + 1))) = ((!‘(𝑁 + 1)) · (𝑁 + 1))) | 
| 127 | 126 | oveq2d 7447 | . . . 4
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) ·
((𝑁 + 1) + 1)) /
((!‘𝑁) ·
((𝑁 + 1) · (𝑁 + 1)))) = (((!‘𝑁) · ((𝑁 + 1) + 1)) / ((!‘(𝑁 + 1)) · (𝑁 + 1)))) | 
| 128 | 21 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) ∈
ℂ) | 
| 129 | 23 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · (𝑁 + 1)) ∈
ℂ) | 
| 130 | 23 | nnne0d 12316 | . . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · (𝑁 + 1)) ≠ 0) | 
| 131 | 3 | nnne0d 12316 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ≠
0) | 
| 132 | 128, 129,
4, 130, 131 | divcan5d 12069 | . . . 4
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) ·
((𝑁 + 1) + 1)) /
((!‘𝑁) ·
((𝑁 + 1) · (𝑁 + 1)))) = (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1)))) | 
| 133 | 54 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) ·
(𝑁 + 1)) ∈
ℂ) | 
| 134 | 54 | nnne0d 12316 | . . . . 5
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) ·
(𝑁 + 1)) ≠
0) | 
| 135 | 4, 128, 133, 134 | divassd 12078 | . . . 4
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) ·
((𝑁 + 1) + 1)) /
((!‘(𝑁 + 1)) ·
(𝑁 + 1))) = ((!‘𝑁) · (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))))) | 
| 136 | 127, 132,
135 | 3eqtr3d 2785 | . . 3
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1))) = ((!‘𝑁) · (((𝑁 + 1) + 1) / ((!‘(𝑁 + 1)) · (𝑁 + 1))))) | 
| 137 | 72, 120, 136 | 3brtr4d 5175 | . 2
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) ≤ (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1)))) | 
| 138 |  | nnmulcl 12290 | . . . . . . 7
⊢ ((((𝑁 + 1) + 1) ∈ ℕ ∧
𝑁 ∈ ℕ) →
(((𝑁 + 1) + 1) ·
𝑁) ∈
ℕ) | 
| 139 | 21, 138 | mpancom 688 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) · 𝑁) ∈
ℕ) | 
| 140 | 139 | nnred 12281 | . . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) · 𝑁) ∈
ℝ) | 
| 141 | 140 | ltp1d 12198 | . . . 4
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) · 𝑁) < ((((𝑁 + 1) + 1) · 𝑁) + 1)) | 
| 142 | 129 | mullidd 11279 | . . . . 5
⊢ (𝑁 ∈ ℕ → (1
· ((𝑁 + 1) ·
(𝑁 + 1))) = ((𝑁 + 1) · (𝑁 + 1))) | 
| 143 | 31 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) | 
| 144 | 75, 143, 124 | adddird 11286 | . . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · (𝑁 + 1)) = ((𝑁 · (𝑁 + 1)) + (1 · (𝑁 + 1)))) | 
| 145 | 75, 124 | mulcomd 11282 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 · (𝑁 + 1)) = ((𝑁 + 1) · 𝑁)) | 
| 146 | 124 | mullidd 11279 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (1
· (𝑁 + 1)) = (𝑁 + 1)) | 
| 147 | 145, 146 | oveq12d 7449 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 · (𝑁 + 1)) + (1 · (𝑁 + 1))) = (((𝑁 + 1) · 𝑁) + (𝑁 + 1))) | 
| 148 | 124, 143,
75 | adddird 11286 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) · 𝑁) = (((𝑁 + 1) · 𝑁) + (1 · 𝑁))) | 
| 149 | 148 | oveq1d 7446 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) + 1) · 𝑁) + 1) = ((((𝑁 + 1) · 𝑁) + (1 · 𝑁)) + 1)) | 
| 150 | 75 | mullidd 11279 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (1
· 𝑁) = 𝑁) | 
| 151 | 150 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) · 𝑁) + (1 · 𝑁)) = (((𝑁 + 1) · 𝑁) + 𝑁)) | 
| 152 | 151 | oveq1d 7446 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) · 𝑁) + (1 · 𝑁)) + 1) = ((((𝑁 + 1) · 𝑁) + 𝑁) + 1)) | 
| 153 | 124, 75 | mulcld 11281 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) · 𝑁) ∈ ℂ) | 
| 154 | 153, 75, 143 | addassd 11283 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) · 𝑁) + 𝑁) + 1) = (((𝑁 + 1) · 𝑁) + (𝑁 + 1))) | 
| 155 | 149, 152,
154 | 3eqtrd 2781 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) + 1) · 𝑁) + 1) = (((𝑁 + 1) · 𝑁) + (𝑁 + 1))) | 
| 156 | 147, 155 | eqtr4d 2780 | . . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑁 · (𝑁 + 1)) + (1 · (𝑁 + 1))) = ((((𝑁 + 1) + 1) · 𝑁) + 1)) | 
| 157 | 142, 144,
156 | 3eqtrd 2781 | . . . 4
⊢ (𝑁 ∈ ℕ → (1
· ((𝑁 + 1) ·
(𝑁 + 1))) = ((((𝑁 + 1) + 1) · 𝑁) + 1)) | 
| 158 | 141, 157 | breqtrrd 5171 | . . 3
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) · 𝑁) < (1 · ((𝑁 + 1) · (𝑁 + 1)))) | 
| 159 |  | nnre 12273 | . . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 160 |  | nngt0 12297 | . . . . 5
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) | 
| 161 | 159, 160 | jca 511 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) | 
| 162 |  | 1red 11262 | . . . 4
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) | 
| 163 |  | nnre 12273 | . . . . . 6
⊢ (((𝑁 + 1) · (𝑁 + 1)) ∈ ℕ →
((𝑁 + 1) · (𝑁 + 1)) ∈
ℝ) | 
| 164 |  | nngt0 12297 | . . . . . 6
⊢ (((𝑁 + 1) · (𝑁 + 1)) ∈ ℕ → 0
< ((𝑁 + 1) ·
(𝑁 + 1))) | 
| 165 | 163, 164 | jca 511 | . . . . 5
⊢ (((𝑁 + 1) · (𝑁 + 1)) ∈ ℕ →
(((𝑁 + 1) · (𝑁 + 1)) ∈ ℝ ∧ 0
< ((𝑁 + 1) ·
(𝑁 + 1)))) | 
| 166 | 23, 165 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) · (𝑁 + 1)) ∈ ℝ ∧ 0
< ((𝑁 + 1) ·
(𝑁 + 1)))) | 
| 167 |  | lt2mul2div 12146 | . . . 4
⊢
(((((𝑁 + 1) + 1)
∈ ℝ ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) ∧ (1 ∈ ℝ ∧ (((𝑁 + 1) · (𝑁 + 1)) ∈ ℝ ∧ 0
< ((𝑁 + 1) ·
(𝑁 + 1))))) →
((((𝑁 + 1) + 1) ·
𝑁) < (1 · ((𝑁 + 1) · (𝑁 + 1))) ↔ (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1))) < (1 / 𝑁))) | 
| 168 | 22, 161, 162, 166, 167 | syl22anc 839 | . . 3
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) + 1) · 𝑁) < (1 · ((𝑁 + 1) · (𝑁 + 1))) ↔ (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1))) < (1 / 𝑁))) | 
| 169 | 158, 168 | mpbid 232 | . 2
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) + 1) / ((𝑁 + 1) · (𝑁 + 1))) < (1 / 𝑁)) | 
| 170 | 19, 24, 25, 137, 169 | lelttrd 11419 | 1
⊢ (𝑁 ∈ ℕ →
(abs‘(((!‘𝑁) /
e) − (𝑆‘𝑁))) < (1 / 𝑁)) |