Theorem subfacval2

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

	Ref	Expression
Hypotheses	derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
	subfac.n	$$⊢S=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)$$
Assertion	subfacval2	$$⊢N\in {\mathbb{N}}_0\to S\left(N\right)=N!\sum _{k=0}^N\left(\frac{{\left(-1\right)}^k}{k!}\right)$$

Proof

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