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 35381

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 6834	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
2		derang.d	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
3		subfac.n	. . . . . . 7 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
4	2, 3	subfac0 35371	. . . . . 6 ⊢ (𝑆‘0) = 1
5	1, 4	eqtrdi 2787	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = 1)
6		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘𝑥) = (!‘0))
7		fac0 14199	. . . . . . 7 ⊢ (!‘0) = 1
8	6, 7	eqtrdi 2787	. . . . . 6 ⊢ (𝑥 = 0 → (!‘𝑥) = 1)
9		oveq2 7366	. . . . . . 7 ⊢ (𝑥 = 0 → (0...𝑥) = (0...0))
10	9	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
11	8, 10	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 0 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))))
12	5, 11	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))))
13		fv0p1e1 12263	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = (𝑆‘1))
14	2, 3	subfac1 35372	. . . . . 6 ⊢ (𝑆‘1) = 0
15	13, 14	eqtrdi 2787	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = 0)
16		fv0p1e1 12263	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = (!‘1))
17		fac1 14200	. . . . . . 7 ⊢ (!‘1) = 1
18	16, 17	eqtrdi 2787	. . . . . 6 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1)
19		oveq1 7365	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
20		0p1e1 12262	. . . . . . . . 9 ⊢ (0 + 1) = 1
21	19, 20	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
22	21	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 0 → (0...(𝑥 + 1)) = (0...1))
23	22	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
24	18, 23	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 0 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
25	15, 24	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))))
26	12, 25	anbi12d 632	. . 3 ⊢ (𝑥 = 0 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))))
27		fveq2 6834	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘𝑥) = (𝑆‘𝑚))
28		fveq2 6834	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘𝑥) = (!‘𝑚))
29		oveq2 7366	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...𝑥) = (0...𝑚))
30	29	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))
31	28, 30	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
32	27, 31	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
33		fvoveq1 7381	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑚 + 1)))
34		fvoveq1 7381	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘(𝑥 + 1)) = (!‘(𝑚 + 1)))
35		oveq1 7365	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 + 1) = (𝑚 + 1))
36	35	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...(𝑥 + 1)) = (0...(𝑚 + 1)))
37	36	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
38	34, 37	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
39	33, 38	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
40	32, 39	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑚 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))))
41		fveq2 6834	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘𝑥) = (𝑆‘(𝑚 + 1)))
42		fveq2 6834	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘𝑥) = (!‘(𝑚 + 1)))
43		oveq2 7366	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...𝑥) = (0...(𝑚 + 1)))
44	43	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
45	42, 44	oveq12d 7376	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
46	41, 45	eqeq12d 2752	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
47		fvoveq1 7381	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘(𝑥 + 1)) = (𝑆‘((𝑚 + 1) + 1)))
48		fvoveq1 7381	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘(𝑥 + 1)) = (!‘((𝑚 + 1) + 1)))
49		oveq1 7365	. . . . . . . 8 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 + 1) = ((𝑚 + 1) + 1))
50	49	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...(𝑥 + 1)) = (0...((𝑚 + 1) + 1)))
51	50	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))
52	48, 51	oveq12d 7376	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))
53	47, 52	eqeq12d 2752	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
54	46, 53	anbi12d 632	. . 3 ⊢ (𝑥 = (𝑚 + 1) → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
55		fveq2 6834	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
56		fveq2 6834	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
57		oveq2 7366	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
58	57	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))
59	56, 58	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
60	55, 59	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))))
61		fvoveq1 7381	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑁 + 1)))
62		fvoveq1 7381	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘(𝑥 + 1)) = (!‘(𝑁 + 1)))
63		oveq1 7365	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
64	63	oveq2d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...(𝑥 + 1)) = (0...(𝑁 + 1)))
65	64	sumeq1d 15623	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))
66	62, 65	oveq12d 7376	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))
67	61, 66	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
68	60, 67	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑁 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))))
69		0z 12499	. . . . . . 7 ⊢ 0 ∈ ℤ
70		ax-1cn 11084	. . . . . . 7 ⊢ 1 ∈ ℂ
71		oveq2 7366	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
72		neg1cn 12130	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
73		exp0 13988	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ (-1↑0) = 1
75	71, 74	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (-1↑𝑘) = 1)
76		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
77	76, 7	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
78	75, 77	oveq12d 7376	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = (1 / 1))
79	70	div1i 11869	. . . . . . . . 9 ⊢ (1 / 1) = 1
80	78, 79	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = 1)
81	80	fsum1 15670	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
82	69, 70, 81	mp2an 692	. . . . . 6 ⊢ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1
83	82	oveq2i 7369	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) = (1 · 1)
84		1t1e1 12302	. . . . 5 ⊢ (1 · 1) = 1
85	83, 84	eqtr2i 2760	. . . 4 ⊢ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
86		nn0uz 12789	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
87		1e0p1 12649	. . . . . . . . 9 ⊢ 1 = (0 + 1)
88		oveq2 7366	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (-1↑𝑘) = (-1↑1))
89		exp1 13990	. . . . . . . . . . . . 13 ⊢ (-1 ∈ ℂ → (-1↑1) = -1)
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 ⊢ (-1↑1) = -1
91	88, 90	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (-1↑𝑘) = -1)
92		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (!‘𝑘) = (!‘1))
93	92, 17	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (!‘𝑘) = 1)
94	91, 93	oveq12d 7376	. . . . . . . . . 10 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = (-1 / 1))
95	72	div1i 11869	. . . . . . . . . 10 ⊢ (-1 / 1) = -1
96	94, 95	eqtrdi 2787	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = -1)
97		neg1rr 12131	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
98		reexpcl 14001	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℝ)
99	97, 98	mpan 690	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (-1↑𝑘) ∈ ℝ)
100		faccl 14206	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (!‘𝑘) ∈ ℕ)
101	99, 100	nndivred 12199	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℝ)
102	101	recnd 11160	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
103	102	adantl 481	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
104		0nn0 12416	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
105	104, 82	pm3.2i 470	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
106	105	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1))
107		1pneg1e0 12259	. . . . . . . . . 10 ⊢ (1 + -1) = 0
108	107	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (1 + -1) = 0)
109	86, 87, 96, 103, 106, 108	fsump1i 15692	. . . . . . . 8 ⊢ (⊤ → (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0))
110	109	mptru 1548	. . . . . . 7 ⊢ (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0)
111	110	simpri 485	. . . . . 6 ⊢ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0
112	111	oveq2i 7369	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))) = (1 · 0)
113	70	mul01i 11323	. . . . 5 ⊢ (1 · 0) = 0
114	112, 113	eqtr2i 2760	. . . 4 ⊢ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
115	85, 114	pm3.2i 470	. . 3 ⊢ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
116		simpr 484	. . . . 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 7367	. . . . . . 7 ⊢ (((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
119	118	ancoms 458	. . . . . 6 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
120	119	oveq2d 7374	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
121		nn0p1nn 12440	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
122	2, 3	subfacp1 35380	. . . . . . . 8 ⊢ ((𝑚 + 1) ∈ ℕ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
123	121, 122	syl 17	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
124		nn0cn 12411	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
125		pncan 11386	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
126	124, 70, 125	sylancl 586	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) − 1) = 𝑚)
127	126	fveq2d 6838	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) − 1)) = (𝑆‘𝑚))
128	127	oveq2d 7374	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1))) = ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)))
129	128	oveq2d 7374	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
130	123, 129	eqtrd 2771	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
131		peano2nn0 12441	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
132		peano2nn0 12441	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
133	131, 132	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
134		faccl 14206	. . . . . . . . . . 11 ⊢ (((𝑚 + 1) + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
135	133, 134	syl 17	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
136	135	nncnd 12161	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℂ)
137		fzfid 13896	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (0...(𝑚 + 1)) ∈ Fin)
138		elfznn0 13536	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑚 + 1)) → 𝑘 ∈ ℕ₀)
139	138	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → 𝑘 ∈ ℕ₀)
140	139, 102	syl 17	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
141	137, 140	fsumcl 15656	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
142		expcl 14002	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ ((𝑚 + 1) + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
143	72, 133, 142	sylancr 587	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
144	135	nnne0d 12195	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ≠ 0)
145	143, 136, 144	divcld 11917	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))) ∈ ℂ)
146	136, 141, 145	adddid 11156	. . . . . . . 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 2846	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ (ℤ_≥‘0))
149		oveq2 7366	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (-1↑𝑘) = (-1↑(𝑚 + 1)))
150		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (!‘𝑘) = (!‘(𝑚 + 1)))
151	149, 150	oveq12d 7376	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑚 + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))
152	148, 140, 151	fsump1 15679	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))))
153	152	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
154		fzfid 13896	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (0...𝑚) ∈ Fin)
155		elfznn0 13536	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ₀)
156	155	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ₀)
157	156, 102	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
158	154, 157	fsumcl 15656	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
159		expcl 14002	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑(𝑚 + 1)) ∈ ℂ)
160	72, 131, 159	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑(𝑚 + 1)) ∈ ℂ)
161		faccl 14206	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
162	131, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
163	162	nncnd 12161	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℂ)
164	162	nnne0d 12195	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ≠ 0)
165	160, 163, 164	divcld 11917	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))) ∈ ℂ)
166	136, 158, 165	adddid 11156	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
167		facp1 14201	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
168	131, 167	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
169		facp1 14201	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1)))
170		faccl 14206	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℕ)
171	170	nncnd 12161	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℂ)
172	121	nncnd 12161	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
173	171, 172	mulcomd 11153	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
174	169, 173	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
175	174	oveq1d 7373	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) = (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)))
176	133	nn0cnd 12464	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℂ)
177	172, 171, 176	mulassd 11155	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
178	168, 175, 177	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
179	178	oveq1d 7373	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
180	136, 160, 163, 164	div12d 11953	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))))
181	168	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))))
182	176, 163, 164	divcan3d 11922	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
183	181, 182	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
184	183	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
185	180, 184	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
186	179, 185	oveq12d 7376	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
187	153, 166, 186	3eqtrd 2775	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
188	143, 136, 144	divcan2d 11919	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))) = (-1↑((𝑚 + 1) + 1)))
189	187, 188	oveq12d 7376	. . . . . . . 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 11152	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) ∈ ℂ)
191	172, 190, 158	mulassd 11155	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
192	72	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
193	160, 176, 192	adddid 11156	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
194		negsub 11429	. . . . . . . . . . . . . . 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 11386	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
197	172, 70, 196	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
198	195, 197	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (𝑚 + 1))
199	198	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
200	193, 199	eqtr3d 2773	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
201		expp1 13991	. . . . . . . . . . . . 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 7374	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
204	172, 160	mulcomd 11153	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (-1↑(𝑚 + 1))) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
205	200, 203, 204	3eqtr4d 2781	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · (-1↑(𝑚 + 1))))
206	191, 205	oveq12d 7376	. . . . . . . . 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 11152	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) ∈ ℂ)
208	207, 158	mulcld 11152	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
209	160, 176	mulcld 11152	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) ∈ ℂ)
210	208, 209, 143	addassd 11154	. . . . . . . . 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 11152	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
212	172, 211, 160	adddid 11156	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · (-1↑(𝑚 + 1)))))
213	206, 210, 212	3eqtr4d 2781	. . . . . . . 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 2775	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
215	131, 86	eleqtrdi 2846	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ (ℤ_≥‘0))
216		elfznn0 13536	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((𝑚 + 1) + 1)) → 𝑘 ∈ ℕ₀)
217	216	adantl 481	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → 𝑘 ∈ ℕ₀)
218	217, 102	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
219		oveq2 7366	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (-1↑𝑘) = (-1↑((𝑚 + 1) + 1)))
220		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (!‘𝑘) = (!‘((𝑚 + 1) + 1)))
221	219, 220	oveq12d 7376	. . . . . . . . 9 ⊢ (𝑘 = ((𝑚 + 1) + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))
222	215, 218, 221	fsump1 15679	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))))
223	222	oveq2d 7374	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
224	163, 158	mulcld 11152	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
225	171, 158	mulcld 11152	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
226	224, 160, 225	add32d 11361	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
227	152	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
228	163, 158, 165	adddid 11156	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
229	160, 163, 164	divcan2d 11919	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (-1↑(𝑚 + 1)))
230	229	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
231	227, 228, 230	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
232	231	oveq1d 7373	. . . . . . . . 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 11156	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)))
235	169	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = (!‘(𝑚 + 1)))
236	171	mulridd 11149	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · 1) = (!‘𝑚))
237	235, 236	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
238	234, 237	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
239	238	oveq1d 7373	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
240	163, 171, 158	adddird 11157	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
241	239, 240	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
242	241	oveq1d 7373	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
243	226, 232, 242	3eqtr4d 2781	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
244	243	oveq2d 7374	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
245	214, 223, 244	3eqtr4d 2781	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
246	130, 245	eqeq12d 2752	. . . . 5 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) ↔ ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))))
247	120, 246	imbitrrid 246	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
248	117, 247	jcad 512	. . 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 12587	. 2 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
250	249	simpld 494	1 ⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 {cab 2714 ≠ wne 2932 ∀wral 3051 ↦ cmpt 5179 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7358 Fincfn 8883 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 − cmin 11364 -cneg 11365 / cdiv 11794 ℕcn 12145 ℕ₀cn0 12401 ℤcz 12488 ℤ_≥cuz 12751 ...cfz 13423 ↑cexp 13984 !cfa 14196 ♯chash 14253 Σcsu 15609

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-er 8635 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-oi 9415 df-dju 9813 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-n0 12402 df-xnn0 12475 df-z 12489 df-uz 12752 df-rp 12906 df-fz 13424 df-fzo 13571 df-seq 13925 df-exp 13985 df-fac 14197 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-sum 15610

This theorem is referenced by: subfaclim 35382

W3C validator