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 36038

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 6885	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
2		derang.d	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
3		subfac.n	. . . . . . 7 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
4	2, 3	subfac0 36028	. . . . . 6 ⊢ (𝑆‘0) = 1
5	1, 4	eqtrdi 2811	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = 1)
6		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘𝑥) = (!‘0))
7		fac0 14423	. . . . . . 7 ⊢ (!‘0) = 1
8	6, 7	eqtrdi 2811	. . . . . 6 ⊢ (𝑥 = 0 → (!‘𝑥) = 1)
9		oveq2 7428	. . . . . . 7 ⊢ (𝑥 = 0 → (0...𝑥) = (0...0))
10	9	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)))
11	8, 10	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 0 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘))))
12	5, 11	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ↔ 1 = (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)))))
13		fv0p1e1 12467	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = (𝑆‘1))
14	2, 3	subfac1 36029	. . . . . 6 ⊢ (𝑆‘1) = 0
15	13, 14	eqtrdi 2811	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = 0)
16		fv0p1e1 12467	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = (!‘1))
17		fac1 14424	. . . . . . 7 ⊢ (!‘1) = 1
18	16, 17	eqtrdi 2811	. . . . . 6 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1)
19		oveq1 7427	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
20		0p1e1 12466	. . . . . . . . 9 ⊢ (0 + 1) = 1
21	19, 20	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
22	21	oveq2d 7436	. . . . . . 7 ⊢ (𝑥 = 0 → (0...(𝑥 + 1)) = (0...1))
23	22	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)))
24	18, 23	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 0 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘))))
25	15, 24	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) ↔ 0 = (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)))))
26	12, 25	anbi12d 644	. . 3 ⊢ (𝑥 = 0 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)))) ↔ (1 = (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘))))))
27		fveq2 6885	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘𝑥) = (𝑆‘𝑚))
28		fveq2 6885	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘𝑥) = (!‘𝑚))
29		oveq2 7428	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...𝑥) = (0...𝑚))
30	29	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))
31	28, 30	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))
32	27, 31	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
33		fvoveq1 7443	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑚 + 1)))
34		fvoveq1 7443	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘(𝑥 + 1)) = (!‘(𝑚 + 1)))
35		oveq1 7427	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 + 1) = (𝑚 + 1))
36	35	oveq2d 7436	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...(𝑥 + 1)) = (0...(𝑚 + 1)))
37	36	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))
38	34, 37	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))))
39	33, 38	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))))
40	32, 39	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑚 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))))))
41		fveq2 6885	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘𝑥) = (𝑆‘(𝑚 + 1)))
42		fveq2 6885	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘𝑥) = (!‘(𝑚 + 1)))
43		oveq2 7428	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...𝑥) = (0...(𝑚 + 1)))
44	43	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))
45	42, 44	oveq12d 7438	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))))
46	41, 45	eqeq12d 2776	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))))
47		fvoveq1 7443	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘(𝑥 + 1)) = (𝑆‘((𝑚 + 1) + 1)))
48		fvoveq1 7443	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘(𝑥 + 1)) = (!‘((𝑚 + 1) + 1)))
49		oveq1 7427	. . . . . . . 8 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 + 1) = ((𝑚 + 1) + 1))
50	49	oveq2d 7436	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...(𝑥 + 1)) = (0...((𝑚 + 1) + 1)))
51	50	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘)))
52	48, 51	oveq12d 7438	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘))))
53	47, 52	eqeq12d 2776	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘)))))
54	46, 53	anbi12d 644	. . 3 ⊢ (𝑥 = (𝑚 + 1) → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘))))))
55		fveq2 6885	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
56		fveq2 6885	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
57		oveq2 7428	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
58	57	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘)))
59	56, 58	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘))))
60	55, 59	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘)))))
61		fvoveq1 7443	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑁 + 1)))
62		fvoveq1 7443	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘(𝑥 + 1)) = (!‘(𝑁 + 1)))
63		oveq1 7427	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
64	63	oveq2d 7436	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...(𝑥 + 1)) = (0...(𝑁 + 1)))
65	64	sumeq1d 15872	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑁 + 1))(( -1↑𝑘) / (!‘𝑘)))
66	62, 65	oveq12d 7438	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))(( -1↑𝑘) / (!‘𝑘))))
67	61, 66	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))(( -1↑𝑘) / (!‘𝑘)))))
68	60, 67	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑁 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))(( -1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))(( -1↑𝑘) / (!‘𝑘))))))
69		0z 12707	. . . . . . 7 ⊢ 0 ∈ ℤ
70		ax-1cn 11261	. . . . . . 7 ⊢ 1 ∈ ℂ
71		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → ( -1↑𝑘) = ( -1↑0))
72		neg1cn 12308	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
73		exp0 14211	. . . . . . . . . . . 12 ⊢ ( -1 ∈ ℂ → ( -1↑0) = 1)
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ ( -1↑0) = 1
75	71, 74	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ( -1↑𝑘) = 1)
76		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
77	76, 7	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
78	75, 77	oveq12d 7438	. . . . . . . . 9 ⊢ (𝑘 = 0 → (( -1↑𝑘) / (!‘𝑘)) = (1 / 1))
79	70	div1i 12048	. . . . . . . . 9 ⊢ (1 / 1) = 1
80	78, 79	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑘 = 0 → (( -1↑𝑘) / (!‘𝑘)) = 1)
81	80	fsum1 15918	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)) = 1)
82	69, 70, 81	mp2an 705	. . . . . 6 ⊢ Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)) = 1
83	82	oveq2i 7431	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘))) = (1 · 1)
84		1t1e1 12507	. . . . 5 ⊢ (1 · 1) = 1
85	83, 84	eqtr2i 2784	. . . 4 ⊢ 1 = (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)))
86		nn0uz 13006	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
87		1e0p1 12864	. . . . . . . . 9 ⊢ 1 = (0 + 1)
88		oveq2 7428	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ( -1↑𝑘) = ( -1↑1))
89		exp1 14213	. . . . . . . . . . . . 13 ⊢ ( -1 ∈ ℂ → ( -1↑1) = -1)
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( -1↑1) = -1
91	88, 90	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ( -1↑𝑘) = -1)
92		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (!‘𝑘) = (!‘1))
93	92, 17	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (!‘𝑘) = 1)
94	91, 93	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (( -1↑𝑘) / (!‘𝑘)) = ( -1 / 1))
95	72	div1i 12048	. . . . . . . . . 10 ⊢ ( -1 / 1) = -1
96	94, 95	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑘 = 1 → (( -1↑𝑘) / (!‘𝑘)) = -1)
97		neg1rr 12309	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
98		reexpcl 14224	. . . . . . . . . . . . 13 ⊢ (( -1 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → ( -1↑𝑘) ∈ ℝ)
99	97, 98	mpan 703	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → ( -1↑𝑘) ∈ ℝ)
100		faccl 14430	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (!‘𝑘) ∈ ℕ)
101	99, 100	nndivred 12395	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → (( -1↑𝑘) / (!‘𝑘)) ∈ ℝ)
102	101	recnd 11340	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ → (( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
103	102	adantl 487	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → (( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
104		0nn0 12624	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
105	104, 82	pm3.2i 476	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)) = 1)
106	105	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘)) = 1))
107		1pneg1e0 12463	. . . . . . . . . 10 ⊢ (1 + -1) = 0
108	107	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (1 + -1) = 0)
109	86, 87, 96, 103, 106, 108	fsump1i 15940	. . . . . . . 8 ⊢ (⊤ → (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)) = 0))
110	109	mptru 1576	. . . . . . 7 ⊢ (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)) = 0)
111	110	simpri 491	. . . . . 6 ⊢ Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)) = 0
112	111	oveq2i 7431	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘))) = (1 · 0)
113	70	mul01i 11503	. . . . 5 ⊢ (1 · 0) = 0
114	112, 113	eqtr2i 2784	. . . 4 ⊢ 0 = (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘)))
115	85, 114	pm3.2i 476	. . 3 ⊢ (1 = (1 · Σ𝑘 ∈ (0...0)(( -1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)(( -1↑𝑘) / (!‘𝑘))))
116		simpr 490	. . . . 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 7429	. . . . . . 7 ⊢ (((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
119	118	ancoms 464	. . . . . 6 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
120	119	oveq2d 7436	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))) → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))))
121		nn0p1nn 12648	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
122	2, 3	subfacp1 36037	. . . . . . . 8 ⊢ ((𝑚 + 1) ∈ ℕ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
123	121, 122	syl 18	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
124		nn0cn 12619	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
125		pncan 11566	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
126	124, 70, 125	sylancl 598	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) − 1) = 𝑚)
127	126	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) − 1)) = (𝑆‘𝑚))
128	127	oveq2d 7436	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1))) = ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)))
129	128	oveq2d 7436	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
130	123, 129	eqtrd 2795	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
131		peano2nn0 12649	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
132		peano2nn0 12649	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
133	131, 132	syl 18	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
134		faccl 14430	. . . . . . . . . . 11 ⊢ (((𝑚 + 1) + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
135	133, 134	syl 18	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
136	135	nncnd 12354	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℂ)
137		fzfid 14119	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (0...(𝑚 + 1)) ∈ Fin)
138		elfznn0 13757	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑚 + 1)) → 𝑘 ∈ ℕ₀)
139	138	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → 𝑘 ∈ ℕ₀)
140	139, 102	syl 18	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → (( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
141	137, 140	fsumcl 15904	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
142		expcl 14225	. . . . . . . . . . 11 ⊢ (( -1 ∈ ℂ ∧ ((𝑚 + 1) + 1) ∈ ℕ₀) → ( -1↑((𝑚 + 1) + 1)) ∈ ℂ)
143	72, 133, 142	sylancr 599	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ( -1↑((𝑚 + 1) + 1)) ∈ ℂ)
144	135	nnne0d 12391	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ≠ 0)
145	143, 136, 144	divcld 12096	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))) ∈ ℂ)
146	136, 141, 145	adddid 11336	. . . . . . . 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 23	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℕ₀)
148	147, 86	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ (ℤ_≥‘0))
149		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → ( -1↑𝑘) = ( -1↑(𝑚 + 1)))
150		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (!‘𝑘) = (!‘(𝑚 + 1)))
151	149, 150	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑚 + 1) → (( -1↑𝑘) / (!‘𝑘)) = (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))
152	148, 140, 151	fsump1 15927	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) + (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))))
153	152	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) + (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
154		fzfid 14119	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (0...𝑚) ∈ Fin)
155		elfznn0 13757	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ₀)
156	155	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ₀)
157	156, 102	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → (( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
158	154, 157	fsumcl 15904	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
159		expcl 14225	. . . . . . . . . . . . 13 ⊢ (( -1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → ( -1↑(𝑚 + 1)) ∈ ℂ)
160	72, 131, 159	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ( -1↑(𝑚 + 1)) ∈ ℂ)
161		faccl 14430	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
162	131, 161	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
163	162	nncnd 12354	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℂ)
164	162	nnne0d 12391	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ≠ 0)
165	160, 163, 164	divcld 12096	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))) ∈ ℂ)
166	136, 158, 165	adddid 11336	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) + (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
167		facp1 14425	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
168	131, 167	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
169		facp1 14425	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1)))
170		faccl 14430	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℕ)
171	170	nncnd 12354	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℂ)
172	121	nncnd 12354	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
173	171, 172	mulcomd 11333	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
174	169, 173	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
175	174	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) = (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)))
176	133	nn0cnd 12672	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℂ)
177	172, 171, 176	mulassd 11335	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
178	168, 175, 177	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
179	178	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) = (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))
180	136, 160, 163, 164	div12d 12132	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (( -1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))))
181	168	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))))
182	176, 163, 164	divcan3d 12101	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
183	181, 182	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
184	183	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))) = (( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
185	180, 184	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
186	179, 185	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + (( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
187	153, 166, 186	3eqtrd 2799	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + (( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
188	143, 136, 144	divcan2d 12098	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))) = ( -1↑((𝑚 + 1) + 1)))
189	187, 188	oveq12d 7438	. . . . . . . 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 11332	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) ∈ ℂ)
191	172, 190, 158	mulassd 11335	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
192	72	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
193	160, 176, 192	adddid 11336	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = ((( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (( -1↑(𝑚 + 1)) · -1)))
194		negsub 11609	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 + 1) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
195	176, 70, 194	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
196		pncan 11566	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
197	172, 70, 196	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
198	195, 197	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (𝑚 + 1))
199	198	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = (( -1↑(𝑚 + 1)) · (𝑚 + 1)))
200	193, 199	eqtr3d 2797	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (( -1↑(𝑚 + 1)) · -1)) = (( -1↑(𝑚 + 1)) · (𝑚 + 1)))
201		expp1 14214	. . . . . . . . . . . . 13 ⊢ (( -1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → ( -1↑((𝑚 + 1) + 1)) = (( -1↑(𝑚 + 1)) · -1))
202	72, 131, 201	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ( -1↑((𝑚 + 1) + 1)) = (( -1↑(𝑚 + 1)) · -1))
203	202	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ( -1↑((𝑚 + 1) + 1))) = ((( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (( -1↑(𝑚 + 1)) · -1)))
204	172, 160	mulcomd 11333	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ( -1↑(𝑚 + 1))) = (( -1↑(𝑚 + 1)) · (𝑚 + 1)))
205	200, 203, 204	3eqtr4d 2805	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ( -1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · ( -1↑(𝑚 + 1))))
206	191, 205	oveq12d 7438	. . . . . . . . 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 11332	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) ∈ ℂ)
208	207, 158	mulcld 11332	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∈ ℂ)
209	160, 176	mulcld 11332	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (( -1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) ∈ ℂ)
210	208, 209, 143	addassd 11334	. . . . . . . . 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 11332	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∈ ℂ)
212	172, 211, 160	adddid 11336	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · ( -1↑(𝑚 + 1)))))
213	206, 210, 212	3eqtr4d 2805	. . . . . . . 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 2799	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)) + (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1)))))
215	131, 86	eleqtrdi 2870	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ (ℤ_≥‘0))
216		elfznn0 13757	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((𝑚 + 1) + 1)) → 𝑘 ∈ ℕ₀)
217	216	adantl 487	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → 𝑘 ∈ ℕ₀)
218	217, 102	syl 18	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → (( -1↑𝑘) / (!‘𝑘)) ∈ ℂ)
219		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → ( -1↑𝑘) = ( -1↑((𝑚 + 1) + 1)))
220		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (!‘𝑘) = (!‘((𝑚 + 1) + 1)))
221	219, 220	oveq12d 7438	. . . . . . . . 9 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (( -1↑𝑘) / (!‘𝑘)) = (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))
222	215, 218, 221	fsump1 15927	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)) + (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))))
223	222	oveq2d 7436	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)) + (( -1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
224	163, 158	mulcld 11332	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∈ ℂ)
225	171, 158	mulcld 11332	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∈ ℂ)
226	224, 160, 225	add32d 11541	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) + ( -1↑(𝑚 + 1))))
227	152	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) + (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
228	163, 158, 165	adddid 11336	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)) + (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
229	160, 163, 164	divcan2d 12098	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ( -1↑(𝑚 + 1)))
230	229	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · (( -1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1))))
231	227, 228, 230	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1))))
232	231	oveq1d 7435	. . . . . . . . 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 11336	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)))
235	169	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = (!‘(𝑚 + 1)))
236	171	mulridd 11329	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · 1) = (!‘𝑚))
237	235, 236	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
238	234, 237	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
239	238	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))
240	163, 171, 158	adddird 11337	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
241	239, 240	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))
242	241	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) + ( -1↑(𝑚 + 1))))
243	226, 232, 242	3eqtr4d 2805	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))) = ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1))))
244	243	oveq2d 7436	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) + ( -1↑(𝑚 + 1)))))
245	214, 223, 244	3eqtr4d 2805	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))))))
246	130, 245	eqeq12d 2776	. . . . 5 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘))) ↔ ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘)))))))
247	120, 246	imbitrrid 249	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))(( -1↑𝑘) / (!‘𝑘)))) → (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))(( -1↑𝑘) / (!‘𝑘)))))
248	117, 247	jcad 522	. . 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 12797	. 2 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))(( -1↑𝑘) / (!‘𝑘)))))
250	249	simpld 500	1 ⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) / (!‘𝑘))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ⊤wtru 1570 ∈ wcel 2144 {cab 2738 ≠ wne 2955 ∀wral 3076 ↦ cmpt 5185 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 Fincfn 8976 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 + caddc 11206 · cmul 11208 − cmin 11544 -cneg 11545 / cdiv 11976 ℕcn 12338 ℕ₀cn0 12609 ℤcz 12696 ℤ_≥cuz 12968 ...cfz 13642 ↑cexp 14207 !cfa 14420 ♯chash 14477 Σcsu 15858

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-oadd 8483 df-er 8720 df-map 8852 df-pm 8853 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-sup 9437 df-oi 9507 df-dju 9985 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-n0 12610 df-xnn0 12683 df-z 12697 df-uz 12969 df-rp 13124 df-fz 13643 df-fzo 13792 df-seq 14148 df-exp 14208 df-fac 14421 df-hash 14478 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-clim 15660 df-sum 15859

This theorem is used by: subfaclim 36039

W3C validator