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 
|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
subfac.n 
|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
Assertion subfacval2 
|- ( N e. NN0 -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )

Proof

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