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 33049

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 6756	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0))
2		derang.d	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
3		subfac.n	. . . . . . 7 ⊢ 𝑆 = (𝑛 ∈ ℕ₀ ↦ (𝐷‘(1...𝑛)))
4	2, 3	subfac0 33039	. . . . . 6 ⊢ (𝑆‘0) = 1
5	1, 4	eqtrdi 2795	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘𝑥) = 1)
6		fveq2 6756	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘𝑥) = (!‘0))
7		fac0 13918	. . . . . . 7 ⊢ (!‘0) = 1
8	6, 7	eqtrdi 2795	. . . . . 6 ⊢ (𝑥 = 0 → (!‘𝑥) = 1)
9		oveq2 7263	. . . . . . 7 ⊢ (𝑥 = 0 → (0...𝑥) = (0...0))
10	9	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
11	8, 10	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 0 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))))
12	5, 11	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))))
13		fv0p1e1 12026	. . . . . 6 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = (𝑆‘1))
14	2, 3	subfac1 33040	. . . . . 6 ⊢ (𝑆‘1) = 0
15	13, 14	eqtrdi 2795	. . . . 5 ⊢ (𝑥 = 0 → (𝑆‘(𝑥 + 1)) = 0)
16		fv0p1e1 12026	. . . . . . 7 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = (!‘1))
17		fac1 13919	. . . . . . 7 ⊢ (!‘1) = 1
18	16, 17	eqtrdi 2795	. . . . . 6 ⊢ (𝑥 = 0 → (!‘(𝑥 + 1)) = 1)
19		oveq1 7262	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
20		0p1e1 12025	. . . . . . . . 9 ⊢ (0 + 1) = 1
21	19, 20	eqtrdi 2795	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
22	21	oveq2d 7271	. . . . . . 7 ⊢ (𝑥 = 0 → (0...(𝑥 + 1)) = (0...1))
23	22	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
24	18, 23	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 0 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
25	15, 24	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 0 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))))
26	12, 25	anbi12d 630	. . 3 ⊢ (𝑥 = 0 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))))
27		fveq2 6756	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘𝑥) = (𝑆‘𝑚))
28		fveq2 6756	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘𝑥) = (!‘𝑚))
29		oveq2 7263	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...𝑥) = (0...𝑚))
30	29	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))
31	28, 30	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
32	27, 31	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
33		fvoveq1 7278	. . . . 5 ⊢ (𝑥 = 𝑚 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑚 + 1)))
34		fvoveq1 7278	. . . . . 6 ⊢ (𝑥 = 𝑚 → (!‘(𝑥 + 1)) = (!‘(𝑚 + 1)))
35		oveq1 7262	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 + 1) = (𝑚 + 1))
36	35	oveq2d 7271	. . . . . . 7 ⊢ (𝑥 = 𝑚 → (0...(𝑥 + 1)) = (0...(𝑚 + 1)))
37	36	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 𝑚 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
38	34, 37	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 𝑚 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
39	33, 38	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑚 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
40	32, 39	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑚 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))))
41		fveq2 6756	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘𝑥) = (𝑆‘(𝑚 + 1)))
42		fveq2 6756	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘𝑥) = (!‘(𝑚 + 1)))
43		oveq2 7263	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...𝑥) = (0...(𝑚 + 1)))
44	43	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))
45	42, 44	oveq12d 7273	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
46	41, 45	eqeq12d 2754	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
47		fvoveq1 7278	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → (𝑆‘(𝑥 + 1)) = (𝑆‘((𝑚 + 1) + 1)))
48		fvoveq1 7278	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → (!‘(𝑥 + 1)) = (!‘((𝑚 + 1) + 1)))
49		oveq1 7262	. . . . . . . 8 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 + 1) = ((𝑚 + 1) + 1))
50	49	oveq2d 7271	. . . . . . 7 ⊢ (𝑥 = (𝑚 + 1) → (0...(𝑥 + 1)) = (0...((𝑚 + 1) + 1)))
51	50	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = (𝑚 + 1) → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))
52	48, 51	oveq12d 7273	. . . . 5 ⊢ (𝑥 = (𝑚 + 1) → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))
53	47, 52	eqeq12d 2754	. . . 4 ⊢ (𝑥 = (𝑚 + 1) → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
54	46, 53	anbi12d 630	. . 3 ⊢ (𝑥 = (𝑚 + 1) → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
55		fveq2 6756	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁))
56		fveq2 6756	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
57		oveq2 7263	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁))
58	57	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))
59	56, 58	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
60	55, 59	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘)))))
61		fvoveq1 7278	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑆‘(𝑥 + 1)) = (𝑆‘(𝑁 + 1)))
62		fvoveq1 7278	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘(𝑥 + 1)) = (!‘(𝑁 + 1)))
63		oveq1 7262	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
64	63	oveq2d 7271	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (0...(𝑥 + 1)) = (0...(𝑁 + 1)))
65	64	sumeq1d 15341	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)) = Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))
66	62, 65	oveq12d 7273	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))
67	61, 66	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘))) ↔ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
68	60, 67	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑁 → (((𝑆‘𝑥) = ((!‘𝑥) · Σ𝑘 ∈ (0...𝑥)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑥 + 1)) = ((!‘(𝑥 + 1)) · Σ𝑘 ∈ (0...(𝑥 + 1))((-1↑𝑘) / (!‘𝑘)))) ↔ ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘))))))
69		0z 12260	. . . . . . 7 ⊢ 0 ∈ ℤ
70		ax-1cn 10860	. . . . . . 7 ⊢ 1 ∈ ℂ
71		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
72		neg1cn 12017	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
73		exp0 13714	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
74	72, 73	ax-mp 5	. . . . . . . . . . 11 ⊢ (-1↑0) = 1
75	71, 74	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (-1↑𝑘) = 1)
76		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
77	76, 7	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
78	75, 77	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = (1 / 1))
79	70	div1i 11633	. . . . . . . . 9 ⊢ (1 / 1) = 1
80	78, 79	eqtrdi 2795	. . . . . . . 8 ⊢ (𝑘 = 0 → ((-1↑𝑘) / (!‘𝑘)) = 1)
81	80	fsum1 15387	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
82	69, 70, 81	mp2an 688	. . . . . 6 ⊢ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1
83	82	oveq2i 7266	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) = (1 · 1)
84		1t1e1 12065	. . . . 5 ⊢ (1 · 1) = 1
85	83, 84	eqtr2i 2767	. . . 4 ⊢ 1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)))
86		nn0uz 12549	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
87		1e0p1 12408	. . . . . . . . 9 ⊢ 1 = (0 + 1)
88		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (-1↑𝑘) = (-1↑1))
89		exp1 13716	. . . . . . . . . . . . 13 ⊢ (-1 ∈ ℂ → (-1↑1) = -1)
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 ⊢ (-1↑1) = -1
91	88, 90	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (-1↑𝑘) = -1)
92		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (!‘𝑘) = (!‘1))
93	92, 17	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (!‘𝑘) = 1)
94	91, 93	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = (-1 / 1))
95	72	div1i 11633	. . . . . . . . . 10 ⊢ (-1 / 1) = -1
96	94, 95	eqtrdi 2795	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((-1↑𝑘) / (!‘𝑘)) = -1)
97		neg1rr 12018	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℝ
98		reexpcl 13727	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℝ)
99	97, 98	mpan 686	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (-1↑𝑘) ∈ ℝ)
100		faccl 13925	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ₀ → (!‘𝑘) ∈ ℕ)
101	99, 100	nndivred 11957	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℝ)
102	101	recnd 10934	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
103	102	adantl 481	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ₀) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
104		0nn0 12178	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
105	104, 82	pm3.2i 470	. . . . . . . . . 10 ⊢ (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1)
106	105	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (0 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘)) = 1))
107		1pneg1e0 12022	. . . . . . . . . 10 ⊢ (1 + -1) = 0
108	107	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (1 + -1) = 0)
109	86, 87, 96, 103, 106, 108	fsump1i 15409	. . . . . . . 8 ⊢ (⊤ → (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0))
110	109	mptru 1546	. . . . . . 7 ⊢ (1 ∈ ℕ₀ ∧ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0)
111	110	simpri 485	. . . . . 6 ⊢ Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)) = 0
112	111	oveq2i 7266	. . . . 5 ⊢ (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))) = (1 · 0)
113	70	mul01i 11095	. . . . 5 ⊢ (1 · 0) = 0
114	112, 113	eqtr2i 2767	. . . 4 ⊢ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘)))
115	85, 114	pm3.2i 470	. . 3 ⊢ (1 = (1 · Σ𝑘 ∈ (0...0)((-1↑𝑘) / (!‘𝑘))) ∧ 0 = (1 · Σ𝑘 ∈ (0...1)((-1↑𝑘) / (!‘𝑘))))
116		simpr 484	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))))
117	116	a1i 11	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))))
118		oveq12 7264	. . . . . . 7 ⊢ (((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
119	118	ancoms 458	. . . . . 6 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
120	119	oveq2d 7271	. . . . 5 ⊢ (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
121		nn0p1nn 12202	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
122	2, 3	subfacp1 33048	. . . . . . . 8 ⊢ ((𝑚 + 1) ∈ ℕ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
123	121, 122	syl 17	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))))
124		nn0cn 12173	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
125		pncan 11157	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
126	124, 70, 125	sylancl 585	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) − 1) = 𝑚)
127	126	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) − 1)) = (𝑆‘𝑚))
128	127	oveq2d 7271	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1))) = ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚)))
129	128	oveq2d 7271	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘((𝑚 + 1) − 1)))) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
130	123, 129	eqtrd 2778	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (𝑆‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))))
131		peano2nn0 12203	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
132		peano2nn0 12203	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
133	131, 132	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℕ₀)
134		faccl 13925	. . . . . . . . . . 11 ⊢ (((𝑚 + 1) + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
135	133, 134	syl 17	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℕ)
136	135	nncnd 11919	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ∈ ℂ)
137		fzfid 13621	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (0...(𝑚 + 1)) ∈ Fin)
138		elfznn0 13278	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑚 + 1)) → 𝑘 ∈ ℕ₀)
139	138	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → 𝑘 ∈ ℕ₀)
140	139, 102	syl 17	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...(𝑚 + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
141	137, 140	fsumcl 15373	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
142		expcl 13728	. . . . . . . . . . 11 ⊢ ((-1 ∈ ℂ ∧ ((𝑚 + 1) + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
143	72, 133, 142	sylancr 586	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) ∈ ℂ)
144	135	nnne0d 11953	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) ≠ 0)
145	143, 136, 144	divcld 11681	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))) ∈ ℂ)
146	136, 141, 145	adddid 10930	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
147		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℕ₀)
148	147, 86	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ (ℤ_≥‘0))
149		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (-1↑𝑘) = (-1↑(𝑚 + 1)))
150		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑚 + 1) → (!‘𝑘) = (!‘(𝑚 + 1)))
151	149, 150	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑚 + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))
152	148, 140, 151	fsump1 15396	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))))
153	152	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
154		fzfid 13621	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (0...𝑚) ∈ Fin)
155		elfznn0 13278	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ₀)
156	155	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ₀)
157	156, 102	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...𝑚)) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
158	154, 157	fsumcl 15373	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
159		expcl 13728	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑(𝑚 + 1)) ∈ ℂ)
160	72, 131, 159	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑(𝑚 + 1)) ∈ ℂ)
161		faccl 13925	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
162	131, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℕ)
163	162	nncnd 11919	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ∈ ℂ)
164	162	nnne0d 11953	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) ≠ 0)
165	160, 163, 164	divcld 11681	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))) ∈ ℂ)
166	136, 158, 165	adddid 10930	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
167		facp1 13920	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
168	131, 167	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)))
169		facp1 13920	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1)))
170		faccl 13925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℕ)
171	170	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (!‘𝑚) ∈ ℂ)
172	121	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℂ)
173	171, 172	mulcomd 10927	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
174	169, 173	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (!‘(𝑚 + 1)) = ((𝑚 + 1) · (!‘𝑚)))
175	174	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) = (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)))
176	133	nn0cnd 12225	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) + 1) ∈ ℂ)
177	172, 171, 176	mulassd 10929	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · (!‘𝑚)) · ((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
178	168, 175, 177	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (!‘((𝑚 + 1) + 1)) = ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))))
179	178	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
180	136, 160, 163, 164	div12d 11717	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))))
181	168	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))))
182	176, 163, 164	divcan3d 11686	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · ((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
183	181, 182	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1))) = ((𝑚 + 1) + 1))
184	183	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((!‘((𝑚 + 1) + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
185	180, 184	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)))
186	179, 185	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘((𝑚 + 1) + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
187	153, 166, 186	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1))))
188	143, 136, 144	divcan2d 11683	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))) = (-1↑((𝑚 + 1) + 1)))
189	187, 188	oveq12d 7273	. . . . . . . 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 10926	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) ∈ ℂ)
191	172, 190, 158	mulassd 10929	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
192	72	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → -1 ∈ ℂ)
193	160, 176, 192	adddid 10930	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
194		negsub 11199	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 + 1) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
195	176, 70, 194	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (((𝑚 + 1) + 1) − 1))
196		pncan 11157	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
197	172, 70, 196	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) − 1) = (𝑚 + 1))
198	195, 197	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) + 1) + -1) = (𝑚 + 1))
199	198	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · (((𝑚 + 1) + 1) + -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
200	193, 199	eqtr3d 2780	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
201		expp1 13717	. . . . . . . . . . . . 13 ⊢ ((-1 ∈ ℂ ∧ (𝑚 + 1) ∈ ℕ₀) → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
202	72, 131, 201	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → (-1↑((𝑚 + 1) + 1)) = ((-1↑(𝑚 + 1)) · -1))
203	202	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + ((-1↑(𝑚 + 1)) · -1)))
204	172, 160	mulcomd 10927	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (-1↑(𝑚 + 1))) = ((-1↑(𝑚 + 1)) · (𝑚 + 1)))
205	200, 203, 204	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) + (-1↑((𝑚 + 1) + 1))) = ((𝑚 + 1) · (-1↑(𝑚 + 1))))
206	191, 205	oveq12d 7273	. . . . . . . . 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 10926	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) ∈ ℂ)
208	207, 158	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 + 1) · ((!‘𝑚) · ((𝑚 + 1) + 1))) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
209	160, 176	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((-1↑(𝑚 + 1)) · ((𝑚 + 1) + 1)) ∈ ℂ)
210	208, 209, 143	addassd 10928	. . . . . . . . 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 10926	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
212	172, 211, 160	adddid 10930	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))) = (((𝑚 + 1) · (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + ((𝑚 + 1) · (-1↑(𝑚 + 1)))))
213	206, 210, 212	3eqtr4d 2788	. . . . . . . 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 2782	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
215	131, 86	eleqtrdi 2849	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ (ℤ_≥‘0))
216		elfznn0 13278	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...((𝑚 + 1) + 1)) → 𝑘 ∈ ℕ₀)
217	216	adantl 481	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → 𝑘 ∈ ℕ₀)
218	217, 102	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ₀ ∧ 𝑘 ∈ (0...((𝑚 + 1) + 1))) → ((-1↑𝑘) / (!‘𝑘)) ∈ ℂ)
219		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (-1↑𝑘) = (-1↑((𝑚 + 1) + 1)))
220		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑘 = ((𝑚 + 1) + 1) → (!‘𝑘) = (!‘((𝑚 + 1) + 1)))
221	219, 220	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑘 = ((𝑚 + 1) + 1) → ((-1↑𝑘) / (!‘𝑘)) = ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))
222	215, 218, 221	fsump1 15396	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)) = (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1)))))
223	222	oveq2d 7271	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘((𝑚 + 1) + 1)) · (Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)) + ((-1↑((𝑚 + 1) + 1)) / (!‘((𝑚 + 1) + 1))))))
224	163, 158	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
225	171, 158	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∈ ℂ)
226	224, 160, 225	add32d 11132	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
227	152	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
228	163, 158, 165	adddid 10930	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · (Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)) + ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))))
229	160, 163, 164	divcan2d 11683	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1)))) = (-1↑(𝑚 + 1)))
230	229	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘(𝑚 + 1)) · ((-1↑(𝑚 + 1)) / (!‘(𝑚 + 1))))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
231	227, 228, 230	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
232	231	oveq1d 7270	. . . . . . . . 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 10930	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)))
235	169	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · (𝑚 + 1)) = (!‘(𝑚 + 1)))
236	171	mulid1d 10923	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · 1) = (!‘𝑚))
237	235, 236	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · (𝑚 + 1)) + ((!‘𝑚) · 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
238	234, 237	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ₀ → ((!‘𝑚) · ((𝑚 + 1) + 1)) = ((!‘(𝑚 + 1)) + (!‘𝑚)))
239	238	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))
240	163, 171, 158	adddird 10931	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) + (!‘𝑚)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
241	239, 240	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ₀ → (((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) = (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))
242	241	oveq1d 7270	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ₀ → ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))) = ((((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) + (-1↑(𝑚 + 1))))
243	226, 232, 242	3eqtr4d 2788	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ → (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))) = ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1))))
244	243	oveq2d 7271	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))) = ((𝑚 + 1) · ((((!‘𝑚) · ((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) + (-1↑(𝑚 + 1)))))
245	214, 223, 244	3eqtr4d 2788	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))))))
246	130, 245	eqeq12d 2754	. . . . 5 ⊢ (𝑚 ∈ ℕ₀ → ((𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))) ↔ ((𝑚 + 1) · ((𝑆‘(𝑚 + 1)) + (𝑆‘𝑚))) = ((𝑚 + 1) · (((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) + ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘)))))))
247	120, 246	syl5ibr 245	. . . 4 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘)))))
248	117, 247	jcad 512	. . 3 ⊢ (𝑚 ∈ ℕ₀ → (((𝑆‘𝑚) = ((!‘𝑚) · Σ𝑘 ∈ (0...𝑚)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘)))) → ((𝑆‘(𝑚 + 1)) = ((!‘(𝑚 + 1)) · Σ𝑘 ∈ (0...(𝑚 + 1))((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘((𝑚 + 1) + 1)) = ((!‘((𝑚 + 1) + 1)) · Σ𝑘 ∈ (0...((𝑚 + 1) + 1))((-1↑𝑘) / (!‘𝑘))))))
249	26, 40, 54, 68, 115, 248	nn0ind 12345	. 2 ⊢ (𝑁 ∈ ℕ₀ → ((𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))) ∧ (𝑆‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) · Σ𝑘 ∈ (0...(𝑁 + 1))((-1↑𝑘) / (!‘𝑘)))))
250	249	simpld 494	1 ⊢ (𝑁 ∈ ℕ₀ → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 {cab 2715 ≠ wne 2942 ∀wral 3063 ↦ cmpt 5153 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 Fincfn 8691 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168 ↑cexp 13710 !cfa 13915 ♯chash 13972 Σcsu 15325

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-rp 12660 df-fz 13169 df-fzo 13312 df-seq 13650 df-exp 13711 df-fac 13916 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326

This theorem is referenced by: subfaclim 33050

W3C validator