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 34853

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 6891	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
2		derang.d	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
3		subfac.n	. . . . . . 7 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
4	2, 3	subfac0 34843	. . . . . 6 ⊢ (𝑆‘0) = 1
5	1, 4	eqtrdi 2781	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = 1)
6		fveq2 6891	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘𝑥) = (!‘0))
7		fac0 14265	. . . . . . 7 ⊢ (!‘0) = 1
8	6, 7	eqtrdi 2781	. . . . . 6 ⊢ (𝑥 = 0 → (!‘𝑥) = 1)
9		oveq2 7423	. . . . . . 7 ⊢ (𝑥 = 0 → (0...𝑥) = (0...0))
10	9	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
11	8, 10	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 0 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))))
12	5, 11	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))))
13		fv0p1e1 12363	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = (𝑆‘1))
14	2, 3	subfac1 34844	. . . . . 6 ⊢ (𝑆‘1) = 0
15	13, 14	eqtrdi 2781	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = 0)
16		fv0p1e1 12363	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = (!‘1))
17		fac1 14266	. . . . . . 7 ⊢ (!‘1) = 1
18	16, 17	eqtrdi 2781	. . . . . 6 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1)
19		oveq1 7422	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
20		0p1e1 12362	. . . . . . . . 9 ⊢ (0 + 1) = 1
21	19, 20	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
22	21	oveq2d 7431	. . . . . . 7 ⊢ (𝑥 = 0 → (0...(𝑥 + 1)) = (0...1))
23	22	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
24	18, 23	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 0 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
25	15, 24	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))))
26	12, 25	anbi12d 630	. . 3 ⊢ (𝑥 = 0 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))))
27		fveq2 6891	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘𝑥) = (𝑆‘𝑚))
28		fveq2 6891	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘𝑥) = (!‘𝑚))
29		oveq2 7423	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...𝑥) = (0...𝑚))
30	29	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))
31	28, 30	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
32	27, 31	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
33		fvoveq1 7438	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑚 + 1)))
34		fvoveq1 7438	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘(𝑥 + 1)) = (!‘(𝑚 + 1)))
35		oveq1 7422	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 + 1) = (𝑚 + 1))
36	35	oveq2d 7431	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...(𝑥 + 1)) = (0...(𝑚 + 1)))
37	36	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
38	34, 37	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
39	33, 38	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
40	32, 39	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑚 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))))
41		fveq2 6891	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘𝑥) = (𝑆‘(𝑚 + 1)))
42		fveq2 6891	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘𝑥) = (!‘(𝑚 + 1)))
43		oveq2 7423	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...𝑥) = (0...(𝑚 + 1)))
44	43	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
45	42, 44	oveq12d 7433	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
46	41, 45	eqeq12d 2741	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
47		fvoveq1 7438	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘(𝑥 + 1)) = (𝑆‘((𝑚 + 1) + 1)))
48		fvoveq1 7438	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘(𝑥 + 1)) = (!‘((𝑚 + 1) + 1)))
49		oveq1 7422	. . . . . . . 8 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 + 1) = ((𝑚 + 1) + 1))
50	49	oveq2d 7431	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...(𝑥 + 1)) = (0...((𝑚 + 1) + 1)))
51	50	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))
52	48, 51	oveq12d 7433	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))
53	47, 52	eqeq12d 2741	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
54	46, 53	anbi12d 630	. . 3 ⊢ (𝑥 = (𝑚 + 1) → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
55		fveq2 6891	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
56		fveq2 6891	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
57		oveq2 7423	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
58	57	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))
59	56, 58	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
60	55, 59	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))))
61		fvoveq1 7438	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑁 + 1)))
62		fvoveq1 7438	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘(𝑥 + 1)) = (!‘(𝑁 + 1)))
63		oveq1 7422	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
64	63	oveq2d 7431	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...(𝑥 + 1)) = (0...(𝑁 + 1)))
65	64	sumeq1d 15677	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))
66	62, 65	oveq12d 7433	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))
67	61, 66	eqeq12d 2741	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
68	60, 67	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑁 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))))
69		0z 12597	. . . . . . 7 ⊢ 0 ∈ ℤ
70		ax-1cn 11194	. . . . . . 7 ⊢ 1 ∈ ℂ
71		oveq2 7423	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
72		neg1cn 12354	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
73		exp0 14060	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ (-1↑0) = 1
75	71, 74	eqtrdi 2781	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (-1↑𝑘) = 1)
76		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
77	76, 7	eqtrdi 2781	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
78	75, 77	oveq12d 7433	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = (1 / 1))
79	70	div1i 11970	. . . . . . . . 9 ⊢ (1 / 1) = 1
80	78, 79	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = 1)
81	80	fsum1 15723	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
82	69, 70, 81	mp2an 690	. . . . . 6 ⊢ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1
83	82	oveq2i 7426	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) = (1 · 1)
84		1t1e1 12402	. . . . 5 ⊢ (1 · 1) = 1
85	83, 84	eqtr2i 2754	. . . 4 ⊢ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
86		nn0uz 12892	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
87		1e0p1 12747	. . . . . . . . 9 ⊢ 1 = (0 + 1)
88		oveq2 7423	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (-1↑𝑘) = (-1↑1))
89		exp1 14062	. . . . . . . . . . . . 13 ⊢ (-1 ∈ ℂ → (-1↑1) = -1)
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 ⊢ (-1↑1) = -1
91	88, 90	eqtrdi 2781	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (-1↑𝑘) = -1)
92		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (!‘𝑘) = (!‘1))
93	92, 17	eqtrdi 2781	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (!‘𝑘) = 1)
94	91, 93	oveq12d 7433	. . . . . . . . . 10 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = (-1 / 1))
95	72	div1i 11970	. . . . . . . . . 10 ⊢ (-1 / 1) = -1
96	94, 95	eqtrdi 2781	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = -1)
97		neg1rr 12355	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
98		reexpcl 14073	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℝ)
99	97, 98	mpan 688	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (-1↑𝑘) ∈ ℝ)
100		faccl 14272	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (!‘𝑘) ∈ ℕ)
101	99, 100	nndivred 12294	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℝ)
102	101	recnd 11270	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
103	102	adantl 480	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
104		0nn0 12515	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
105	104, 82	pm3.2i 469	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
106	105	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1))
107		1pneg1e0 12359	. . . . . . . . . 10 ⊢ (1 + -1) = 0
108	107	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (1 + -1) = 0)
109	86, 87, 96, 103, 106, 108	fsump1i 15745	. . . . . . . 8 ⊢ (⊤ → (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0))
110	109	mptru 1540	. . . . . . 7 ⊢ (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0)
111	110	simpri 484	. . . . . 6 ⊢ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0
112	111	oveq2i 7426	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))) = (1 · 0)
113	70	mul01i 11432	. . . . 5 ⊢ (1 · 0) = 0
114	112, 113	eqtr2i 2754	. . . 4 ⊢ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
115	85, 114	pm3.2i 469	. . 3 ⊢ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
116		simpr 483	. . . . 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 7424	. . . . . . 7 ⊢ (((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
119	118	ancoms 457	. . . . . 6 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
120	119	oveq2d 7431	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
121		nn0p1nn 12539	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
122	2, 3	subfacp1 34852	. . . . . . . 8 ⊢ ((𝑚 + 1) ∈ ℕ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
123	121, 122	syl 17	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
124		nn0cn 12510	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
125		pncan 11494	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
126	124, 70, 125	sylancl 584	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) − 1) = 𝑚)
127	126	fveq2d 6895	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) − 1)) = (𝑆‘𝑚))
128	127	oveq2d 7431	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1))) = ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)))
129	128	oveq2d 7431	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
130	123, 129	eqtrd 2765	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
131		peano2nn0 12540	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
132		peano2nn0 12540	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
133	131, 132	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
134		faccl 14272	. . . . . . . . . . 11 ⊢ (((𝑚 + 1) + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
135	133, 134	syl 17	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
136	135	nncnd 12256	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℂ)
137		fzfid 13968	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (0...(𝑚 + 1)) ∈ Fin)
138		elfznn0 13624	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑚 + 1)) → 𝑘 ∈ ℕ₀)
139	138	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → 𝑘 ∈ ℕ₀)
140	139, 102	syl 17	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
141	137, 140	fsumcl 15709	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
142		expcl 14074	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ ((𝑚 + 1) + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
143	72, 133, 142	sylancr 585	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
144	135	nnne0d 12290	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ≠ 0)
145	143, 136, 144	divcld 12018	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))) ∈ ℂ)
146	136, 141, 145	adddid 11266	. . . . . . . 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 2835	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ (ℤ_≥‘0))
149		oveq2 7423	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (-1↑𝑘) = (-1↑(𝑚 + 1)))
150		fveq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (!‘𝑘) = (!‘(𝑚 + 1)))
151	149, 150	oveq12d 7433	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑚 + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))
152	148, 140, 151	fsump1 15732	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))))
153	152	oveq2d 7431	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
154		fzfid 13968	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (0...𝑚) ∈ Fin)
155		elfznn0 13624	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ₀)
156	155	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ₀)
157	156, 102	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
158	154, 157	fsumcl 15709	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
159		expcl 14074	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑(𝑚 + 1)) ∈ ℂ)
160	72, 131, 159	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑(𝑚 + 1)) ∈ ℂ)
161		faccl 14272	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
162	131, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
163	162	nncnd 12256	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℂ)
164	162	nnne0d 12290	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ≠ 0)
165	160, 163, 164	divcld 12018	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))) ∈ ℂ)
166	136, 158, 165	adddid 11266	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
167		facp1 14267	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
168	131, 167	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
169		facp1 14267	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1)))
170		faccl 14272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℕ)
171	170	nncnd 12256	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℂ)
172	121	nncnd 12256	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
173	171, 172	mulcomd 11263	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
174	169, 173	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
175	174	oveq1d 7430	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) = (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)))
176	133	nn0cnd 12562	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℂ)
177	172, 171, 176	mulassd 11265	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
178	168, 175, 177	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
179	178	oveq1d 7430	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
180	136, 160, 163, 164	div12d 12054	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))))
181	168	oveq1d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))))
182	176, 163, 164	divcan3d 12023	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
183	181, 182	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
184	183	oveq2d 7431	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
185	180, 184	eqtrd 2765	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
186	179, 185	oveq12d 7433	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
187	153, 166, 186	3eqtrd 2769	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
188	143, 136, 144	divcan2d 12020	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))) = (-1↑((𝑚 + 1) + 1)))
189	187, 188	oveq12d 7433	. . . . . . . 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 11262	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) ∈ ℂ)
191	172, 190, 158	mulassd 11265	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
192	72	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
193	160, 176, 192	adddid 11266	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
194		negsub 11536	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 + 1) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
195	176, 70, 194	sylancl 584	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
196		pncan 11494	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
197	172, 70, 196	sylancl 584	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
198	195, 197	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (𝑚 + 1))
199	198	oveq2d 7431	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
200	193, 199	eqtr3d 2767	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
201		expp1 14063	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
202	72, 131, 201	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
203	202	oveq2d 7431	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
204	172, 160	mulcomd 11263	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (-1↑(𝑚 + 1))) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
205	200, 203, 204	3eqtr4d 2775	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · (-1↑(𝑚 + 1))))
206	191, 205	oveq12d 7433	. . . . . . . . 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 11262	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) ∈ ℂ)
208	207, 158	mulcld 11262	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
209	160, 176	mulcld 11262	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) ∈ ℂ)
210	208, 209, 143	addassd 11264	. . . . . . . . 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 11262	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
212	172, 211, 160	adddid 11266	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · (-1↑(𝑚 + 1)))))
213	206, 210, 212	3eqtr4d 2775	. . . . . . . 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 2769	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
215	131, 86	eleqtrdi 2835	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ (ℤ_≥‘0))
216		elfznn0 13624	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((𝑚 + 1) + 1)) → 𝑘 ∈ ℕ₀)
217	216	adantl 480	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → 𝑘 ∈ ℕ₀)
218	217, 102	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
219		oveq2 7423	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (-1↑𝑘) = (-1↑((𝑚 + 1) + 1)))
220		fveq2 6891	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (!‘𝑘) = (!‘((𝑚 + 1) + 1)))
221	219, 220	oveq12d 7433	. . . . . . . . 9 ⊢ (𝑘 = ((𝑚 + 1) + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))
222	215, 218, 221	fsump1 15732	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))))
223	222	oveq2d 7431	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
224	163, 158	mulcld 11262	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
225	171, 158	mulcld 11262	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
226	224, 160, 225	add32d 11469	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
227	152	oveq2d 7431	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
228	163, 158, 165	adddid 11266	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
229	160, 163, 164	divcan2d 12020	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (-1↑(𝑚 + 1)))
230	229	oveq2d 7431	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
231	227, 228, 230	3eqtrd 2769	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
232	231	oveq1d 7430	. . . . . . . . 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 11266	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)))
235	169	eqcomd 2731	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = (!‘(𝑚 + 1)))
236	171	mulridd 11259	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · 1) = (!‘𝑚))
237	235, 236	oveq12d 7433	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
238	234, 237	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
239	238	oveq1d 7430	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
240	163, 171, 158	adddird 11267	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
241	239, 240	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
242	241	oveq1d 7430	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
243	226, 232, 242	3eqtr4d 2775	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
244	243	oveq2d 7431	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
245	214, 223, 244	3eqtr4d 2775	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
246	130, 245	eqeq12d 2741	. . . . 5 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) ↔ ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))))
247	120, 246	imbitrrid 245	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
248	117, 247	jcad 511	. . 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 12685	. 2 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
250	249	simpld 493	1 ⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 {cab 2702 ≠ wne 2930 ∀wral 3051 ↦ cmpt 5226 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7415 Fincfn 8960 ℂcc 11134 ℝcr 11135 0cc0 11136 1c1 11137 + caddc 11139 · cmul 11141 − cmin 11472 -cneg 11473 / cdiv 11899 ℕcn 12240 ℕ₀cn0 12500 ℤcz 12586 ℤ_≥cuz 12850 ...cfz 13514 ↑cexp 14056 !cfa 14262 ♯chash 14319 Σcsu 15662

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737 ax-inf2 9662 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3960 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7371 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7868 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8388 df-rdg 8427 df-1o 8483 df-oadd 8487 df-er 8721 df-map 8843 df-pm 8844 df-en 8961 df-dom 8962 df-sdom 8963 df-fin 8964 df-sup 9463 df-oi 9531 df-dju 9922 df-card 9960 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11474 df-neg 11475 df-div 11900 df-nn 12241 df-2 12303 df-3 12304 df-n0 12501 df-xnn0 12573 df-z 12587 df-uz 12851 df-rp 13005 df-fz 13515 df-fzo 13658 df-seq 13997 df-exp 14057 df-fac 14263 df-hash 14320 df-cj 15076 df-re 15077 df-im 15078 df-sqrt 15212 df-abs 15213 df-clim 15462 df-sum 15663

This theorem is referenced by: subfaclim 34854

W3C validator