Theorem subfacval2 31169

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

Hypotheses

Ref	Expression
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

Ref	Expression
subfacval2	|- ( N e. NN0 -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )

Distinct variable groups:   f, n, x, y, k, N   D, n   S, n, x, y

Allowed substitution hints:   D( x, y, f, k)   S( f, k)

Proof of Theorem subfacval2

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . . . . 6 |- ( x = 0 -> ( S ` x ) = ( S ` 0 ) )
2		derang.d	. . . . . . 7 |- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
3		subfac.n	. . . . . . 7 |- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
4	2, 3	subfac0 31159	. . . . . 6 |- ( S ` 0 ) = 1
5	1, 4	syl6eq 2672	. . . . 5 |- ( x = 0 -> ( S ` x ) = 1 )
6		fveq2 6191	. . . . . . 7 |- ( x = 0 -> ( ! ` x ) = ( ! ` 0 ) )
7		fac0 13063	. . . . . . 7 |- ( ! ` 0 ) = 1
8	6, 7	syl6eq 2672	. . . . . 6 |- ( x = 0 -> ( ! ` x ) = 1 )
9		oveq2 6658	. . . . . . 7 |- ( x = 0 -> ( 0 ... x ) = ( 0 ... 0 ) )
10	9	sumeq1d 14431	. . . . . 6 |- ( x = 0 -> sum_ k e. ( 0 ... x ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
11	8, 10	oveq12d 6668	. . . . 5 |- ( 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 2637	. . . 4 |- ( 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		oveq1 6657	. . . . . . . 8 |- ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
14		0p1e1 11132	. . . . . . . 8 |- ( 0 + 1 ) = 1
15	13, 14	syl6eq 2672	. . . . . . 7 |- ( x = 0 -> ( x + 1 ) = 1 )
16	15	fveq2d 6195	. . . . . 6 |- ( x = 0 -> ( S ` ( x + 1 ) ) = ( S ` 1 ) )
17	2, 3	subfac1 31160	. . . . . 6 |- ( S ` 1 ) = 0
18	16, 17	syl6eq 2672	. . . . 5 |- ( x = 0 -> ( S ` ( x + 1 ) ) = 0 )
19	15	fveq2d 6195	. . . . . . 7 |- ( x = 0 -> ( ! ` ( x + 1 ) ) = ( ! ` 1 ) )
20		fac1 13064	. . . . . . 7 |- ( ! ` 1 ) = 1
21	19, 20	syl6eq 2672	. . . . . 6 |- ( x = 0 -> ( ! ` ( x + 1 ) ) = 1 )
22	15	oveq2d 6666	. . . . . . 7 |- ( x = 0 -> ( 0 ... ( x + 1 ) ) = ( 0 ... 1 ) )
23	22	sumeq1d 14431	. . . . . 6 |- ( x = 0 -> sum_ k e. ( 0 ... ( x + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
24	21, 23	oveq12d 6668	. . . . 5 |- ( 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	18, 24	eqeq12d 2637	. . . 4 |- ( 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 747	. . 3 |- ( 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 6191	. . . . 5 |- ( x = m -> ( S ` x ) = ( S ` m ) )
28		fveq2 6191	. . . . . 6 |- ( x = m -> ( ! ` x ) = ( ! ` m ) )
29		oveq2 6658	. . . . . . 7 |- ( x = m -> ( 0 ... x ) = ( 0 ... m ) )
30	29	sumeq1d 14431	. . . . . 6 |- ( x = m -> sum_ k e. ( 0 ... x ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... m ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
31	28, 30	oveq12d 6668	. . . . 5 |- ( 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 2637	. . . 4 |- ( 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		oveq1 6657	. . . . . 6 |- ( x = m -> ( x + 1 ) = ( m + 1 ) )
34	33	fveq2d 6195	. . . . 5 |- ( x = m -> ( S ` ( x + 1 ) ) = ( S ` ( m + 1 ) ) )
35	33	fveq2d 6195	. . . . . 6 |- ( x = m -> ( ! ` ( x + 1 ) ) = ( ! ` ( m + 1 ) ) )
36	33	oveq2d 6666	. . . . . . 7 |- ( x = m -> ( 0 ... ( x + 1 ) ) = ( 0 ... ( m + 1 ) ) )
37	36	sumeq1d 14431	. . . . . 6 |- ( x = m -> sum_ k e. ( 0 ... ( x + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... ( m + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
38	35, 37	oveq12d 6668	. . . . 5 |- ( 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	34, 38	eqeq12d 2637	. . . 4 |- ( 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 747	. . 3 |- ( 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 6191	. . . . 5 |- ( x = ( m + 1 ) -> ( S ` x ) = ( S ` ( m + 1 ) ) )
42		fveq2 6191	. . . . . 6 |- ( x = ( m + 1 ) -> ( ! ` x ) = ( ! ` ( m + 1 ) ) )
43		oveq2 6658	. . . . . . 7 |- ( x = ( m + 1 ) -> ( 0 ... x ) = ( 0 ... ( m + 1 ) ) )
44	43	sumeq1d 14431	. . . . . 6 |- ( 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 6668	. . . . 5 |- ( 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 2637	. . . 4 |- ( 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		oveq1 6657	. . . . . 6 |- ( x = ( m + 1 ) -> ( x + 1 ) = ( ( m + 1 ) + 1 ) )
48	47	fveq2d 6195	. . . . 5 |- ( x = ( m + 1 ) -> ( S ` ( x + 1 ) ) = ( S ` ( ( m + 1 ) + 1 ) ) )
49	47	fveq2d 6195	. . . . . 6 |- ( x = ( m + 1 ) -> ( ! ` ( x + 1 ) ) = ( ! ` ( ( m + 1 ) + 1 ) ) )
50	47	oveq2d 6666	. . . . . . 7 |- ( x = ( m + 1 ) -> ( 0 ... ( x + 1 ) ) = ( 0 ... ( ( m + 1 ) + 1 ) ) )
51	50	sumeq1d 14431	. . . . . 6 |- ( 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	49, 51	oveq12d 6668	. . . . 5 |- ( 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	48, 52	eqeq12d 2637	. . . 4 |- ( 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 747	. . 3 |- ( 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 6191	. . . . 5 |- ( x = N -> ( S ` x ) = ( S ` N ) )
56		fveq2 6191	. . . . . 6 |- ( x = N -> ( ! ` x ) = ( ! ` N ) )
57		oveq2 6658	. . . . . . 7 |- ( x = N -> ( 0 ... x ) = ( 0 ... N ) )
58	57	sumeq1d 14431	. . . . . 6 |- ( x = N -> sum_ k e. ( 0 ... x ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
59	56, 58	oveq12d 6668	. . . . 5 |- ( 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 2637	. . . 4 |- ( 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		oveq1 6657	. . . . . 6 |- ( x = N -> ( x + 1 ) = ( N + 1 ) )
62	61	fveq2d 6195	. . . . 5 |- ( x = N -> ( S ` ( x + 1 ) ) = ( S ` ( N + 1 ) ) )
63	61	fveq2d 6195	. . . . . 6 |- ( x = N -> ( ! ` ( x + 1 ) ) = ( ! ` ( N + 1 ) ) )
64	61	oveq2d 6666	. . . . . . 7 |- ( x = N -> ( 0 ... ( x + 1 ) ) = ( 0 ... ( N + 1 ) ) )
65	64	sumeq1d 14431	. . . . . 6 |- ( x = N -> sum_ k e. ( 0 ... ( x + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
66	63, 65	oveq12d 6668	. . . . 5 |- ( 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	62, 66	eqeq12d 2637	. . . 4 |- ( 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 747	. . 3 |- ( 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 11388	. . . . . . 7 |- 0 e. ZZ
70		ax-1cn 9994	. . . . . . 7 |- 1 e. CC
71		oveq2 6658	. . . . . . . . . . 11 |- ( k = 0 -> ( -u 1 ^ k ) = ( -u 1 ^ 0 ) )
72		neg1cn 11124	. . . . . . . . . . . 12 |- -u 1 e. CC
73		exp0 12864	. . . . . . . . . . . 12 |- ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
74	72, 73	ax-mp 5	. . . . . . . . . . 11 |- ( -u 1 ^ 0 ) = 1
75	71, 74	syl6eq 2672	. . . . . . . . . 10 |- ( k = 0 -> ( -u 1 ^ k ) = 1 )
76		fveq2 6191	. . . . . . . . . . 11 |- ( k = 0 -> ( ! ` k ) = ( ! ` 0 ) )
77	76, 7	syl6eq 2672	. . . . . . . . . 10 |- ( k = 0 -> ( ! ` k ) = 1 )
78	75, 77	oveq12d 6668	. . . . . . . . 9 |- ( k = 0 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = ( 1 / 1 ) )
79	70	div1i 10753	. . . . . . . . 9 |- ( 1 / 1 ) = 1
80	78, 79	syl6eq 2672	. . . . . . . 8 |- ( k = 0 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = 1 )
81	80	fsum1 14476	. . . . . . 7 |- ( ( 0 e. ZZ /\ 1 e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 1 )
82	69, 70, 81	mp2an 708	. . . . . 6 |- sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 1
83	82	oveq2i 6661	. . . . 5 |- ( 1 x. sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) = ( 1 x. 1 )
84		1t1e1 11175	. . . . 5 |- ( 1 x. 1 ) = 1
85	83, 84	eqtr2i 2645	. . . 4 |- 1 = ( 1 x. sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
86		nn0uz 11722	. . . . . . . . 9 |- NN0 = ( ZZ>= ` 0 )
87		1e0p1 11552	. . . . . . . . 9 |- 1 = ( 0 + 1 )
88		oveq2 6658	. . . . . . . . . . . 12 |- ( k = 1 -> ( -u 1 ^ k ) = ( -u 1 ^ 1 ) )
89		exp1 12866	. . . . . . . . . . . . 13 |- ( -u 1 e. CC -> ( -u 1 ^ 1 ) = -u 1 )
90	72, 89	ax-mp 5	. . . . . . . . . . . 12 |- ( -u 1 ^ 1 ) = -u 1
91	88, 90	syl6eq 2672	. . . . . . . . . . 11 |- ( k = 1 -> ( -u 1 ^ k ) = -u 1 )
92		fveq2 6191	. . . . . . . . . . . 12 |- ( k = 1 -> ( ! ` k ) = ( ! ` 1 ) )
93	92, 20	syl6eq 2672	. . . . . . . . . . 11 |- ( k = 1 -> ( ! ` k ) = 1 )
94	91, 93	oveq12d 6668	. . . . . . . . . 10 |- ( k = 1 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = ( -u 1 / 1 ) )
95	72	div1i 10753	. . . . . . . . . 10 |- ( -u 1 / 1 ) = -u 1
96	94, 95	syl6eq 2672	. . . . . . . . 9 |- ( k = 1 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = -u 1 )
97		neg1rr 11125	. . . . . . . . . . . . 13 |- -u 1 e. RR
98		reexpcl 12877	. . . . . . . . . . . . 13 |- ( ( -u 1 e. RR /\ k e. NN0 ) -> ( -u 1 ^ k ) e. RR )
99	97, 98	mpan 706	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( -u 1 ^ k ) e. RR )
100		faccl 13070	. . . . . . . . . . . 12 |- ( k e. NN0 -> ( ! ` k ) e. NN )
101	99, 100	nndivred 11069	. . . . . . . . . . 11 |- ( k e. NN0 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. RR )
102	101	recnd 10068	. . . . . . . . . 10 |- ( k e. NN0 -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
103	102	adantl 482	. . . . . . . . 9 |- ( ( T. /\ k e. NN0 ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
104		0nn0 11307	. . . . . . . . . . 11 |- 0 e. NN0
105	104, 82	pm3.2i 471	. . . . . . . . . 10 |- ( 0 e. NN0 /\ sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 1 )
106	105	a1i 11	. . . . . . . . 9 |- ( T. -> ( 0 e. NN0 /\ sum_ k e. ( 0 ... 0 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 1 ) )
107		1pneg1e0 11129	. . . . . . . . . 10 |- ( 1 + -u 1 ) = 0
108	107	a1i 11	. . . . . . . . 9 |- ( T. -> ( 1 + -u 1 ) = 0 )
109	86, 87, 96, 103, 106, 108	fsump1i 14500	. . . . . . . 8 |- ( T. -> ( 1 e. NN0 /\ sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 0 ) )
110	109	trud 1493	. . . . . . 7 |- ( 1 e. NN0 /\ sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 0 )
111	110	simpri 478	. . . . . 6 |- sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) = 0
112	111	oveq2i 6661	. . . . 5 |- ( 1 x. sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) = ( 1 x. 0 )
113	70	mul01i 10226	. . . . 5 |- ( 1 x. 0 ) = 0
114	112, 113	eqtr2i 2645	. . . 4 |- 0 = ( 1 x. sum_ k e. ( 0 ... 1 ) ( ( -u 1 ^ k ) / ( ! ` k ) ) )
115	85, 114	pm3.2i 471	. . 3 |- ( 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 477	. . . . 5 |- ( ( ( 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 11	. . . 4 |- ( 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 6659	. . . . . . 7 |- ( ( ( 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 469	. . . . . 6 |- ( ( ( 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 6666	. . . . 5 |- ( ( ( 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 11332	. . . . . . . 8 |- ( m e. NN0 -> ( m + 1 ) e. NN )
122	2, 3	subfacp1 31168	. . . . . . . 8 |- ( ( m + 1 ) e. NN -> ( S ` ( ( m + 1 ) + 1 ) ) = ( ( m + 1 ) x. ( ( S ` ( m + 1 ) ) + ( S ` ( ( m + 1 ) - 1 ) ) ) ) )
123	121, 122	syl 17	. . . . . . 7 |- ( m e. NN0 -> ( S ` ( ( m + 1 ) + 1 ) ) = ( ( m + 1 ) x. ( ( S ` ( m + 1 ) ) + ( S ` ( ( m + 1 ) - 1 ) ) ) ) )
124		nn0cn 11302	. . . . . . . . . . 11 |- ( m e. NN0 -> m e. CC )
125		pncan 10287	. . . . . . . . . . 11 |- ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
126	124, 70, 125	sylancl 694	. . . . . . . . . 10 |- ( m e. NN0 -> ( ( m + 1 ) - 1 ) = m )
127	126	fveq2d 6195	. . . . . . . . 9 |- ( m e. NN0 -> ( S ` ( ( m + 1 ) - 1 ) ) = ( S ` m ) )
128	127	oveq2d 6666	. . . . . . . 8 |- ( m e. NN0 -> ( ( S ` ( m + 1 ) ) + ( S ` ( ( m + 1 ) - 1 ) ) ) = ( ( S ` ( m + 1 ) ) + ( S ` m ) ) )
129	128	oveq2d 6666	. . . . . . 7 |- ( 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 2656	. . . . . 6 |- ( m e. NN0 -> ( S ` ( ( m + 1 ) + 1 ) ) = ( ( m + 1 ) x. ( ( S ` ( m + 1 ) ) + ( S ` m ) ) ) )
131		peano2nn0 11333	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( m + 1 ) e. NN0 )
132		peano2nn0 11333	. . . . . . . . . . . 12 |- ( ( m + 1 ) e. NN0 -> ( ( m + 1 ) + 1 ) e. NN0 )
133	131, 132	syl 17	. . . . . . . . . . 11 |- ( m e. NN0 -> ( ( m + 1 ) + 1 ) e. NN0 )
134		faccl 13070	. . . . . . . . . . 11 |- ( ( ( m + 1 ) + 1 ) e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) e. NN )
135	133, 134	syl 17	. . . . . . . . . 10 |- ( m e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) e. NN )
136	135	nncnd 11036	. . . . . . . . 9 |- ( m e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) e. CC )
137		fzfid 12772	. . . . . . . . . 10 |- ( m e. NN0 -> ( 0 ... ( m + 1 ) ) e. Fin )
138		elfznn0 12433	. . . . . . . . . . . 12 |- ( k e. ( 0 ... ( m + 1 ) ) -> k e. NN0 )
139	138	adantl 482	. . . . . . . . . . 11 |- ( ( m e. NN0 /\ k e. ( 0 ... ( m + 1 ) ) ) -> k e. NN0 )
140	139, 102	syl 17	. . . . . . . . . 10 |- ( ( m e. NN0 /\ k e. ( 0 ... ( m + 1 ) ) ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
141	137, 140	fsumcl 14464	. . . . . . . . 9 |- ( m e. NN0 -> sum_ k e. ( 0 ... ( m + 1 ) ) ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
142		expcl 12878	. . . . . . . . . . 11 |- ( ( -u 1 e. CC /\ ( ( m + 1 ) + 1 ) e. NN0 ) -> ( -u 1 ^ ( ( m + 1 ) + 1 ) ) e. CC )
143	72, 133, 142	sylancr 695	. . . . . . . . . 10 |- ( m e. NN0 -> ( -u 1 ^ ( ( m + 1 ) + 1 ) ) e. CC )
144	135	nnne0d 11065	. . . . . . . . . 10 |- ( m e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) =/= 0 )
145	143, 136, 144	divcld 10801	. . . . . . . . 9 |- ( m e. NN0 -> ( ( -u 1 ^ ( ( m + 1 ) + 1 ) ) / ( ! ` ( ( m + 1 ) + 1 ) ) ) e. CC )
146	136, 141, 145	adddid 10064	. . . . . . . 8 |- ( 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 22	. . . . . . . . . . . . 13 |- ( m e. NN0 -> m e. NN0 )
148	147, 86	syl6eleq 2711	. . . . . . . . . . . 12 |- ( m e. NN0 -> m e. ( ZZ>= ` 0 ) )
149		oveq2 6658	. . . . . . . . . . . . 13 |- ( k = ( m + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( m + 1 ) ) )
150		fveq2 6191	. . . . . . . . . . . . 13 |- ( k = ( m + 1 ) -> ( ! ` k ) = ( ! ` ( m + 1 ) ) )
151	149, 150	oveq12d 6668	. . . . . . . . . . . 12 |- ( k = ( m + 1 ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = ( ( -u 1 ^ ( m + 1 ) ) / ( ! ` ( m + 1 ) ) ) )
152	148, 140, 151	fsump1 14487	. . . . . . . . . . 11 |- ( 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 6666	. . . . . . . . . 10 |- ( 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 12772	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( 0 ... m ) e. Fin )
155		elfznn0 12433	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... m ) -> k e. NN0 )
156	155	adantl 482	. . . . . . . . . . . . 13 |- ( ( m e. NN0 /\ k e. ( 0 ... m ) ) -> k e. NN0 )
157	156, 102	syl 17	. . . . . . . . . . . 12 |- ( ( m e. NN0 /\ k e. ( 0 ... m ) ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
158	154, 157	fsumcl 14464	. . . . . . . . . . 11 |- ( m e. NN0 -> sum_ k e. ( 0 ... m ) ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
159		expcl 12878	. . . . . . . . . . . . 13 |- ( ( -u 1 e. CC /\ ( m + 1 ) e. NN0 ) -> ( -u 1 ^ ( m + 1 ) ) e. CC )
160	72, 131, 159	sylancr 695	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( -u 1 ^ ( m + 1 ) ) e. CC )
161		faccl 13070	. . . . . . . . . . . . . 14 |- ( ( m + 1 ) e. NN0 -> ( ! ` ( m + 1 ) ) e. NN )
162	131, 161	syl 17	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ! ` ( m + 1 ) ) e. NN )
163	162	nncnd 11036	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ! ` ( m + 1 ) ) e. CC )
164	162	nnne0d 11065	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ! ` ( m + 1 ) ) =/= 0 )
165	160, 163, 164	divcld 10801	. . . . . . . . . . 11 |- ( m e. NN0 -> ( ( -u 1 ^ ( m + 1 ) ) / ( ! ` ( m + 1 ) ) ) e. CC )
166	136, 158, 165	adddid 10064	. . . . . . . . . 10 |- ( 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 13065	. . . . . . . . . . . . . 14 |- ( ( m + 1 ) e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) = ( ( ! ` ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) )
168	131, 167	syl 17	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) = ( ( ! ` ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) )
169		facp1 13065	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ! ` ( m + 1 ) ) = ( ( ! ` m ) x. ( m + 1 ) ) )
170		faccl 13070	. . . . . . . . . . . . . . . . 17 |- ( m e. NN0 -> ( ! ` m ) e. NN )
171	170	nncnd 11036	. . . . . . . . . . . . . . . 16 |- ( m e. NN0 -> ( ! ` m ) e. CC )
172	121	nncnd 11036	. . . . . . . . . . . . . . . 16 |- ( m e. NN0 -> ( m + 1 ) e. CC )
173	171, 172	mulcomd 10061	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ( ! ` m ) x. ( m + 1 ) ) = ( ( m + 1 ) x. ( ! ` m ) ) )
174	169, 173	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ! ` ( m + 1 ) ) = ( ( m + 1 ) x. ( ! ` m ) ) )
175	174	oveq1d 6665	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ! ` ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) = ( ( ( m + 1 ) x. ( ! ` m ) ) x. ( ( m + 1 ) + 1 ) ) )
176	133	nn0cnd 11353	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( m + 1 ) + 1 ) e. CC )
177	172, 171, 176	mulassd 10063	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ( m + 1 ) x. ( ! ` m ) ) x. ( ( m + 1 ) + 1 ) ) = ( ( m + 1 ) x. ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) ) )
178	168, 175, 177	3eqtrd 2660	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ! ` ( ( m + 1 ) + 1 ) ) = ( ( m + 1 ) x. ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) ) )
179	178	oveq1d 6665	. . . . . . . . . . 11 |- ( 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 10837	. . . . . . . . . . . 12 |- ( 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 6665	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ! ` ( ( m + 1 ) + 1 ) ) / ( ! ` ( m + 1 ) ) ) = ( ( ( ! ` ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) / ( ! ` ( m + 1 ) ) ) )
182	176, 163, 164	divcan3d 10806	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ( ! ` ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) / ( ! ` ( m + 1 ) ) ) = ( ( m + 1 ) + 1 ) )
183	181, 182	eqtrd 2656	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ! ` ( ( m + 1 ) + 1 ) ) / ( ! ` ( m + 1 ) ) ) = ( ( m + 1 ) + 1 ) )
184	183	oveq2d 6666	. . . . . . . . . . . 12 |- ( 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 2656	. . . . . . . . . . 11 |- ( 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 6668	. . . . . . . . . 10 |- ( 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 2660	. . . . . . . . 9 |- ( 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 10803	. . . . . . . . 9 |- ( m e. NN0 -> ( ( ! ` ( ( m + 1 ) + 1 ) ) x. ( ( -u 1 ^ ( ( m + 1 ) + 1 ) ) / ( ! ` ( ( m + 1 ) + 1 ) ) ) ) = ( -u 1 ^ ( ( m + 1 ) + 1 ) ) )
189	187, 188	oveq12d 6668	. . . . . . . 8 |- ( 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 10060	. . . . . . . . . . 11 |- ( m e. NN0 -> ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) e. CC )
191	172, 190, 158	mulassd 10063	. . . . . . . . . 10 |- ( 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 11	. . . . . . . . . . . . 13 |- ( m e. NN0 -> -u 1 e. CC )
193	160, 176, 192	adddid 10064	. . . . . . . . . . . 12 |- ( 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 10329	. . . . . . . . . . . . . . 15 |- ( ( ( ( m + 1 ) + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( m + 1 ) + 1 ) + -u 1 ) = ( ( ( m + 1 ) + 1 ) - 1 ) )
195	176, 70, 194	sylancl 694	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ( m + 1 ) + 1 ) + -u 1 ) = ( ( ( m + 1 ) + 1 ) - 1 ) )
196		pncan 10287	. . . . . . . . . . . . . . 15 |- ( ( ( m + 1 ) e. CC /\ 1 e. CC ) -> ( ( ( m + 1 ) + 1 ) - 1 ) = ( m + 1 ) )
197	172, 70, 196	sylancl 694	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ( m + 1 ) + 1 ) - 1 ) = ( m + 1 ) )
198	195, 197	eqtrd 2656	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ( m + 1 ) + 1 ) + -u 1 ) = ( m + 1 ) )
199	198	oveq2d 6666	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ( -u 1 ^ ( m + 1 ) ) x. ( ( ( m + 1 ) + 1 ) + -u 1 ) ) = ( ( -u 1 ^ ( m + 1 ) ) x. ( m + 1 ) ) )
200	193, 199	eqtr3d 2658	. . . . . . . . . . 11 |- ( 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 12867	. . . . . . . . . . . . 13 |- ( ( -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 695	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( -u 1 ^ ( ( m + 1 ) + 1 ) ) = ( ( -u 1 ^ ( m + 1 ) ) x. -u 1 ) )
203	202	oveq2d 6666	. . . . . . . . . . 11 |- ( 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 10061	. . . . . . . . . . 11 |- ( m e. NN0 -> ( ( m + 1 ) x. ( -u 1 ^ ( m + 1 ) ) ) = ( ( -u 1 ^ ( m + 1 ) ) x. ( m + 1 ) ) )
205	200, 203, 204	3eqtr4d 2666	. . . . . . . . . 10 |- ( 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 6668	. . . . . . . . 9 |- ( 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 10060	. . . . . . . . . . 11 |- ( m e. NN0 -> ( ( m + 1 ) x. ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) ) e. CC )
208	207, 158	mulcld 10060	. . . . . . . . . 10 |- ( 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 10060	. . . . . . . . . 10 |- ( m e. NN0 -> ( ( -u 1 ^ ( m + 1 ) ) x. ( ( m + 1 ) + 1 ) ) e. CC )
210	208, 209, 143	addassd 10062	. . . . . . . . 9 |- ( 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 10060	. . . . . . . . . 10 |- ( 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 10064	. . . . . . . . 9 |- ( 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 2666	. . . . . . . 8 |- ( 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 2660	. . . . . . 7 |- ( 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	syl6eleq 2711	. . . . . . . . 9 |- ( m e. NN0 -> ( m + 1 ) e. ( ZZ>= ` 0 ) )
216		elfznn0 12433	. . . . . . . . . . 11 |- ( k e. ( 0 ... ( ( m + 1 ) + 1 ) ) -> k e. NN0 )
217	216	adantl 482	. . . . . . . . . 10 |- ( ( m e. NN0 /\ k e. ( 0 ... ( ( m + 1 ) + 1 ) ) ) -> k e. NN0 )
218	217, 102	syl 17	. . . . . . . . 9 |- ( ( m e. NN0 /\ k e. ( 0 ... ( ( m + 1 ) + 1 ) ) ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) e. CC )
219		oveq2 6658	. . . . . . . . . 10 |- ( k = ( ( m + 1 ) + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ( m + 1 ) + 1 ) ) )
220		fveq2 6191	. . . . . . . . . 10 |- ( k = ( ( m + 1 ) + 1 ) -> ( ! ` k ) = ( ! ` ( ( m + 1 ) + 1 ) ) )
221	219, 220	oveq12d 6668	. . . . . . . . 9 |- ( k = ( ( m + 1 ) + 1 ) -> ( ( -u 1 ^ k ) / ( ! ` k ) ) = ( ( -u 1 ^ ( ( m + 1 ) + 1 ) ) / ( ! ` ( ( m + 1 ) + 1 ) ) ) )
222	215, 218, 221	fsump1 14487	. . . . . . . 8 |- ( 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 6666	. . . . . . 7 |- ( 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 10060	. . . . . . . . . 10 |- ( m e. NN0 -> ( ( ! ` ( m + 1 ) ) x. sum_ k e. ( 0 ... m ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) e. CC )
225	171, 158	mulcld 10060	. . . . . . . . . 10 |- ( m e. NN0 -> ( ( ! ` m ) x. sum_ k e. ( 0 ... m ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) e. CC )
226	224, 160, 225	add32d 10263	. . . . . . . . 9 |- ( 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 6666	. . . . . . . . . . 11 |- ( 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 10064	. . . . . . . . . . 11 |- ( 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 10803	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ( ! ` ( m + 1 ) ) x. ( ( -u 1 ^ ( m + 1 ) ) / ( ! ` ( m + 1 ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) )
230	229	oveq2d 6666	. . . . . . . . . . 11 |- ( 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 2660	. . . . . . . . . 10 |- ( 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 6665	. . . . . . . . 9 |- ( 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 11	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> 1 e. CC )
234	171, 172, 233	adddid 10064	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) = ( ( ( ! ` m ) x. ( m + 1 ) ) + ( ( ! ` m ) x. 1 ) ) )
235	169	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ! ` m ) x. ( m + 1 ) ) = ( ! ` ( m + 1 ) ) )
236	171	mulid1d 10057	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( ( ! ` m ) x. 1 ) = ( ! ` m ) )
237	235, 236	oveq12d 6668	. . . . . . . . . . . . 13 |- ( m e. NN0 -> ( ( ( ! ` m ) x. ( m + 1 ) ) + ( ( ! ` m ) x. 1 ) ) = ( ( ! ` ( m + 1 ) ) + ( ! ` m ) ) )
238	234, 237	eqtrd 2656	. . . . . . . . . . . 12 |- ( m e. NN0 -> ( ( ! ` m ) x. ( ( m + 1 ) + 1 ) ) = ( ( ! ` ( m + 1 ) ) + ( ! ` m ) ) )
239	238	oveq1d 6665	. . . . . . . . . . 11 |- ( 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 10065	. . . . . . . . . . 11 |- ( 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 2656	. . . . . . . . . 10 |- ( 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 6665	. . . . . . . . 9 |- ( 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 2666	. . . . . . . 8 |- ( 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 6666	. . . . . . 7 |- ( 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 2666	. . . . . 6 |- ( 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 2637	. . . . 5 |- ( 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 236	. . . 4 |- ( 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 555	. . 3 |- ( 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 11472	. 2 |- ( 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 475	1 |- ( N e. NN0 -> ( S ` N ) = ( ( ! ` N ) x. sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) / ( ! ` k ) ) ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   T. wtru 1484   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   |-> cmpt 4729   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   ^cexp 12860   !cfa 13060   #chash 13117   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-fac 13061  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417

This theorem is referenced by:  subfaclim  31170