Theorem sticksstones12a

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 11-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones12a.1	|- ( ph -> N e. NN0 )
	sticksstones12a.2	|- ( ph -> K e. NN )
	sticksstones12a.3	|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
	sticksstones12a.4	|- G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
	sticksstones12a.5	|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
	sticksstones12a.6	|- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion	sticksstones12a	|- ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )

Proof

Step	Hyp	Ref	Expression
1		sticksstones12a.1	|- ( ph -> N e. NN0 )
2		sticksstones12a.2	|- ( ph -> K e. NN )
3		sticksstones12a.3	|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
4		sticksstones12a.4	|- G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
5		sticksstones12a.5	|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
6		sticksstones12a.6	|- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
7	4	a1i	|- ( ( ph /\ d e. B ) -> G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) ) )
8		0red	|- ( ph -> 0 e. RR )
9	2	nngt0d	|- ( ph -> 0 < K )
10	8 9	ltned	|- ( ph -> 0 =/= K )
11	10	necomd	|- ( ph -> K =/= 0 )
12	11	neneqd	|- ( ph -> -. K = 0 )
13	12	ad2antrr	|- ( ( ( ph /\ d e. B ) /\ b = d ) -> -. K = 0 )
14	13	iffalsed	|- ( ( ( ph /\ d e. B ) /\ b = d ) -> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) )
15		fveq1	|- ( b = d -> ( b ` K ) = ( d ` K ) )
16	15	oveq2d	|- ( b = d -> ( ( N + K ) - ( b ` K ) ) = ( ( N + K ) - ( d ` K ) ) )
17		fveq1	|- ( b = d -> ( b ` 1 ) = ( d ` 1 ) )
18	17	oveq1d	|- ( b = d -> ( ( b ` 1 ) - 1 ) = ( ( d ` 1 ) - 1 ) )
19		fveq1	|- ( b = d -> ( b ` k ) = ( d ` k ) )
20		fveq1	|- ( b = d -> ( b ` ( k - 1 ) ) = ( d ` ( k - 1 ) ) )
21	19 20	oveq12d	|- ( b = d -> ( ( b ` k ) - ( b ` ( k - 1 ) ) ) = ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
22	21	oveq1d	|- ( b = d -> ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) = ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) )
23	18 22	ifeq12d	|- ( b = d -> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
24	16 23	ifeq12d	|- ( b = d -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
25	24	adantl	|- ( ( ( ph /\ d e. B ) /\ b = d ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
26	25	adantr	|- ( ( ( ( ph /\ d e. B ) /\ b = d ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
27	26	mpteq2dva	|- ( ( ( ph /\ d e. B ) /\ b = d ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
28	14 27	eqtrd	|- ( ( ( ph /\ d e. B ) /\ b = d ) -> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
29		simpr	|- ( ( ph /\ d e. B ) -> d e. B )
30		fzfid	|- ( ( ph /\ d e. B ) -> ( 1 ... ( K + 1 ) ) e. Fin )
31	30	mptexd	|- ( ( ph /\ d e. B ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. _V )
32	7 28 29 31	fvmptd	|- ( ( ph /\ d e. B ) -> ( G ` d ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
33	32	fveq2d	|- ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = ( F ` ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
34	3	a1i	|- ( ( ph /\ d e. B ) -> F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) ) )
35		simpll	|- ( ( ( a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
36	35	fveq1d	|- ( ( ( a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( a ` l ) = ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) )
37	36	sumeq2dv	|- ( ( a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) ( a ` l ) = sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) )
38	37	oveq2d	|- ( ( a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) = ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) )
39	38	mpteq2dva	|- ( a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) )
40	39	adantl	|- ( ( ( ph /\ d e. B ) /\ a = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) )
41		eleq1	|- ( ( ( N + K ) - ( d ` K ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) -> ( ( ( N + K ) - ( d ` K ) ) e. NN0 <-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) e. NN0 ) )
42		eleq1	|- ( if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) -> ( if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. NN0 <-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) e. NN0 ) )
43	6	eleq2i	|- ( d e. B <-> d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
44		vex	|- d e. _V
45		feq1	|- ( f = d -> ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) ) )
46		fveq1	|- ( f = d -> ( f ` x ) = ( d ` x ) )
47		fveq1	|- ( f = d -> ( f ` y ) = ( d ` y ) )
48	46 47	breq12d	|- ( f = d -> ( ( f ` x ) < ( f ` y ) <-> ( d ` x ) < ( d ` y ) ) )
49	48	imbi2d	|- ( f = d -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
50	49	2ralbidv	|- ( f = d -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
51	45 50	anbi12d	|- ( f = d -> ( ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) ) )
52	44 51	elab	|- ( d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
53	43 52	bitri	|- ( d e. B <-> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
54	53	biimpi	|- ( d e. B -> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
55	54	adantl	|- ( ( ph /\ d e. B ) -> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
56	55	simpld	|- ( ( ph /\ d e. B ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
57		1zzd	|- ( ph -> 1 e. ZZ )
58	57	adantr	|- ( ( ph /\ d e. B ) -> 1 e. ZZ )
59	2	nnnn0d	|- ( ph -> K e. NN0 )
60	59	nn0zd	|- ( ph -> K e. ZZ )
61	60	adantr	|- ( ( ph /\ d e. B ) -> K e. ZZ )
62	2	nnge1d	|- ( ph -> 1 <_ K )
63	62	adantr	|- ( ( ph /\ d e. B ) -> 1 <_ K )
64	2	nnred	|- ( ph -> K e. RR )
65	64	leidd	|- ( ph -> K <_ K )
66	65	adantr	|- ( ( ph /\ d e. B ) -> K <_ K )
67	58 61 61 63 66	elfzd	|- ( ( ph /\ d e. B ) -> K e. ( 1 ... K ) )
68	56 67	ffvelcdmd	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. ( 1 ... ( N + K ) ) )
69		elfzle2	|- ( ( d ` K ) e. ( 1 ... ( N + K ) ) -> ( d ` K ) <_ ( N + K ) )
70	68 69	syl	|- ( ( ph /\ d e. B ) -> ( d ` K ) <_ ( N + K ) )
71	70	adantr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( d ` K ) <_ ( N + K ) )
72	71	adantr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( d ` K ) <_ ( N + K ) )
73		elfznn	|- ( ( d ` K ) e. ( 1 ... ( N + K ) ) -> ( d ` K ) e. NN )
74	73	nnnn0d	|- ( ( d ` K ) e. ( 1 ... ( N + K ) ) -> ( d ` K ) e. NN0 )
75	68 74	syl	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. NN0 )
76	75	adantr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( d ` K ) e. NN0 )
77	76	adantr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( d ` K ) e. NN0 )
78	1	ad3antrrr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> N e. NN0 )
79	59	ad3antrrr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> K e. NN0 )
80	78 79	nn0addcld	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( N + K ) e. NN0 )
81		nn0sub	|- ( ( ( d ` K ) e. NN0 /\ ( N + K ) e. NN0 ) -> ( ( d ` K ) <_ ( N + K ) <-> ( ( N + K ) - ( d ` K ) ) e. NN0 ) )
82	77 80 81	syl2anc	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( d ` K ) <_ ( N + K ) <-> ( ( N + K ) - ( d ` K ) ) e. NN0 ) )
83	72 82	mpbid	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( d ` K ) ) e. NN0 )
84		eleq1	|- ( ( ( d ` 1 ) - 1 ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( d ` 1 ) - 1 ) e. NN0 <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. NN0 ) )
85		eleq1	|- ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. NN0 <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. NN0 ) )
86		1le1	|- 1 <_ 1
87	86	a1i	|- ( ( ph /\ d e. B ) -> 1 <_ 1 )
88	58 61 58 87 63	elfzd	|- ( ( ph /\ d e. B ) -> 1 e. ( 1 ... K ) )
89	56 88	ffvelcdmd	|- ( ( ph /\ d e. B ) -> ( d ` 1 ) e. ( 1 ... ( N + K ) ) )
90		elfznn	|- ( ( d ` 1 ) e. ( 1 ... ( N + K ) ) -> ( d ` 1 ) e. NN )
91	89 90	syl	|- ( ( ph /\ d e. B ) -> ( d ` 1 ) e. NN )
92		nnm1nn0	|- ( ( d ` 1 ) e. NN -> ( ( d ` 1 ) - 1 ) e. NN0 )
93	91 92	syl	|- ( ( ph /\ d e. B ) -> ( ( d ` 1 ) - 1 ) e. NN0 )
94	93	adantr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( d ` 1 ) - 1 ) e. NN0 )
95	94	adantr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( ( d ` 1 ) - 1 ) e. NN0 )
96	95	adantr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( d ` 1 ) - 1 ) e. NN0 )
97	56	ad3antrrr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
98		1zzd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
99	61	ad3antrrr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
100		elfznn	|- ( k e. ( 1 ... ( K + 1 ) ) -> k e. NN )
101	100	nnzd	|- ( k e. ( 1 ... ( K + 1 ) ) -> k e. ZZ )
102	101	ad3antlr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
103		elfzle1	|- ( k e. ( 1 ... ( K + 1 ) ) -> 1 <_ k )
104	103	ad3antlr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
105		neqne	|- ( -. k = ( K + 1 ) -> k =/= ( K + 1 ) )
106	105	adantl	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k =/= ( K + 1 ) )
107	106	necomd	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) =/= k )
108	100	ad2antlr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. NN )
109	108	nnred	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. RR )
110	64	ad3antrrr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. RR )
111		1red	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 e. RR )
112	110 111	readdcld	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. RR )
113		elfzle2	|- ( k e. ( 1 ... ( K + 1 ) ) -> k <_ ( K + 1 ) )
114	113	ad2antlr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ ( K + 1 ) )
115	109 112 114	leltned	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k < ( K + 1 ) <-> ( K + 1 ) =/= k ) )
116	107 115	mpbird	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k < ( K + 1 ) )
117	101	ad2antlr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ZZ )
118	61	ad2antrr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. ZZ )
119		zleltp1	|- ( ( k e. ZZ /\ K e. ZZ ) -> ( k <_ K <-> k < ( K + 1 ) ) )
120	117 118 119	syl2anc	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ K <-> k < ( K + 1 ) ) )
121	116 120	mpbird	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ K )
122	121	adantr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k <_ K )
123	98 99 102 104 122	elfzd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... K ) )
124	97 123	ffvelcdmd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` k ) e. ( 1 ... ( N + K ) ) )
125		elfznn	|- ( ( d ` k ) e. ( 1 ... ( N + K ) ) -> ( d ` k ) e. NN )
126	125	nnzd	|- ( ( d ` k ) e. ( 1 ... ( N + K ) ) -> ( d ` k ) e. ZZ )
127	124 126	syl	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` k ) e. ZZ )
128		1zzd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
129	60	ad2antrr	|- ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> K e. ZZ )
130	129	3impa	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
131	101	adantl	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
132	131	adantr	|- ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> k e. ZZ )
133	132	3impa	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
134	133 128	zsubcld	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
135		neqne	|- ( -. k = 1 -> k =/= 1 )
136	135	3ad2ant3	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k =/= 1 )
137		1red	|- ( ph -> 1 e. RR )
138	137	3ad2ant1	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
139	133	zred	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. RR )
140		simp2	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... ( K + 1 ) ) )
141	140 103	syl	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
142	138 139 141	leltned	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> k =/= 1 ) )
143	136 142	mpbird	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 < k )
144	128 133	zltp1led	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
145	143 144	mpbid	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 + 1 ) <_ k )
146		leaddsub	|- ( ( 1 e. RR /\ 1 e. RR /\ k e. RR ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
147	138 138 139 146	syl3anc	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
148	145 147	mpbid	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
149	134	zred	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
150	64	3ad2ant1	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. RR )
151		1red	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
152	150 151	readdcld	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( K + 1 ) e. RR )
153	152 151	resubcld	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) e. RR )
154	113	3ad2ant2	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k <_ ( K + 1 ) )
155	139 152 151 154	lesub1dd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( ( K + 1 ) - 1 ) )
156	64	recnd	|- ( ph -> K e. CC )
157	156	3ad2ant1	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. CC )
158		1cnd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
159	157 158	pncand	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) = K )
160	65	3ad2ant1	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K <_ K )
161	159 160	eqbrtrd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) <_ K )
162	149 153 150 155 161	letrd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
163	128 130 134 148 162	elfzd	|- ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
164	163	ad5ant135	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
165	97 164	ffvelcdmd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) )
166		elfznn	|- ( ( d ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( k - 1 ) ) e. NN )
167	165 166	syl	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. NN )
168	167	nnzd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ZZ )
169	127 168	zsubcld	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) e. ZZ )
170	169 98	zsubcld	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. ZZ )
171	108	adantr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. NN )
172	171	nnred	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. RR )
173	172	ltm1d	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) < k )
174	164 123	jca	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - 1 ) e. ( 1 ... K ) /\ k e. ( 1 ... K ) ) )
175	55	simprd	|- ( ( ph /\ d e. B ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) )
176	175	ad3antrrr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) )
177		breq1	|- ( x = ( k - 1 ) -> ( x < y <-> ( k - 1 ) < y ) )
178		fveq2	|- ( x = ( k - 1 ) -> ( d ` x ) = ( d ` ( k - 1 ) ) )
179	178	breq1d	|- ( x = ( k - 1 ) -> ( ( d ` x ) < ( d ` y ) <-> ( d ` ( k - 1 ) ) < ( d ` y ) ) )
180	177 179	imbi12d	|- ( x = ( k - 1 ) -> ( ( x < y -> ( d ` x ) < ( d ` y ) ) <-> ( ( k - 1 ) < y -> ( d ` ( k - 1 ) ) < ( d ` y ) ) ) )
181		breq2	|- ( y = k -> ( ( k - 1 ) < y <-> ( k - 1 ) < k ) )
182		fveq2	|- ( y = k -> ( d ` y ) = ( d ` k ) )
183	182	breq2d	|- ( y = k -> ( ( d ` ( k - 1 ) ) < ( d ` y ) <-> ( d ` ( k - 1 ) ) < ( d ` k ) ) )
184	181 183	imbi12d	|- ( y = k -> ( ( ( k - 1 ) < y -> ( d ` ( k - 1 ) ) < ( d ` y ) ) <-> ( ( k - 1 ) < k -> ( d ` ( k - 1 ) ) < ( d ` k ) ) ) )
185	180 184	rspc2va	|- ( ( ( ( k - 1 ) e. ( 1 ... K ) /\ k e. ( 1 ... K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) -> ( ( k - 1 ) < k -> ( d ` ( k - 1 ) ) < ( d ` k ) ) )
186	174 176 185	syl2anc	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - 1 ) < k -> ( d ` ( k - 1 ) ) < ( d ` k ) ) )
187	173 186	mpd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) < ( d ` k ) )
188	167	nnred	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. RR )
189	127	zred	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( d ` k ) e. RR )
190	188 189	posdifd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( d ` ( k - 1 ) ) < ( d ` k ) <-> 0 < ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
191	187 190	mpbid	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 < ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
192		0zd	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 e. ZZ )
193	192 169	zltlem1d	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 0 < ( ( d ` k ) - ( d ` ( k - 1 ) ) ) <-> 0 <_ ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
194	191 193	mpbid	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 <_ ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) )
195	170 194	jca	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. ZZ /\ 0 <_ ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
196		elnn0z	|- ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. NN0 <-> ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. ZZ /\ 0 <_ ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
197	195 196	sylibr	|- ( ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. NN0 )
198	84 85 96 197	ifbothda	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. NN0 )
199	41 42 83 198	ifbothda	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) e. NN0 )
200		eqid	|- ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
201	199 200	fmptd	|- ( ( ph /\ d e. B ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 )
202		eqidd	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
203		simpr	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> k = i )
204	203	eqeq1d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( k = ( K + 1 ) <-> i = ( K + 1 ) ) )
205	203	eqeq1d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( k = 1 <-> i = 1 ) )
206	203	fveq2d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( d ` k ) = ( d ` i ) )
207	203	fvoveq1d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( d ` ( k - 1 ) ) = ( d ` ( i - 1 ) ) )
208	206 207	oveq12d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` i ) - ( d ` ( i - 1 ) ) ) )
209	208	oveq1d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) )
210	205 209	ifbieq2d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) )
211	204 210	ifbieq2d	|- ( ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) )
212		simpr	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. ( 1 ... ( K + 1 ) ) )
213		ovexd	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( d ` K ) ) e. _V )
214		ovexd	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( d ` 1 ) - 1 ) e. _V )
215		ovexd	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) e. _V )
216	214 215	ifcld	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) e. _V )
217	213 216	ifcld	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) e. _V )
218	202 211 212 217	fvmptd	|- ( ( ( ph /\ d e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) )
219	218	sumeq2dv	|- ( ( ph /\ d e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) )
220		eqeq1	|- ( i = k -> ( i = ( K + 1 ) <-> k = ( K + 1 ) ) )
221		eqeq1	|- ( i = k -> ( i = 1 <-> k = 1 ) )
222		fveq2	|- ( i = k -> ( d ` i ) = ( d ` k ) )
223		fvoveq1	|- ( i = k -> ( d ` ( i - 1 ) ) = ( d ` ( k - 1 ) ) )
224	222 223	oveq12d	|- ( i = k -> ( ( d ` i ) - ( d ` ( i - 1 ) ) ) = ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
225	224	oveq1d	|- ( i = k -> ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) = ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) )
226	221 225	ifbieq2d	|- ( i = k -> if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
227	220 226	ifbieq2d	|- ( i = k -> if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
228		nfcv	|- F/_ k if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) )
229		nfcv	|- F/_ i if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
230	227 228 229	cbvsum	|- sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) = sum_ k e. ( 1 ... ( K + 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
231	230	a1i	|- ( ( ph /\ d e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) = sum_ k e. ( 1 ... ( K + 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
232		eqid	|- 1 = 1
233		1p0e1	|- ( 1 + 0 ) = 1
234	232 233	eqtr4i	|- 1 = ( 1 + 0 )
235	234	a1i	|- ( ph -> 1 = ( 1 + 0 ) )
236		0le1	|- 0 <_ 1
237	236	a1i	|- ( ph -> 0 <_ 1 )
238	137 8 64 137 62 237	le2addd	|- ( ph -> ( 1 + 0 ) <_ ( K + 1 ) )
239	235 238	eqbrtrd	|- ( ph -> 1 <_ ( K + 1 ) )
240	60	peano2zd	|- ( ph -> ( K + 1 ) e. ZZ )
241		eluz	|- ( ( 1 e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( ( K + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( K + 1 ) ) )
242	57 240 241	syl2anc	|- ( ph -> ( ( K + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( K + 1 ) ) )
243	239 242	mpbird	|- ( ph -> ( K + 1 ) e. ( ZZ>= ` 1 ) )
244	243	adantr	|- ( ( ph /\ d e. B ) -> ( K + 1 ) e. ( ZZ>= ` 1 ) )
245	199	nn0cnd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) e. CC )
246		eqeq1	|- ( k = ( K + 1 ) -> ( k = ( K + 1 ) <-> ( K + 1 ) = ( K + 1 ) ) )
247		eqeq1	|- ( k = ( K + 1 ) -> ( k = 1 <-> ( K + 1 ) = 1 ) )
248		fveq2	|- ( k = ( K + 1 ) -> ( d ` k ) = ( d ` ( K + 1 ) ) )
249		fvoveq1	|- ( k = ( K + 1 ) -> ( d ` ( k - 1 ) ) = ( d ` ( ( K + 1 ) - 1 ) ) )
250	248 249	oveq12d	|- ( k = ( K + 1 ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) )
251	250	oveq1d	|- ( k = ( K + 1 ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) )
252	247 251	ifbieq2d	|- ( k = ( K + 1 ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) )
253	246 252	ifbieq2d	|- ( k = ( K + 1 ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) )
254	244 245 253	fsumm1	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... ( K + 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = ( sum_ k e. ( 1 ... ( ( K + 1 ) - 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) )
255	156	adantr	|- ( ( ph /\ d e. B ) -> K e. CC )
256		1cnd	|- ( ( ph /\ d e. B ) -> 1 e. CC )
257	255 256	pncand	|- ( ( ph /\ d e. B ) -> ( ( K + 1 ) - 1 ) = K )
258	257	oveq2d	|- ( ( ph /\ d e. B ) -> ( 1 ... ( ( K + 1 ) - 1 ) ) = ( 1 ... K ) )
259	258	sumeq1d	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... ( ( K + 1 ) - 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = sum_ k e. ( 1 ... K ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) )
260		eqidd	|- ( ( ph /\ d e. B ) -> ( K + 1 ) = ( K + 1 ) )
261	260	iftrued	|- ( ( ph /\ d e. B ) -> if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) = ( ( N + K ) - ( d ` K ) ) )
262	259 261	oveq12d	|- ( ( ph /\ d e. B ) -> ( sum_ k e. ( 1 ... ( ( K + 1 ) - 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) = ( sum_ k e. ( 1 ... K ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) + ( ( N + K ) - ( d ` K ) ) ) )
263	1	nn0cnd	|- ( ph -> N e. CC )
264	263	adantr	|- ( ( ph /\ d e. B ) -> N e. CC )
265	264 255	addcld	|- ( ( ph /\ d e. B ) -> ( N + K ) e. CC )
266	68 73	syl	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. NN )
267	266	nncnd	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. CC )
268	265 267	subcld	|- ( ( ph /\ d e. B ) -> ( ( N + K ) - ( d ` K ) ) e. CC )
269		elfzelz	|- ( k e. ( 1 ... K ) -> k e. ZZ )
270	269	adantl	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k e. ZZ )
271	270	zred	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k e. RR )
272	64	ad2antrr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> K e. RR )
273		1red	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> 1 e. RR )
274	272 273	readdcld	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
275		elfzle2	|- ( k e. ( 1 ... K ) -> k <_ K )
276	275	adantl	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k <_ K )
277	272	ltp1d	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> K < ( K + 1 ) )
278	271 272 274 276 277	lelttrd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k < ( K + 1 ) )
279	271 278	ltned	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k =/= ( K + 1 ) )
280	279	neneqd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> -. k = ( K + 1 ) )
281	280	iffalsed	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
282	281	sumeq2dv	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) )
283		eqeq1	|- ( ( ( d ` 1 ) - 1 ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( d ` 1 ) - 1 ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) ) )
284		eqeq1	|- ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) ) )
285		simpr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> k = 1 )
286	285	iftrued	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
287	286	eqcomd	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( d ` 1 ) = if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
288	287	oveq1d	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( ( d ` 1 ) - 1 ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) )
289		simpr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> -. k = 1 )
290	289	iffalsed	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
291	290	eqcomd	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
292	291	oveq1d	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) )
293	283 284 288 292	ifbothda	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) )
294	293	sumeq2dv	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = sum_ k e. ( 1 ... K ) ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) )
295		fzfid	|- ( ( ph /\ d e. B ) -> ( 1 ... K ) e. Fin )
296		eleq1	|- ( ( d ` 1 ) = if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) -> ( ( d ` 1 ) e. ZZ <-> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ ) )
297		eleq1	|- ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) e. ZZ <-> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ ) )
298	56	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
299	88	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> 1 e. ( 1 ... K ) )
300	298 299	ffvelcdmd	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` 1 ) e. ( 1 ... ( N + K ) ) )
301	90	nnzd	|- ( ( d ` 1 ) e. ( 1 ... ( N + K ) ) -> ( d ` 1 ) e. ZZ )
302	300 301	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` 1 ) e. ZZ )
303	302	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( d ` 1 ) e. ZZ )
304		simp3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k e. ( 1 ... K ) )
305	298 304	ffvelcdmd	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` k ) e. ( 1 ... ( N + K ) ) )
306	305 126	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` k ) e. ZZ )
307	306	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` k ) e. ZZ )
308	298	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
309		1zzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 e. ZZ )
310	61	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> K e. ZZ )
311	310	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> K e. ZZ )
312	270	3impa	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k e. ZZ )
313	312	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k e. ZZ )
314	313 309	zsubcld	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
315		elfzle1	|- ( k e. ( 1 ... K ) -> 1 <_ k )
316	304 315	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> 1 <_ k )
317	316	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 <_ k )
318	135	adantl	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k =/= 1 )
319	317 318	jca	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 <_ k /\ k =/= 1 ) )
320		1red	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 e. RR )
321	313	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k e. RR )
322	320 321	ltlend	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 <_ k /\ k =/= 1 ) ) )
323	319 322	mpbird	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 < k )
324	309 313	zltlem1d	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 < k <-> 1 <_ ( k - 1 ) ) )
325	323 324	mpbid	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
326	314	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
327	311	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> K e. RR )
328	321	lem1d	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ k )
329	304 275	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k <_ K )
330	329	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k <_ K )
331	326 321 327 328 330	letrd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
332	309 311 314 325 331	elfzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
333	308 332	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) )
334	333 166	syl	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. NN )
335	334	nnzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ZZ )
336	307 335	zsubcld	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) e. ZZ )
337	296 297 303 336	ifbothda	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ )
338	337	3expa	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ )
339	338	zcnd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. CC )
340	256	adantr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> 1 e. CC )
341	295 339 340	fsumsub	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) = ( sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - sum_ k e. ( 1 ... K ) 1 ) )
342		simpr	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> 1 = K )
343	342	oveq2d	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( 1 ... 1 ) = ( 1 ... K ) )
344	343	eqcomd	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( 1 ... K ) = ( 1 ... 1 ) )
345	344	sumeq1d	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
346		1zzd	|- ( ( ph /\ d e. B ) -> 1 e. ZZ )
347	232	a1i	|- ( ( ph /\ d e. B ) -> 1 = 1 )
348	347	iftrued	|- ( ( ph /\ d e. B ) -> if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) = ( d ` 1 ) )
349	91	nncnd	|- ( ( ph /\ d e. B ) -> ( d ` 1 ) e. CC )
350	348 349	eqeltrd	|- ( ( ph /\ d e. B ) -> if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) e. CC )
351		eqeq1	|- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
352		fveq2	|- ( k = 1 -> ( d ` k ) = ( d ` 1 ) )
353		fvoveq1	|- ( k = 1 -> ( d ` ( k - 1 ) ) = ( d ` ( 1 - 1 ) ) )
354	352 353	oveq12d	|- ( k = 1 -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) )
355	351 354	ifbieq2d	|- ( k = 1 -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) )
356	355	fsum1	|- ( ( 1 e. ZZ /\ if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) e. CC ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) )
357	346 350 356	syl2anc	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) )
358	357 348	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
359	358	adantr	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
360		fveq2	|- ( 1 = K -> ( d ` 1 ) = ( d ` K ) )
361	360	adantl	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( d ` 1 ) = ( d ` K ) )
362	345 359 361	3eqtrd	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
363	2	3ad2ant1	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. NN )
364		nnuz	|- NN = ( ZZ>= ` 1 )
365	364	a1i	|- ( ( ph /\ d e. B /\ 1 < K ) -> NN = ( ZZ>= ` 1 ) )
366	363 365	eleqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. ( ZZ>= ` 1 ) )
367	339	3adantl3	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. CC )
368		iftrue	|- ( k = 1 -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
369	366 367 368	fsum1p	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) ) )
370		1red	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 e. RR )
371		elfzle1	|- ( k e. ( ( 1 + 1 ) ... K ) -> ( 1 + 1 ) <_ k )
372	371	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> ( 1 + 1 ) <_ k )
373		1zzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 e. ZZ )
374		elfzelz	|- ( k e. ( ( 1 + 1 ) ... K ) -> k e. ZZ )
375	374	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> k e. ZZ )
376	373 375	zltp1led	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
377	372 376	mpbird	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 < k )
378	370 377	ltned	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 =/= k )
379	378	necomd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> k =/= 1 )
380	379	neneqd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> -. k = 1 )
381	380	iffalsed	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
382	381	sumeq2dv	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( ( 1 + 1 ) ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
383	382	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) ) = ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
384	255	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. CC )
385		1cnd	|- ( ( ph /\ d e. B /\ 1 < K ) -> 1 e. CC )
386	384 385	npcand	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( K - 1 ) + 1 ) = K )
387	386	eqcomd	|- ( ( ph /\ d e. B /\ 1 < K ) -> K = ( ( K - 1 ) + 1 ) )
388	387	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( 1 + 1 ) ... K ) = ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) )
389	388	sumeq1d	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) )
390	389	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
391		elfzelz	|- ( k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) -> k e. ZZ )
392	391	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k e. ZZ )
393	392	zcnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k e. CC )
394		1cnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. CC )
395	393 394	npcand	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( k - 1 ) + 1 ) = k )
396	395	eqcomd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k = ( ( k - 1 ) + 1 ) )
397	396	fveq2d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` k ) = ( d ` ( ( k - 1 ) + 1 ) ) )
398	397	oveq1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) )
399	398	sumeq2dv	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) )
400	399	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) ) )
401	58	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> 1 e. ZZ )
402	61	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. ZZ )
403	402 401	zsubcld	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( K - 1 ) e. ZZ )
404	56	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
405	404	adantr	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
406		1zzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. ZZ )
407	402	adantr	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. ZZ )
408		elfznn	|- ( s e. ( 1 ... ( K - 1 ) ) -> s e. NN )
409	408	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. NN )
410	409	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ZZ )
411	410	peano2zd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ZZ )
412		1red	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. RR )
413	409	nnred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. RR )
414	411	zred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. RR )
415	409	nnge1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ s )
416	413	lep1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( s + 1 ) )
417	412 413 414 415 416	letrd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ ( s + 1 ) )
418		elfzle2	|- ( s e. ( 1 ... ( K - 1 ) ) -> s <_ ( K - 1 ) )
419	418	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( K - 1 ) )
420	407	zred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. RR )
421		leaddsub	|- ( ( s e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
422	413 412 420 421	syl3anc	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
423	419 422	mpbird	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) <_ K )
424	406 407 411 417 423	elfzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ( 1 ... K ) )
425	405 424	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) )
426		elfznn	|- ( ( d ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( s + 1 ) ) e. NN )
427	425 426	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. NN )
428	427	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. ZZ )
429	420 412	resubcld	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
430	420	lem1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) <_ K )
431	413 429 420 419 430	letrd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ K )
432	406 407 410 415 431	elfzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ( 1 ... K ) )
433	405	ffvelcdmda	|- ( ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) /\ s e. ( 1 ... K ) ) -> ( d ` s ) e. ( 1 ... ( N + K ) ) )
434	432 433	mpdan	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. ( 1 ... ( N + K ) ) )
435		elfznn	|- ( ( d ` s ) e. ( 1 ... ( N + K ) ) -> ( d ` s ) e. NN )
436	434 435	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. NN )
437	436	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. ZZ )
438	428 437	zsubcld	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) e. ZZ )
439	438	zcnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) e. CC )
440		fvoveq1	|- ( s = ( k - 1 ) -> ( d ` ( s + 1 ) ) = ( d ` ( ( k - 1 ) + 1 ) ) )
441		fveq2	|- ( s = ( k - 1 ) -> ( d ` s ) = ( d ` ( k - 1 ) ) )
442	440 441	oveq12d	|- ( s = ( k - 1 ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) = ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) )
443	401 401 403 439 442	fsumshft	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) = sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) )
444	443	eqcomd	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) = sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) )
445	444	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) ) = ( ( d ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) ) )
446		fveq2	|- ( o = s -> ( d ` o ) = ( d ` s ) )
447		fveq2	|- ( o = ( s + 1 ) -> ( d ` o ) = ( d ` ( s + 1 ) ) )
448		fveq2	|- ( o = 1 -> ( d ` o ) = ( d ` 1 ) )
449		fveq2	|- ( o = ( ( K - 1 ) + 1 ) -> ( d ` o ) = ( d ` ( ( K - 1 ) + 1 ) ) )
450	386 366	eqeltrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( K - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
451	56	adantr	|- ( ( ( ph /\ d e. B ) /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
452	451	3impa	|- ( ( ph /\ d e. B /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
453	452	ffvelcdmda	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... K ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) )
454	453	ex	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... K ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) )
455	386	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( 1 ... ( ( K - 1 ) + 1 ) ) = ( 1 ... K ) )
456	455	eleq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... ( ( K - 1 ) + 1 ) ) <-> o e. ( 1 ... K ) ) )
457	456	imbi1d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( o e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) <-> ( o e. ( 1 ... K ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) ) )
458	454 457	mpbird	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) )
459	458	imp	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) )
460		elfznn	|- ( ( d ` o ) e. ( 1 ... ( N + K ) ) -> ( d ` o ) e. NN )
461	459 460	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. NN )
462	461	nncnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. CC )
463	446 447 448 449 403 450 462	telfsum2	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) = ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) )
464	463	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) ) = ( ( d ` 1 ) + ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) ) )
465	386	fveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` ( ( K - 1 ) + 1 ) ) = ( d ` K ) )
466	465	oveq1d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) = ( ( d ` K ) - ( d ` 1 ) ) )
467	466	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) )
468	349	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` 1 ) e. CC )
469	267	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` K ) e. CC )
470	468 469	pncan3d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) = ( d ` K ) )
471		eqidd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` K ) = ( d ` K ) )
472	470 471	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) = ( d ` K ) )
473	467 472	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` K ) )
474	464 473	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) ) = ( d ` K ) )
475	445 474	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
476	400 475	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
477	390 476	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
478	383 477	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) ) = ( d ` K ) )
479	369 478	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
480	479	3expa	|- ( ( ( ph /\ d e. B ) /\ 1 < K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
481	137	adantr	|- ( ( ph /\ d e. B ) -> 1 e. RR )
482	64	adantr	|- ( ( ph /\ d e. B ) -> K e. RR )
483	481 482	leloed	|- ( ( ph /\ d e. B ) -> ( 1 <_ K <-> ( 1 < K \/ 1 = K ) ) )
484	63 483	mpbid	|- ( ( ph /\ d e. B ) -> ( 1 < K \/ 1 = K ) )
485	484	orcomd	|- ( ( ph /\ d e. B ) -> ( 1 = K \/ 1 < K ) )
486	362 480 485	mpjaodan	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
487		fsumconst	|- ( ( ( 1 ... K ) e. Fin /\ 1 e. CC ) -> sum_ k e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
488	295 256 487	syl2anc	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
489	59	adantr	|- ( ( ph /\ d e. B ) -> K e. NN0 )
490		hashfz1	|- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
491	489 490	syl	|- ( ( ph /\ d e. B ) -> ( # ` ( 1 ... K ) ) = K )
492	491	oveq1d	|- ( ( ph /\ d e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = ( K x. 1 ) )
493	255	mulridd	|- ( ( ph /\ d e. B ) -> ( K x. 1 ) = K )
494	492 493	eqtrd	|- ( ( ph /\ d e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = K )
495	488 494	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) 1 = K )
496	486 495	oveq12d	|- ( ( ph /\ d e. B ) -> ( sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - sum_ k e. ( 1 ... K ) 1 ) = ( ( d ` K ) - K ) )
497	341 496	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) = ( ( d ` K ) - K ) )
498	294 497	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( ( d ` K ) - K ) )
499	267 255	subcld	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) e. CC )
500	499	addridd	|- ( ( ph /\ d e. B ) -> ( ( ( d ` K ) - K ) + 0 ) = ( ( d ` K ) - K ) )
501	500	eqcomd	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) = ( ( ( d ` K ) - K ) + 0 ) )
502		0cnd	|- ( ( ph /\ d e. B ) -> 0 e. CC )
503	499 502	addcomd	|- ( ( ph /\ d e. B ) -> ( ( ( d ` K ) - K ) + 0 ) = ( 0 + ( ( d ` K ) - K ) ) )
504	501 503	eqtrd	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) = ( 0 + ( ( d ` K ) - K ) ) )
505	498 504	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( 0 + ( ( d ` K ) - K ) ) )
506	502 255 267	subsub2d	|- ( ( ph /\ d e. B ) -> ( 0 - ( K - ( d ` K ) ) ) = ( 0 + ( ( d ` K ) - K ) ) )
507	506	eqcomd	|- ( ( ph /\ d e. B ) -> ( 0 + ( ( d ` K ) - K ) ) = ( 0 - ( K - ( d ` K ) ) ) )
508	505 507	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( 0 - ( K - ( d ` K ) ) ) )
509	264	subidd	|- ( ( ph /\ d e. B ) -> ( N - N ) = 0 )
510	509	eqcomd	|- ( ( ph /\ d e. B ) -> 0 = ( N - N ) )
511	510	oveq1d	|- ( ( ph /\ d e. B ) -> ( 0 - ( K - ( d ` K ) ) ) = ( ( N - N ) - ( K - ( d ` K ) ) ) )
512	508 511	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( ( N - N ) - ( K - ( d ` K ) ) ) )
513	255 267	subcld	|- ( ( ph /\ d e. B ) -> ( K - ( d ` K ) ) e. CC )
514	264 264 513	subsub4d	|- ( ( ph /\ d e. B ) -> ( ( N - N ) - ( K - ( d ` K ) ) ) = ( N - ( N + ( K - ( d ` K ) ) ) ) )
515	512 514	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( N - ( N + ( K - ( d ` K ) ) ) ) )
516	264 255 267	addsubassd	|- ( ( ph /\ d e. B ) -> ( ( N + K ) - ( d ` K ) ) = ( N + ( K - ( d ` K ) ) ) )
517	516	eqcomd	|- ( ( ph /\ d e. B ) -> ( N + ( K - ( d ` K ) ) ) = ( ( N + K ) - ( d ` K ) ) )
518	517	oveq2d	|- ( ( ph /\ d e. B ) -> ( N - ( N + ( K - ( d ` K ) ) ) ) = ( N - ( ( N + K ) - ( d ` K ) ) ) )
519	515 518	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = ( N - ( ( N + K ) - ( d ` K ) ) ) )
520	282 519	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = ( N - ( ( N + K ) - ( d ` K ) ) ) )
521	264 268 520	mvrrsubd	|- ( ( ph /\ d e. B ) -> ( sum_ k e. ( 1 ... K ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) + ( ( N + K ) - ( d ` K ) ) ) = N )
522	262 521	eqtrd	|- ( ( ph /\ d e. B ) -> ( sum_ k e. ( 1 ... ( ( K + 1 ) - 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( ( K + 1 ) = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` ( K + 1 ) ) - ( d ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) = N )
523	254 522	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... ( K + 1 ) ) if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = N )
524	231 523	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( i = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` i ) - ( d ` ( i - 1 ) ) ) - 1 ) ) ) = N )
525	219 524	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N )
526	201 525	jca	|- ( ( ph /\ d e. B ) -> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) )
527		ovex	|- ( 1 ... ( K + 1 ) ) e. _V
528	527	mptex	|- ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. _V
529		feq1	|- ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) -> ( g : ( 1 ... ( K + 1 ) ) --> NN0 <-> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 ) )
530		simpl	|- ( ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
531	530	fveq1d	|- ( ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( g ` i ) = ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) )
532	531	sumeq2dv	|- ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) )
533	532	eqeq1d	|- ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) -> ( sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N <-> sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) )
534	529 533	anbi12d	|- ( g = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) -> ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) <-> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) ) )
535	528 534	elab	|- ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) )
536	535	a1i	|- ( ( ph /\ d e. B ) -> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) ) )
537	526 536	mpbird	|- ( ( ph /\ d e. B ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
538	5	a1i	|- ( ( ph /\ d e. B ) -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
539	538	eqcomd	|- ( ( ph /\ d e. B ) -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } = A )
540	537 539	eleqtrd	|- ( ( ph /\ d e. B ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) e. A )
541	295	mptexd	|- ( ( ph /\ d e. B ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) e. _V )
542	34 40 540 541	fvmptd	|- ( ( ph /\ d e. B ) -> ( F ` ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) )
543		eqidd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) )
544		simpr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> k = l )
545	544	eqeq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k = ( K + 1 ) <-> l = ( K + 1 ) ) )
546	544	eqeq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k = 1 <-> l = 1 ) )
547	544	fveq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( d ` k ) = ( d ` l ) )
548	544	oveq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k - 1 ) = ( l - 1 ) )
549	548	fveq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( d ` ( k - 1 ) ) = ( d ` ( l - 1 ) ) )
550	547 549	oveq12d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` l ) - ( d ` ( l - 1 ) ) ) )
551	550	oveq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) = ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) )
552	546 551	ifbieq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) = if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) )
553	545 552	ifbieq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) = if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
554		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 e. ZZ )
555	60	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ZZ )
556	555	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. ZZ )
557	556	peano2zd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. ZZ )
558		elfzelz	|- ( l e. ( 1 ... j ) -> l e. ZZ )
559	558	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ZZ )
560		elfzle1	|- ( l e. ( 1 ... j ) -> 1 <_ l )
561	560	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 <_ l )
562	559	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. RR )
563		simp3	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ( 1 ... K ) )
564		elfznn	|- ( j e. ( 1 ... K ) -> j e. NN )
565	563 564	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. NN )
566	565	nnred	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. RR )
567	566	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. RR )
568	557	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. RR )
569		elfzle2	|- ( l e. ( 1 ... j ) -> l <_ j )
570	569	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ j )
571	64	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. RR )
572		1red	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. RR )
573	571 572	readdcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
574		elfzle2	|- ( j e. ( 1 ... K ) -> j <_ K )
575	563 574	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j <_ K )
576	571	lep1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K <_ ( K + 1 ) )
577	566 571 573 575 576	letrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j <_ ( K + 1 ) )
578	577	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j <_ ( K + 1 ) )
579	562 567 568 570 578	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ ( K + 1 ) )
580	554 557 559 561 579	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ( 1 ... ( K + 1 ) ) )
581		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( N + K ) - ( d ` K ) ) e. _V )
582		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( d ` 1 ) - 1 ) e. _V )
583		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. _V )
584	582 583	ifcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) e. _V )
585	581 584	ifcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) e. _V )
586	543 553 580 585	fvmptd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) = if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
587	586	sumeq2dv	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) = sum_ l e. ( 1 ... j ) if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
588	587	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) = ( j + sum_ l e. ( 1 ... j ) if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) )
589		elfznn	|- ( l e. ( 1 ... j ) -> l e. NN )
590	589	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. NN )
591	590	nnred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. RR )
592	571	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. RR )
593		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 e. RR )
594	592 593	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. RR )
595	565	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. NN )
596	595	nnred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. RR )
597	575	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j <_ K )
598	591 596 592 570 597	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ K )
599	592	ltp1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K < ( K + 1 ) )
600	591 592 594 598 599	lelttrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l < ( K + 1 ) )
601	591 600	ltned	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l =/= ( K + 1 ) )
602	601	neneqd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> -. l = ( K + 1 ) )
603	602	iffalsed	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) )
604	603	sumeq2dv	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = sum_ l e. ( 1 ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) )
605	604	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) = ( j + sum_ l e. ( 1 ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
606	565	nnge1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 <_ j )
607	57	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ZZ )
608	565	nnzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ZZ )
609		eluz	|- ( ( 1 e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` 1 ) <-> 1 <_ j ) )
610	607 608 609	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j e. ( ZZ>= ` 1 ) <-> 1 <_ j ) )
611	606 610	mpbird	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ( ZZ>= ` 1 ) )
612		eleq1	|- ( ( ( d ` 1 ) - 1 ) = if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) -> ( ( ( d ` 1 ) - 1 ) e. CC <-> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) e. CC ) )
613		eleq1	|- ( ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) = if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) -> ( ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. CC <-> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) e. CC ) )
614	56	3adant3	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
615		simp1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ph )
616	615 62	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 <_ K )
617	615 60	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ZZ )
618		eluz	|- ( ( 1 e. ZZ /\ K e. ZZ ) -> ( K e. ( ZZ>= ` 1 ) <-> 1 <_ K ) )
619	607 617 618	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( K e. ( ZZ>= ` 1 ) <-> 1 <_ K ) )
620	616 619	mpbird	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ( ZZ>= ` 1 ) )
621		eluzfz1	|- ( K e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... K ) )
622	620 621	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ( 1 ... K ) )
623	614 622	ffvelcdmd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. ( 1 ... ( N + K ) ) )
624	623 90	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. NN )
625	624	nnzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. ZZ )
626	625 607	zsubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) - 1 ) e. ZZ )
627	626	zcnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) - 1 ) e. CC )
628	627	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( d ` 1 ) - 1 ) e. CC )
629	628	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ l = 1 ) -> ( ( d ` 1 ) - 1 ) e. CC )
630	614	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
631	617	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. ZZ )
632	590	nnzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ZZ )
633	590	nnge1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 <_ l )
634	554 631 632 633 598	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ( 1 ... K ) )
635	630 634	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
636		elfzelz	|- ( ( d ` l ) e. ( 1 ... ( N + K ) ) -> ( d ` l ) e. ZZ )
637	635 636	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( d ` l ) e. ZZ )
638	637	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` l ) e. ZZ )
639	630	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
640		1zzd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 e. ZZ )
641	631	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> K e. ZZ )
642	632	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l e. ZZ )
643	642 640	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. ZZ )
644		neqne	|- ( -. l = 1 -> l =/= 1 )
645	644	adantl	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l =/= 1 )
646	593	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 e. RR )
647	591	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l e. RR )
648	633	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 <_ l )
649	646 647 648	leltned	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( 1 < l <-> l =/= 1 ) )
650	645 649	mpbird	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 < l )
651	640 642	zltlem1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( 1 < l <-> 1 <_ ( l - 1 ) ) )
652	650 651	mpbid	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 <_ ( l - 1 ) )
653	643	zred	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. RR )
654	592	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> K e. RR )
655	647	lem1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) <_ l )
656	598	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l <_ K )
657	653 647 654 655 656	letrd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) <_ K )
658	640 641 643 652 657	elfzd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. ( 1 ... K ) )
659	639 658	ffvelcdmd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) )
660		elfzelz	|- ( ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l - 1 ) ) e. ZZ )
661	659 660	syl	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` ( l - 1 ) ) e. ZZ )
662	638 661	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. ZZ )
663	662 640	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. ZZ )
664	663	zcnd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. CC )
665	612 613 629 664	ifbothda	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) e. CC )
666		iftrue	|- ( l = 1 -> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = ( ( d ` 1 ) - 1 ) )
667	611 665 666	fsum1p	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
668	667	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) )
669	615 137	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. RR )
670	669	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. RR )
671	670 670	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( 1 + 1 ) e. RR )
672		elfzelz	|- ( l e. ( ( 1 + 1 ) ... j ) -> l e. ZZ )
673	672	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. ZZ )
674	673	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. RR )
675	670	ltp1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 < ( 1 + 1 ) )
676		elfzle1	|- ( l e. ( ( 1 + 1 ) ... j ) -> ( 1 + 1 ) <_ l )
677	676	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( 1 + 1 ) <_ l )
678	670 671 674 675 677	ltletrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 < l )
679	670 678	ltned	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 =/= l )
680	679	necomd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l =/= 1 )
681	680	neneqd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> -. l = 1 )
682	681	iffalsed	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) )
683	682	sumeq2dv	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) )
684	683	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) )
685	684	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) = ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) )
686		fzfid	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + 1 ) ... j ) e. Fin )
687	614	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
688		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. ZZ )
689	617	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> K e. ZZ )
690	670 671 675	ltled	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ ( 1 + 1 ) )
691	670 671 674 690 677	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ l )
692	566	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> j e. RR )
693	571	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> K e. RR )
694		elfzle2	|- ( l e. ( ( 1 + 1 ) ... j ) -> l <_ j )
695	694	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l <_ j )
696	575	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> j <_ K )
697	674 692 693 695 696	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l <_ K )
698	688 689 673 691 697	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. ( 1 ... K ) )
699	687 698	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
700	699 636	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. ZZ )
701	700	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. CC )
702	673 688	zsubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. ZZ )
703		leaddsub	|- ( ( 1 e. RR /\ 1 e. RR /\ l e. RR ) -> ( ( 1 + 1 ) <_ l <-> 1 <_ ( l - 1 ) ) )
704	670 670 674 703	syl3anc	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( 1 + 1 ) <_ l <-> 1 <_ ( l - 1 ) ) )
705	677 704	mpbid	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ ( l - 1 ) )
706	674 670	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. RR )
707	674	lem1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) <_ l )
708	706 674 693 707 697	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) <_ K )
709	688 689 702 705 708	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. ( 1 ... K ) )
710	687 709	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) )
711	660	zcnd	|- ( ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l - 1 ) ) e. CC )
712	710 711	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( l - 1 ) ) e. CC )
713	701 712	subcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. CC )
714		1cnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. CC )
715	686 713 714	fsumsub	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) = ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) )
716	715	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) ) )
717	716	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) ) ) )
718		1cnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. CC )
719		fsumconst	|- ( ( ( ( 1 + 1 ) ... j ) e. Fin /\ 1 e. CC ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) )
720	686 718 719	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) )
721		hashfzp1	|- ( j e. ( ZZ>= ` 1 ) -> ( # ` ( ( 1 + 1 ) ... j ) ) = ( j - 1 ) )
722	611 721	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( # ` ( ( 1 + 1 ) ... j ) ) = ( j - 1 ) )
723	722	oveq1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) = ( ( j - 1 ) x. 1 ) )
724	565	nncnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. CC )
725	724 718	subcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. CC )
726	725	mulridd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) x. 1 ) = ( j - 1 ) )
727	723 726	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) = ( j - 1 ) )
728	720 727	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( j - 1 ) )
729	728	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) = ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) )
730	729	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) ) = ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) )
731	730	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) ) ) = ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) ) )
732	686 713	fsumcl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. CC )
733	627 732 725	addsubassd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) = ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) )
734	733	eqcomd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) = ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) )
735	734	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) ) = ( j + ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) ) )
736	627 732	addcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) e. CC )
737	724 736 725	addsubassd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) - ( j - 1 ) ) = ( j + ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) ) )
738	737	eqcomd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) ) = ( ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) - ( j - 1 ) ) )
739	724 736 725	addsubd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) - ( j - 1 ) ) = ( ( j - ( j - 1 ) ) + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) )
740	724 718	nncand	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - ( j - 1 ) ) = 1 )
741		1zzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ZZ )
742	608 607	zsubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. ZZ )
743	614	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
744		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 e. ZZ )
745	617	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> K e. ZZ )
746		elfzelz	|- ( l e. ( 1 ... ( j - 1 ) ) -> l e. ZZ )
747	746	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ZZ )
748	747	peano2zd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ZZ )
749		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 e. RR )
750	747	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. RR )
751	750 749	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. RR )
752		elfzle1	|- ( l e. ( 1 ... ( j - 1 ) ) -> 1 <_ l )
753	752	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 <_ l )
754	750	lep1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( l + 1 ) )
755	749 750 751 753 754	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 <_ ( l + 1 ) )
756	566	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j e. RR )
757	756 749	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) e. RR )
758	571	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> K e. RR )
759	758 749	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( K - 1 ) e. RR )
760		elfzle2	|- ( l e. ( 1 ... ( j - 1 ) ) -> l <_ ( j - 1 ) )
761	760	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( j - 1 ) )
762	575	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j <_ K )
763	756 758 749 762	lesub1dd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) <_ ( K - 1 ) )
764	750 757 759 761 763	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( K - 1 ) )
765		leaddsub	|- ( ( l e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( l + 1 ) <_ K <-> l <_ ( K - 1 ) ) )
766	750 749 758 765	syl3anc	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( l + 1 ) <_ K <-> l <_ ( K - 1 ) ) )
767	764 766	mpbird	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) <_ K )
768	744 745 748 755 767	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ( 1 ... K ) )
769	743 768	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` ( l + 1 ) ) e. ( 1 ... ( N + K ) ) )
770		elfzelz	|- ( ( d ` ( l + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l + 1 ) ) e. ZZ )
771	769 770	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` ( l + 1 ) ) e. ZZ )
772	566 669	resubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. RR )
773	566	lem1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) <_ j )
774	772 566 571 773 575	letrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) <_ K )
775	774	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) <_ K )
776	750 757 758 761 775	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ K )
777	744 745 747 753 776	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( 1 ... K ) )
778	743 777	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
779	778 636	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` l ) e. ZZ )
780	771 779	zsubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) e. ZZ )
781	780	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) e. CC )
782		fvoveq1	|- ( l = ( w - 1 ) -> ( d ` ( l + 1 ) ) = ( d ` ( ( w - 1 ) + 1 ) ) )
783		fveq2	|- ( l = ( w - 1 ) -> ( d ` l ) = ( d ` ( w - 1 ) ) )
784	782 783	oveq12d	|- ( l = ( w - 1 ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) )
785	741 741 742 781 784	fsumshft	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = sum_ w e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) )
786		oveq1	|- ( w = l -> ( w - 1 ) = ( l - 1 ) )
787	786	fvoveq1d	|- ( w = l -> ( d ` ( ( w - 1 ) + 1 ) ) = ( d ` ( ( l - 1 ) + 1 ) ) )
788	786	fveq2d	|- ( w = l -> ( d ` ( w - 1 ) ) = ( d ` ( l - 1 ) ) )
789	787 788	oveq12d	|- ( w = l -> ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) = ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) )
790		nfcv	|- F/_ l ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) )
791		nfcv	|- F/_ w ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) )
792	789 790 791	cbvsum	|- sum_ w e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) = sum_ l e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) )
793	792	a1i	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ w e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) = sum_ l e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) )
794	785 793	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = sum_ l e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) )
795	724 718	npcand	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) = j )
796	795	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... j ) )
797	796	sumeq1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) = sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) )
798	674	recnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. CC )
799	798 714	npcand	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( l - 1 ) + 1 ) = l )
800	799	fveq2d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( ( l - 1 ) + 1 ) ) = ( d ` l ) )
801	800	oveq1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) = ( ( d ` l ) - ( d ` ( l - 1 ) ) ) )
802	801	sumeq2dv	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) = sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) )
803	797 802	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) = sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) )
804	794 803	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) )
805	804	eqcomd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) = sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) )
806	805	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) = ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) ) )
807	740 806	oveq12d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - ( j - 1 ) ) + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) = ( 1 + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) ) ) )
808		fveq2	|- ( r = l -> ( d ` r ) = ( d ` l ) )
809		fveq2	|- ( r = ( l + 1 ) -> ( d ` r ) = ( d ` ( l + 1 ) ) )
810		fveq2	|- ( r = 1 -> ( d ` r ) = ( d ` 1 ) )
811		fveq2	|- ( r = ( ( j - 1 ) + 1 ) -> ( d ` r ) = ( d ` ( ( j - 1 ) + 1 ) ) )
812	795 611	eqeltrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
813	614	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
814		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 e. ZZ )
815	617	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> K e. ZZ )
816		elfzelz	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> r e. ZZ )
817	816	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. ZZ )
818		elfzle1	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> 1 <_ r )
819	818	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 <_ r )
820	817	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. RR )
821	566	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> j e. RR )
822		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 e. RR )
823	821 822	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( j - 1 ) e. RR )
824	823 822	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( ( j - 1 ) + 1 ) e. RR )
825	571	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> K e. RR )
826		elfzle2	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> r <_ ( ( j - 1 ) + 1 ) )
827	826	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r <_ ( ( j - 1 ) + 1 ) )
828	795 575	eqbrtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) <_ K )
829	828	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( ( j - 1 ) + 1 ) <_ K )
830	820 824 825 827 829	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r <_ K )
831	814 815 817 819 830	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. ( 1 ... K ) )
832	813 831	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. ( 1 ... ( N + K ) ) )
833		elfzelz	|- ( ( d ` r ) e. ( 1 ... ( N + K ) ) -> ( d ` r ) e. ZZ )
834	832 833	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. ZZ )
835	834	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. CC )
836	808 809 810 811 742 812 835	telfsum2	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) )
837	836	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) ) = ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) )
838	837	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) ) ) = ( 1 + ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) ) )
839	795	fveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) = ( d ` j ) )
840	614 563	ffvelcdmd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` j ) e. ( 1 ... ( N + K ) ) )
841		elfzelz	|- ( ( d ` j ) e. ( 1 ... ( N + K ) ) -> ( d ` j ) e. ZZ )
842	840 841	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` j ) e. ZZ )
843	839 842	eqeltrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) e. ZZ )
844	843	zcnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) e. CC )
845	624	nnred	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. RR )
846	845	recnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. CC )
847	844 846	subcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) e. CC )
848	718 627 847	addassd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + ( ( d ` 1 ) - 1 ) ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( 1 + ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) ) )
849	848	eqcomd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) ) = ( ( 1 + ( ( d ` 1 ) - 1 ) ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) )
850	718 846	pncan3d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( d ` 1 ) - 1 ) ) = ( d ` 1 ) )
851	850	oveq1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + ( ( d ` 1 ) - 1 ) ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( ( d ` 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) )
852	846 844	pncan3d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` ( ( j - 1 ) + 1 ) ) )
853	852 839	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` j ) )
854	851 853	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + ( ( d ` 1 ) - 1 ) ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` j ) )
855	849 854	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) ) = ( d ` j ) )
856	838 855	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( 1 ... ( j - 1 ) ) ( ( d ` ( l + 1 ) ) - ( d ` l ) ) ) ) = ( d ` j ) )
857	807 856	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - ( j - 1 ) ) + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) = ( d ` j ) )
858	739 857	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) ) - ( j - 1 ) ) = ( d ` j ) )
859	738 858	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) ) - ( j - 1 ) ) ) = ( d ` j ) )
860	735 859	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - ( j - 1 ) ) ) ) = ( d ` j ) )
861	731 860	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + ( sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - sum_ l e. ( ( 1 + 1 ) ... j ) 1 ) ) ) = ( d ` j ) )
862	717 861	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = ( d ` j ) )
863	685 862	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + ( ( ( d ` 1 ) - 1 ) + sum_ l e. ( ( 1 + 1 ) ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) = ( d ` j ) )
864	668 863	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) = ( d ` j ) )
865	605 864	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) if ( l = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) ) ) = ( d ` j ) )
866	588 865	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) = ( d ` j ) )
867	866	3expa	|- ( ( ( ph /\ d e. B ) /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) = ( d ` j ) )
868	867	mpteq2dva	|- ( ( ph /\ d e. B ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( d ` j ) ) )
869		nfcv	|- F/_ q ( d ` j )
870		nfcv	|- F/_ j ( d ` q )
871		fveq2	|- ( j = q -> ( d ` j ) = ( d ` q ) )
872	869 870 871	cbvmpt	|- ( j e. ( 1 ... K ) |-> ( d ` j ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) )
873	872	a1i	|- ( ( ph /\ d e. B ) -> ( j e. ( 1 ... K ) |-> ( d ` j ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
874	868 873	eqtrd	|- ( ( ph /\ d e. B ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ` l ) ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
875	542 874	eqtrd	|- ( ( ph /\ d e. B ) -> ( F ` ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( d ` K ) ) , if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
876	33 875	eqtrd	|- ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
877	56	ffnd	|- ( ( ph /\ d e. B ) -> d Fn ( 1 ... K ) )
878		dffn5	|- ( d Fn ( 1 ... K ) <-> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
879	878	biimpi	|- ( d Fn ( 1 ... K ) -> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
880	877 879	syl	|- ( ( ph /\ d e. B ) -> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
881	880	eqcomd	|- ( ( ph /\ d e. B ) -> ( q e. ( 1 ... K ) |-> ( d ` q ) ) = d )
882	876 881	eqtrd	|- ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = d )
883	882	ralrimiva	|- ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )