Theorem ballotlemfval0

Description: ( FC ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016)

	Ref	Expression
Hypotheses	ballotth.m	|- M e. NN
	ballotth.n	|- N e. NN
	ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
	ballotth.p	|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
	ballotth.f	|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
Assertion	ballotlemfval0	|- ( C e. O -> ( ( F ` C ) ` 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	|- M e. NN
2		ballotth.n	|- N e. NN
3		ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4		ballotth.p	|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5		ballotth.f	|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
6		id	|- ( C e. O -> C e. O )
7		0zd	|- ( C e. O -> 0 e. ZZ )
8	1 2 3 4 5 6 7	ballotlemfval	|- ( C e. O -> ( ( F ` C ) ` 0 ) = ( ( # ` ( ( 1 ... 0 ) i^i C ) ) - ( # ` ( ( 1 ... 0 ) \ C ) ) ) )
9		fz10	|- ( 1 ... 0 ) = (/)
10	9	ineq1i	|- ( ( 1 ... 0 ) i^i C ) = ( (/) i^i C )
11		incom	|- ( C i^i (/) ) = ( (/) i^i C )
12		in0	|- ( C i^i (/) ) = (/)
13	10 11 12	3eqtr2i	|- ( ( 1 ... 0 ) i^i C ) = (/)
14	13	fveq2i	|- ( # ` ( ( 1 ... 0 ) i^i C ) ) = ( # ` (/) )
15		hash0	|- ( # ` (/) ) = 0
16	14 15	eqtri	|- ( # ` ( ( 1 ... 0 ) i^i C ) ) = 0
17	9	difeq1i	|- ( ( 1 ... 0 ) \ C ) = ( (/) \ C )
18		0dif	|- ( (/) \ C ) = (/)
19	17 18	eqtri	|- ( ( 1 ... 0 ) \ C ) = (/)
20	19	fveq2i	|- ( # ` ( ( 1 ... 0 ) \ C ) ) = ( # ` (/) )
21	20 15	eqtri	|- ( # ` ( ( 1 ... 0 ) \ C ) ) = 0
22	16 21	oveq12i	|- ( ( # ` ( ( 1 ... 0 ) i^i C ) ) - ( # ` ( ( 1 ... 0 ) \ C ) ) ) = ( 0 - 0 )
23		0m0e0	|- ( 0 - 0 ) = 0
24	22 23	eqtri	|- ( ( # ` ( ( 1 ... 0 ) i^i C ) ) - ( # ` ( ( 1 ... 0 ) \ C ) ) ) = 0
25	8 24	eqtrdi	|- ( C e. O -> ( ( F ` C ) ` 0 ) = 0 )