subfacval2 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > subfacval2		Structured version Visualization version GIF version

Theorem subfacval2 33149

Description: A closed-form expression for the subfactorial. (Contributed by Mario Carneiro, 23-Jan-2015.)

**Hypotheses**
Ref	Expression
derang.d	⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
subfac.n	⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))

**Assertion**
Ref	Expression
subfacval2	⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))

Distinct variable groups: 𝑓,𝑛,𝑥,𝑦,𝑘,𝑁 𝐷,𝑛 𝑆,𝑛,𝑥,𝑦 Allowed substitution hints: 𝐷(𝑥,𝑦,𝑓,𝑘) 𝑆(𝑓,𝑘)

Proof of Theorem subfacval2 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6774	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
2		derang.d	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
3		subfac.n	. . . . . . 7 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
4	2, 3	subfac0 33139	. . . . . 6 ⊢ (𝑆‘0) = 1
5	1, 4	eqtrdi 2794	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = 1)
6		fveq2 6774	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘𝑥) = (!‘0))
7		fac0 13990	. . . . . . 7 ⊢ (!‘0) = 1
8	6, 7	eqtrdi 2794	. . . . . 6 ⊢ (𝑥 = 0 → (!‘𝑥) = 1)
9		oveq2 7283	. . . . . . 7 ⊢ (𝑥 = 0 → (0...𝑥) = (0...0))
10	9	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
11	8, 10	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 0 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))))
12	5, 11	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))))
13		fv0p1e1 12096	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = (𝑆‘1))
14	2, 3	subfac1 33140	. . . . . 6 ⊢ (𝑆‘1) = 0
15	13, 14	eqtrdi 2794	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = 0)
16		fv0p1e1 12096	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = (!‘1))
17		fac1 13991	. . . . . . 7 ⊢ (!‘1) = 1
18	16, 17	eqtrdi 2794	. . . . . 6 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1)
19		oveq1 7282	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
20		0p1e1 12095	. . . . . . . . 9 ⊢ (0 + 1) = 1
21	19, 20	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
22	21	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 0 → (0...(𝑥 + 1)) = (0...1))
23	22	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
24	18, 23	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 0 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
25	15, 24	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))))
26	12, 25	anbi12d 631	. . 3 ⊢ (𝑥 = 0 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))))
27		fveq2 6774	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘𝑥) = (𝑆‘𝑚))
28		fveq2 6774	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘𝑥) = (!‘𝑚))
29		oveq2 7283	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...𝑥) = (0...𝑚))
30	29	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))
31	28, 30	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
32	27, 31	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
33		fvoveq1 7298	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑚 + 1)))
34		fvoveq1 7298	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘(𝑥 + 1)) = (!‘(𝑚 + 1)))
35		oveq1 7282	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 + 1) = (𝑚 + 1))
36	35	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...(𝑥 + 1)) = (0...(𝑚 + 1)))
37	36	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
38	34, 37	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
39	33, 38	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
40	32, 39	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑚 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))))
41		fveq2 6774	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘𝑥) = (𝑆‘(𝑚 + 1)))
42		fveq2 6774	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘𝑥) = (!‘(𝑚 + 1)))
43		oveq2 7283	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...𝑥) = (0...(𝑚 + 1)))
44	43	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
45	42, 44	oveq12d 7293	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
46	41, 45	eqeq12d 2754	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
47		fvoveq1 7298	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘(𝑥 + 1)) = (𝑆‘((𝑚 + 1) + 1)))
48		fvoveq1 7298	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘(𝑥 + 1)) = (!‘((𝑚 + 1) + 1)))
49		oveq1 7282	. . . . . . . 8 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 + 1) = ((𝑚 + 1) + 1))
50	49	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...(𝑥 + 1)) = (0...((𝑚 + 1) + 1)))
51	50	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))
52	48, 51	oveq12d 7293	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))
53	47, 52	eqeq12d 2754	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
54	46, 53	anbi12d 631	. . 3 ⊢ (𝑥 = (𝑚 + 1) → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
55		fveq2 6774	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
56		fveq2 6774	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
57		oveq2 7283	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
58	57	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))
59	56, 58	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
60	55, 59	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))))
61		fvoveq1 7298	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑁 + 1)))
62		fvoveq1 7298	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘(𝑥 + 1)) = (!‘(𝑁 + 1)))
63		oveq1 7282	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
64	63	oveq2d 7291	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...(𝑥 + 1)) = (0...(𝑁 + 1)))
65	64	sumeq1d 15413	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))
66	62, 65	oveq12d 7293	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))
67	61, 66	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
68	60, 67	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑁 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))))
69		0z 12330	. . . . . . 7 ⊢ 0 ∈ ℤ
70		ax-1cn 10929	. . . . . . 7 ⊢ 1 ∈ ℂ
71		oveq2 7283	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
72		neg1cn 12087	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
73		exp0 13786	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ (-1↑0) = 1
75	71, 74	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (-1↑𝑘) = 1)
76		fveq2 6774	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
77	76, 7	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
78	75, 77	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = (1 / 1))
79	70	div1i 11703	. . . . . . . . 9 ⊢ (1 / 1) = 1
80	78, 79	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = 1)
81	80	fsum1 15459	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
82	69, 70, 81	mp2an 689	. . . . . 6 ⊢ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1
83	82	oveq2i 7286	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) = (1 · 1)
84		1t1e1 12135	. . . . 5 ⊢ (1 · 1) = 1
85	83, 84	eqtr2i 2767	. . . 4 ⊢ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
86		nn0uz 12620	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
87		1e0p1 12479	. . . . . . . . 9 ⊢ 1 = (0 + 1)
88		oveq2 7283	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (-1↑𝑘) = (-1↑1))
89		exp1 13788	. . . . . . . . . . . . 13 ⊢ (-1 ∈ ℂ → (-1↑1) = -1)
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 ⊢ (-1↑1) = -1
91	88, 90	eqtrdi 2794	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (-1↑𝑘) = -1)
92		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (!‘𝑘) = (!‘1))
93	92, 17	eqtrdi 2794	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (!‘𝑘) = 1)
94	91, 93	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = (-1 / 1))
95	72	div1i 11703	. . . . . . . . . 10 ⊢ (-1 / 1) = -1
96	94, 95	eqtrdi 2794	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = -1)
97		neg1rr 12088	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
98		reexpcl 13799	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℝ)
99	97, 98	mpan 687	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (-1↑𝑘) ∈ ℝ)
100		faccl 13997	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (!‘𝑘) ∈ ℕ)
101	99, 100	nndivred 12027	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℝ)
102	101	recnd 11003	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
103	102	adantl 482	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
104		0nn0 12248	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
105	104, 82	pm3.2i 471	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
106	105	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1))
107		1pneg1e0 12092	. . . . . . . . . 10 ⊢ (1 + -1) = 0
108	107	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (1 + -1) = 0)
109	86, 87, 96, 103, 106, 108	fsump1i 15481	. . . . . . . 8 ⊢ (⊤ → (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0))
110	109	mptru 1546	. . . . . . 7 ⊢ (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0)
111	110	simpri 486	. . . . . 6 ⊢ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0
112	111	oveq2i 7286	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))) = (1 · 0)
113	70	mul01i 11165	. . . . 5 ⊢ (1 · 0) = 0
114	112, 113	eqtr2i 2767	. . . 4 ⊢ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
115	85, 114	pm3.2i 471	. . 3 ⊢ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
116		simpr 485	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
117	116	a1i 11	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
118		oveq12 7284	. . . . . . 7 ⊢ (((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
119	118	ancoms 459	. . . . . 6 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
120	119	oveq2d 7291	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
121		nn0p1nn 12272	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
122	2, 3	subfacp1 33148	. . . . . . . 8 ⊢ ((𝑚 + 1) ∈ ℕ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
123	121, 122	syl 17	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
124		nn0cn 12243	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
125		pncan 11227	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
126	124, 70, 125	sylancl 586	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) − 1) = 𝑚)
127	126	fveq2d 6778	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) − 1)) = (𝑆‘𝑚))
128	127	oveq2d 7291	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1))) = ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)))
129	128	oveq2d 7291	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
130	123, 129	eqtrd 2778	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
131		peano2nn0 12273	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
132		peano2nn0 12273	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
133	131, 132	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
134		faccl 13997	. . . . . . . . . . 11 ⊢ (((𝑚 + 1) + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
135	133, 134	syl 17	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
136	135	nncnd 11989	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℂ)
137		fzfid 13693	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (0...(𝑚 + 1)) ∈ Fin)
138		elfznn0 13349	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑚 + 1)) → 𝑘 ∈ ℕ₀)
139	138	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → 𝑘 ∈ ℕ₀)
140	139, 102	syl 17	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
141	137, 140	fsumcl 15445	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
142		expcl 13800	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ ((𝑚 + 1) + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
143	72, 133, 142	sylancr 587	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
144	135	nnne0d 12023	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ≠ 0)
145	143, 136, 144	divcld 11751	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))) ∈ ℂ)
146	136, 141, 145	adddid 10999	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
147		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℕ₀)
148	147, 86	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ (ℤ_≥‘0))
149		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (-1↑𝑘) = (-1↑(𝑚 + 1)))
150		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (!‘𝑘) = (!‘(𝑚 + 1)))
151	149, 150	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑚 + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))
152	148, 140, 151	fsump1 15468	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))))
153	152	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
154		fzfid 13693	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (0...𝑚) ∈ Fin)
155		elfznn0 13349	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ₀)
156	155	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ₀)
157	156, 102	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
158	154, 157	fsumcl 15445	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
159		expcl 13800	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑(𝑚 + 1)) ∈ ℂ)
160	72, 131, 159	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑(𝑚 + 1)) ∈ ℂ)
161		faccl 13997	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
162	131, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
163	162	nncnd 11989	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℂ)
164	162	nnne0d 12023	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ≠ 0)
165	160, 163, 164	divcld 11751	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))) ∈ ℂ)
166	136, 158, 165	adddid 10999	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
167		facp1 13992	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
168	131, 167	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
169		facp1 13992	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1)))
170		faccl 13997	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℕ)
171	170	nncnd 11989	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℂ)
172	121	nncnd 11989	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
173	171, 172	mulcomd 10996	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
174	169, 173	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
175	174	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) = (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)))
176	133	nn0cnd 12295	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℂ)
177	172, 171, 176	mulassd 10998	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
178	168, 175, 177	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
179	178	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
180	136, 160, 163, 164	div12d 11787	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))))
181	168	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))))
182	176, 163, 164	divcan3d 11756	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
183	181, 182	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
184	183	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
185	180, 184	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
186	179, 185	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
187	153, 166, 186	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
188	143, 136, 144	divcan2d 11753	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))) = (-1↑((𝑚 + 1) + 1)))
189	187, 188	oveq12d 7293	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = (((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))) + (-1↑((𝑚 + 1) + 1))))
190	171, 176	mulcld 10995	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) ∈ ℂ)
191	172, 190, 158	mulassd 10998	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
192	72	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
193	160, 176, 192	adddid 10999	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
194		negsub 11269	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 + 1) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
195	176, 70, 194	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
196		pncan 11227	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
197	172, 70, 196	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
198	195, 197	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (𝑚 + 1))
199	198	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
200	193, 199	eqtr3d 2780	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
201		expp1 13789	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
202	72, 131, 201	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
203	202	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
204	172, 160	mulcomd 10996	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (-1↑(𝑚 + 1))) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
205	200, 203, 204	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · (-1↑(𝑚 + 1))))
206	191, 205	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · (-1↑(𝑚 + 1)))))
207	172, 190	mulcld 10995	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) ∈ ℂ)
208	207, 158	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
209	160, 176	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) ∈ ℂ)
210	208, 209, 143	addassd 10997	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))) + (-1↑((𝑚 + 1) + 1))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1)))))
211	190, 158	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
212	172, 211, 160	adddid 10999	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · (-1↑(𝑚 + 1)))))
213	206, 210, 212	3eqtr4d 2788	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))) + (-1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
214	146, 189, 213	3eqtrd 2782	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
215	131, 86	eleqtrdi 2849	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ (ℤ_≥‘0))
216		elfznn0 13349	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((𝑚 + 1) + 1)) → 𝑘 ∈ ℕ₀)
217	216	adantl 482	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → 𝑘 ∈ ℕ₀)
218	217, 102	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
219		oveq2 7283	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (-1↑𝑘) = (-1↑((𝑚 + 1) + 1)))
220		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (!‘𝑘) = (!‘((𝑚 + 1) + 1)))
221	219, 220	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑘 = ((𝑚 + 1) + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))
222	215, 218, 221	fsump1 15468	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))))
223	222	oveq2d 7291	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
224	163, 158	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
225	171, 158	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
226	224, 160, 225	add32d 11202	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
227	152	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
228	163, 158, 165	adddid 10999	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
229	160, 163, 164	divcan2d 11753	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (-1↑(𝑚 + 1)))
230	229	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
231	227, 228, 230	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
232	231	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
233	70	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → 1 ∈ ℂ)
234	171, 172, 233	adddid 10999	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)))
235	169	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = (!‘(𝑚 + 1)))
236	171	mulid1d 10992	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · 1) = (!‘𝑚))
237	235, 236	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
238	234, 237	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
239	238	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
240	163, 171, 158	adddird 11000	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
241	239, 240	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
242	241	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
243	226, 232, 242	3eqtr4d 2788	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
244	243	oveq2d 7291	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
245	214, 223, 244	3eqtr4d 2788	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
246	130, 245	eqeq12d 2754	. . . . 5 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) ↔ ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))))
247	120, 246	syl5ibr 245	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
248	117, 247	jcad 513	. . 3 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
249	26, 40, 54, 68, 115, 248	nn0ind 12415	. 2 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
250	249	simpld 495	1 ⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 ⊤wtru 1540 ∈ wcel 2106 {cab 2715 ≠ wne 2943 ∀wral 3064 ↦ cmpt 5157 –1-1-onto→wf1o 6432 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 − cmin 11205 -cneg 11206 / cdiv 11632 ℕcn 11973 ℕ₀cn0 12233 ℤcz 12319 ℤ_≥cuz 12582 ...cfz 13239 ↑cexp 13782 !cfa 13987 ♯chash 14044 Σcsu 15397

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-oadd 8301 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-oi 9269 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-xnn0 12306 df-z 12320 df-uz 12583 df-rp 12731 df-fz 13240 df-fzo 13383 df-seq 13722 df-exp 13783 df-fac 13988 df-hash 14045 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-clim 15197 df-sum 15398

This theorem is referenced by: subfaclim 33150

W3C validator