Metamath Proof Explorer

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 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )