Theorem subfacval2

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

	Ref	Expression
Hypotheses	derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
	subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
Assertion	subfacval2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) = ( ( ! ‘ 𝑁 ) · Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )

Proof

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