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		elfzelz	|- ( k e. ( 1 ... K ) -> k e. ZZ )
264	263	adantl	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k e. ZZ )
265	264	zred	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k e. RR )
266	64	ad2antrr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> K e. RR )
267		1red	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> 1 e. RR )
268	266 267	readdcld	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
269		elfzle2	|- ( k e. ( 1 ... K ) -> k <_ K )
270	269	adantl	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k <_ K )
271	266	ltp1d	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> K < ( K + 1 ) )
272	265 266 268 270 271	lelttrd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k < ( K + 1 ) )
273	265 272	ltned	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> k =/= ( K + 1 ) )
274	273	neneqd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> -. k = ( K + 1 ) )
275	274	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 ) ) )
276	275	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 ) ) )
277		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 ) ) )
278		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 ) ) )
279		simpr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> k = 1 )
280	279	iftrued	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
281	280	eqcomd	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( d ` 1 ) = if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) )
282	281	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 ) )
283		simpr	|- ( ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> -. k = 1 )
284	283	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 ) ) ) )
285	284	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 ) ) ) ) )
286	285	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 ) )
287	277 278 282 286	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 ) )
288	287	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 ) )
289		fzfid	|- ( ( ph /\ d e. B ) -> ( 1 ... K ) e. Fin )
290		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 ) )
291		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 ) )
292	56	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
293	88	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> 1 e. ( 1 ... K ) )
294	292 293	ffvelcdmd	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` 1 ) e. ( 1 ... ( N + K ) ) )
295	90	nnzd	|- ( ( d ` 1 ) e. ( 1 ... ( N + K ) ) -> ( d ` 1 ) e. ZZ )
296	294 295	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` 1 ) e. ZZ )
297	296	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( d ` 1 ) e. ZZ )
298		simp3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k e. ( 1 ... K ) )
299	292 298	ffvelcdmd	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` k ) e. ( 1 ... ( N + K ) ) )
300	299 126	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( d ` k ) e. ZZ )
301	300	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` k ) e. ZZ )
302	292	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
303		1zzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 e. ZZ )
304	61	3adant3	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> K e. ZZ )
305	304	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> K e. ZZ )
306	264	3impa	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k e. ZZ )
307	306	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k e. ZZ )
308	307 303	zsubcld	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
309		elfzle1	|- ( k e. ( 1 ... K ) -> 1 <_ k )
310	298 309	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> 1 <_ k )
311	310	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 <_ k )
312	135	adantl	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k =/= 1 )
313	311 312	jca	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 <_ k /\ k =/= 1 ) )
314		1red	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 e. RR )
315	307	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k e. RR )
316	314 315	ltlend	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 <_ k /\ k =/= 1 ) ) )
317	313 316	mpbird	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 < k )
318	303 307	zltlem1d	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( 1 < k <-> 1 <_ ( k - 1 ) ) )
319	317 318	mpbid	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
320	308	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
321	305	zred	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> K e. RR )
322	315	lem1d	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ k )
323	298 269	syl	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> k <_ K )
324	323	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> k <_ K )
325	320 315 321 322 324	letrd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
326	303 305 308 319 325	elfzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
327	302 326	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) )
328	327 166	syl	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. NN )
329	328	nnzd	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( d ` ( k - 1 ) ) e. ZZ )
330	301 329	zsubcld	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) e. ZZ )
331	290 291 297 330	ifbothda	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ )
332	331	3expa	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. ZZ )
333	332	zcnd	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. CC )
334	256	adantr	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> 1 e. CC )
335	289 333 334	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 ) )
336		simpr	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> 1 = K )
337	336	oveq2d	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( 1 ... 1 ) = ( 1 ... K ) )
338	337	eqcomd	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( 1 ... K ) = ( 1 ... 1 ) )
339	338	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 ) ) ) ) )
340		1zzd	|- ( ( ph /\ d e. B ) -> 1 e. ZZ )
341	232	a1i	|- ( ( ph /\ d e. B ) -> 1 = 1 )
342	341	iftrued	|- ( ( ph /\ d e. B ) -> if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) = ( d ` 1 ) )
343	91	nncnd	|- ( ( ph /\ d e. B ) -> ( d ` 1 ) e. CC )
344	342 343	eqeltrd	|- ( ( ph /\ d e. B ) -> if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) e. CC )
345		eqeq1	|- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
346		fveq2	|- ( k = 1 -> ( d ` k ) = ( d ` 1 ) )
347		fvoveq1	|- ( k = 1 -> ( d ` ( k - 1 ) ) = ( d ` ( 1 - 1 ) ) )
348	346 347	oveq12d	|- ( k = 1 -> ( ( d ` k ) - ( d ` ( k - 1 ) ) ) = ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) )
349	345 348	ifbieq2d	|- ( k = 1 -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = if ( 1 = 1 , ( d ` 1 ) , ( ( d ` 1 ) - ( d ` ( 1 - 1 ) ) ) ) )
350	349	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 ) ) ) ) )
351	340 344 350	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 ) ) ) ) )
352	351 342	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
353	352	adantr	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> sum_ k e. ( 1 ... 1 ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
354		fveq2	|- ( 1 = K -> ( d ` 1 ) = ( d ` K ) )
355	354	adantl	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> ( d ` 1 ) = ( d ` K ) )
356	339 353 355	3eqtrd	|- ( ( ( ph /\ d e. B ) /\ 1 = K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
357	2	3ad2ant1	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. NN )
358		nnuz	|- NN = ( ZZ>= ` 1 )
359	358	a1i	|- ( ( ph /\ d e. B /\ 1 < K ) -> NN = ( ZZ>= ` 1 ) )
360	357 359	eleqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. ( ZZ>= ` 1 ) )
361	333	3adantl3	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) e. CC )
362		iftrue	|- ( k = 1 -> if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` 1 ) )
363	360 361 362	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 ) ) ) ) ) )
364		1red	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 e. RR )
365		elfzle1	|- ( k e. ( ( 1 + 1 ) ... K ) -> ( 1 + 1 ) <_ k )
366	365	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> ( 1 + 1 ) <_ k )
367		1zzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 e. ZZ )
368		elfzelz	|- ( k e. ( ( 1 + 1 ) ... K ) -> k e. ZZ )
369	368	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> k e. ZZ )
370	367 369	zltp1led	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
371	366 370	mpbird	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 < k )
372	364 371	ltned	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> 1 =/= k )
373	372	necomd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> k =/= 1 )
374	373	neneqd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... K ) ) -> -. k = 1 )
375	374	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 ) ) ) )
376	375	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 ) ) ) )
377	376	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 ) ) ) ) )
378	255	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. CC )
379		1cnd	|- ( ( ph /\ d e. B /\ 1 < K ) -> 1 e. CC )
380	378 379	npcand	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( K - 1 ) + 1 ) = K )
381	380	eqcomd	|- ( ( ph /\ d e. B /\ 1 < K ) -> K = ( ( K - 1 ) + 1 ) )
382	381	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( 1 + 1 ) ... K ) = ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) )
383	382	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 ) ) ) )
384	383	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 ) ) ) ) )
385		elfzelz	|- ( k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) -> k e. ZZ )
386	385	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k e. ZZ )
387	386	zcnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k e. CC )
388		1cnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. CC )
389	387 388	npcand	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( k - 1 ) + 1 ) = k )
390	389	eqcomd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> k = ( ( k - 1 ) + 1 ) )
391	390	fveq2d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` k ) = ( d ` ( ( k - 1 ) + 1 ) ) )
392	391	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 ) ) ) )
393	392	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 ) ) ) )
394	393	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 ) ) ) ) )
395	58	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> 1 e. ZZ )
396	61	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> K e. ZZ )
397	396 395	zsubcld	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( K - 1 ) e. ZZ )
398	56	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
399	398	adantr	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
400		1zzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. ZZ )
401	396	adantr	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. ZZ )
402		elfznn	|- ( s e. ( 1 ... ( K - 1 ) ) -> s e. NN )
403	402	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. NN )
404	403	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ZZ )
405	404	peano2zd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ZZ )
406		1red	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. RR )
407	403	nnred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. RR )
408	405	zred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. RR )
409	403	nnge1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ s )
410	407	lep1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( s + 1 ) )
411	406 407 408 409 410	letrd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ ( s + 1 ) )
412		elfzle2	|- ( s e. ( 1 ... ( K - 1 ) ) -> s <_ ( K - 1 ) )
413	412	adantl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( K - 1 ) )
414	401	zred	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. RR )
415		leaddsub	|- ( ( s e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
416	407 406 414 415	syl3anc	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
417	413 416	mpbird	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) <_ K )
418	400 401 405 411 417	elfzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ( 1 ... K ) )
419	399 418	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) )
420		elfznn	|- ( ( d ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( s + 1 ) ) e. NN )
421	419 420	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. NN )
422	421	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` ( s + 1 ) ) e. ZZ )
423	414 406	resubcld	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
424	414	lem1d	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) <_ K )
425	407 423 414 413 424	letrd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ K )
426	400 401 404 409 425	elfzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ( 1 ... K ) )
427	399	ffvelcdmda	|- ( ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) /\ s e. ( 1 ... K ) ) -> ( d ` s ) e. ( 1 ... ( N + K ) ) )
428	426 427	mpdan	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. ( 1 ... ( N + K ) ) )
429		elfznn	|- ( ( d ` s ) e. ( 1 ... ( N + K ) ) -> ( d ` s ) e. NN )
430	428 429	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. NN )
431	430	nnzd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( d ` s ) e. ZZ )
432	422 431	zsubcld	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) e. ZZ )
433	432	zcnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) e. CC )
434		fvoveq1	|- ( s = ( k - 1 ) -> ( d ` ( s + 1 ) ) = ( d ` ( ( k - 1 ) + 1 ) ) )
435		fveq2	|- ( s = ( k - 1 ) -> ( d ` s ) = ( d ` ( k - 1 ) ) )
436	434 435	oveq12d	|- ( s = ( k - 1 ) -> ( ( d ` ( s + 1 ) ) - ( d ` s ) ) = ( ( d ` ( ( k - 1 ) + 1 ) ) - ( d ` ( k - 1 ) ) ) )
437	395 395 397 433 436	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 ) ) ) )
438	437	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 ) ) )
439	438	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 ) ) ) )
440		fveq2	|- ( o = s -> ( d ` o ) = ( d ` s ) )
441		fveq2	|- ( o = ( s + 1 ) -> ( d ` o ) = ( d ` ( s + 1 ) ) )
442		fveq2	|- ( o = 1 -> ( d ` o ) = ( d ` 1 ) )
443		fveq2	|- ( o = ( ( K - 1 ) + 1 ) -> ( d ` o ) = ( d ` ( ( K - 1 ) + 1 ) ) )
444	380 360	eqeltrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( K - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
445	56	adantr	|- ( ( ( ph /\ d e. B ) /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
446	445	3impa	|- ( ( ph /\ d e. B /\ 1 < K ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
447	446	ffvelcdmda	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... K ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) )
448	447	ex	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... K ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) )
449	380	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( 1 ... ( ( K - 1 ) + 1 ) ) = ( 1 ... K ) )
450	449	eleq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... ( ( K - 1 ) + 1 ) ) <-> o e. ( 1 ... K ) ) )
451	450	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 ) ) ) ) )
452	448 451	mpbird	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( o e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) ) )
453	452	imp	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. ( 1 ... ( N + K ) ) )
454		elfznn	|- ( ( d ` o ) e. ( 1 ... ( N + K ) ) -> ( d ` o ) e. NN )
455	453 454	syl	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. NN )
456	455	nncnd	|- ( ( ( ph /\ d e. B /\ 1 < K ) /\ o e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( d ` o ) e. CC )
457	440 441 442 443 397 444 456	telfsum2	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) = ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) )
458	457	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 ) ) ) )
459	380	fveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` ( ( K - 1 ) + 1 ) ) = ( d ` K ) )
460	459	oveq1d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) = ( ( d ` K ) - ( d ` 1 ) ) )
461	460	oveq2d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) )
462	343	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` 1 ) e. CC )
463	68 73	syl	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. NN )
464	463	nncnd	|- ( ( ph /\ d e. B ) -> ( d ` K ) e. CC )
465	464	3adant3	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` K ) e. CC )
466	462 465	pncan3d	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) = ( d ` K ) )
467		eqidd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( d ` K ) = ( d ` K ) )
468	466 467	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` K ) - ( d ` 1 ) ) ) = ( d ` K ) )
469	461 468	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + ( ( d ` ( ( K - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` K ) )
470	458 469	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( d ` ( s + 1 ) ) - ( d ` s ) ) ) = ( d ` K ) )
471	439 470	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 ) )
472	394 471	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
473	384 472	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> ( ( d ` 1 ) + sum_ k e. ( ( 1 + 1 ) ... K ) ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
474	377 473	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 ) )
475	363 474	eqtrd	|- ( ( ph /\ d e. B /\ 1 < K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
476	475	3expa	|- ( ( ( ph /\ d e. B ) /\ 1 < K ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
477	137	adantr	|- ( ( ph /\ d e. B ) -> 1 e. RR )
478	64	adantr	|- ( ( ph /\ d e. B ) -> K e. RR )
479	477 478	leloed	|- ( ( ph /\ d e. B ) -> ( 1 <_ K <-> ( 1 < K \/ 1 = K ) ) )
480	63 479	mpbid	|- ( ( ph /\ d e. B ) -> ( 1 < K \/ 1 = K ) )
481	480	orcomd	|- ( ( ph /\ d e. B ) -> ( 1 = K \/ 1 < K ) )
482	356 476 481	mpjaodan	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) = ( d ` K ) )
483		fsumconst	|- ( ( ( 1 ... K ) e. Fin /\ 1 e. CC ) -> sum_ k e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
484	289 256 483	syl2anc	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
485	59	adantr	|- ( ( ph /\ d e. B ) -> K e. NN0 )
486		hashfz1	|- ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
487	485 486	syl	|- ( ( ph /\ d e. B ) -> ( # ` ( 1 ... K ) ) = K )
488	487	oveq1d	|- ( ( ph /\ d e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = ( K x. 1 ) )
489	255	mulridd	|- ( ( ph /\ d e. B ) -> ( K x. 1 ) = K )
490	488 489	eqtrd	|- ( ( ph /\ d e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = K )
491	484 490	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) 1 = K )
492	482 491	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 ) )
493	335 492	eqtrd	|- ( ( ph /\ d e. B ) -> sum_ k e. ( 1 ... K ) ( if ( k = 1 , ( d ` 1 ) , ( ( d ` k ) - ( d ` ( k - 1 ) ) ) ) - 1 ) = ( ( d ` K ) - K ) )
494	288 493	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 ) )
495	464 255	subcld	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) e. CC )
496	495	addridd	|- ( ( ph /\ d e. B ) -> ( ( ( d ` K ) - K ) + 0 ) = ( ( d ` K ) - K ) )
497	496	eqcomd	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) = ( ( ( d ` K ) - K ) + 0 ) )
498		0cnd	|- ( ( ph /\ d e. B ) -> 0 e. CC )
499	495 498	addcomd	|- ( ( ph /\ d e. B ) -> ( ( ( d ` K ) - K ) + 0 ) = ( 0 + ( ( d ` K ) - K ) ) )
500	497 499	eqtrd	|- ( ( ph /\ d e. B ) -> ( ( d ` K ) - K ) = ( 0 + ( ( d ` K ) - K ) ) )
501	494 500	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 ) ) )
502	498 255 464	subsub2d	|- ( ( ph /\ d e. B ) -> ( 0 - ( K - ( d ` K ) ) ) = ( 0 + ( ( d ` K ) - K ) ) )
503	502	eqcomd	|- ( ( ph /\ d e. B ) -> ( 0 + ( ( d ` K ) - K ) ) = ( 0 - ( K - ( d ` K ) ) ) )
504	501 503	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 ) ) ) )
505	1	nn0cnd	|- ( ph -> N e. CC )
506	505	adantr	|- ( ( ph /\ d e. B ) -> N e. CC )
507	506	subidd	|- ( ( ph /\ d e. B ) -> ( N - N ) = 0 )
508	507	eqcomd	|- ( ( ph /\ d e. B ) -> 0 = ( N - N ) )
509	508	oveq1d	|- ( ( ph /\ d e. B ) -> ( 0 - ( K - ( d ` K ) ) ) = ( ( N - N ) - ( K - ( d ` K ) ) ) )
510	504 509	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 ) ) ) )
511	255 464	subcld	|- ( ( ph /\ d e. B ) -> ( K - ( d ` K ) ) e. CC )
512	506 506 511	subsub4d	|- ( ( ph /\ d e. B ) -> ( ( N - N ) - ( K - ( d ` K ) ) ) = ( N - ( N + ( K - ( d ` K ) ) ) ) )
513	510 512	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 ) ) ) ) )
514	506 255 464	addsubassd	|- ( ( ph /\ d e. B ) -> ( ( N + K ) - ( d ` K ) ) = ( N + ( K - ( d ` K ) ) ) )
515	514	eqcomd	|- ( ( ph /\ d e. B ) -> ( N + ( K - ( d ` K ) ) ) = ( ( N + K ) - ( d ` K ) ) )
516	515	oveq2d	|- ( ( ph /\ d e. B ) -> ( N - ( N + ( K - ( d ` K ) ) ) ) = ( N - ( ( N + K ) - ( d ` K ) ) ) )
517	513 516	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 ) ) ) )
518	276 517	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 ) ) ) )
519		eleq1	|- ( ( ( d ` 1 ) - 1 ) = if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( d ` 1 ) - 1 ) e. ZZ <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. ZZ ) )
520		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. ZZ <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. ZZ ) )
521		1zzd	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> 1 e. ZZ )
522	296 521	zsubcld	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> ( ( d ` 1 ) - 1 ) e. ZZ )
523	522	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ k = 1 ) -> ( ( d ` 1 ) - 1 ) e. ZZ )
524	521	adantr	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> 1 e. ZZ )
525	330 524	zsubcld	|- ( ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) /\ -. k = 1 ) -> ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) e. ZZ )
526	519 520 523 525	ifbothda	|- ( ( ph /\ d e. B /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. ZZ )
527	526	3expa	|- ( ( ( ph /\ d e. B ) /\ k e. ( 1 ... K ) ) -> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. ZZ )
528	275	eleq1d	|- ( ( ( 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 ) ) ) e. ZZ <-> if ( k = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` k ) - ( d ` ( k - 1 ) ) ) - 1 ) ) e. ZZ ) )
529	527 528	mpbird	|- ( ( ( 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 ) ) ) e. ZZ )
530	289 529	fsumzcl	|- ( ( 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 ) ) ) e. ZZ )
531	530	zcnd	|- ( ( 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 ) ) ) e. CC )
532	506 255	addcld	|- ( ( ph /\ d e. B ) -> ( N + K ) e. CC )
533	532 464	subcld	|- ( ( ph /\ d e. B ) -> ( ( N + K ) - ( d ` K ) ) e. CC )
534	531 533 506	addlsub	|- ( ( 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 <-> 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 ) ) ) ) )
535	518 534	mpbird	|- ( ( 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 )
536		eqidd	|- ( ( ph /\ d e. B ) -> N = N )
537	535 536	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 + K ) - ( d ` K ) ) ) = N )
538	262 537	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 )
539	254 538	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 )
540	231 539	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 )
541	219 540	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 )
542	201 541	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 ) )
543		ovex	|- ( 1 ... ( K + 1 ) ) e. _V
544	543	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
545		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 ) )
546		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 ) ) ) ) )
547	546	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 ) )
548	547	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 ) )
549	548	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 ) )
550	545 549	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 ) ) )
551	544 550	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 ) )
552	551	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 ) ) )
553	542 552	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 ) } )
554	5	a1i	|- ( ( ph /\ d e. B ) -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
555	554	eqcomd	|- ( ( ph /\ d e. B ) -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } = A )
556	553 555	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 )
557	289	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 )
558	34 40 556 557	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 ) ) ) )
559		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 ) ) ) ) )
560		simpr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> k = l )
561	560	eqeq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k = ( K + 1 ) <-> l = ( K + 1 ) ) )
562	560	eqeq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k = 1 <-> l = 1 ) )
563	560	fveq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( d ` k ) = ( d ` l ) )
564	560	oveq1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( k - 1 ) = ( l - 1 ) )
565	564	fveq2d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ k = l ) -> ( d ` ( k - 1 ) ) = ( d ` ( l - 1 ) ) )
566	563 565	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 ) ) ) )
567	566	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 ) )
568	562 567	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 ) ) )
569	561 568	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 ) ) ) )
570		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 e. ZZ )
571	60	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ZZ )
572	571	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. ZZ )
573	572	peano2zd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. ZZ )
574		elfzelz	|- ( l e. ( 1 ... j ) -> l e. ZZ )
575	574	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ZZ )
576		elfzle1	|- ( l e. ( 1 ... j ) -> 1 <_ l )
577	576	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 <_ l )
578	575	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. RR )
579		simp3	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ( 1 ... K ) )
580		elfznn	|- ( j e. ( 1 ... K ) -> j e. NN )
581	579 580	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. NN )
582	581	nnred	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. RR )
583	582	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. RR )
584	573	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. RR )
585		elfzle2	|- ( l e. ( 1 ... j ) -> l <_ j )
586	585	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ j )
587	64	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. RR )
588		1red	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. RR )
589	587 588	readdcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
590		elfzle2	|- ( j e. ( 1 ... K ) -> j <_ K )
591	579 590	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j <_ K )
592	587	lep1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K <_ ( K + 1 ) )
593	582 587 589 591 592	letrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j <_ ( K + 1 ) )
594	593	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j <_ ( K + 1 ) )
595	578 583 584 586 594	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ ( K + 1 ) )
596	570 573 575 577 595	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ( 1 ... ( K + 1 ) ) )
597		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( N + K ) - ( d ` K ) ) e. _V )
598		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( d ` 1 ) - 1 ) e. _V )
599		ovexd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. _V )
600	598 599	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 )
601	597 600	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 )
602	559 569 596 601	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 ) ) ) )
603	602	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 ) ) ) )
604	603	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 ) ) ) ) )
605		elfznn	|- ( l e. ( 1 ... j ) -> l e. NN )
606	605	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. NN )
607	606	nnred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. RR )
608	587	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. RR )
609		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 e. RR )
610	608 609	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( K + 1 ) e. RR )
611	581	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. NN )
612	611	nnred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j e. RR )
613	591	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> j <_ K )
614	607 612 608 586 613	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l <_ K )
615	608	ltp1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K < ( K + 1 ) )
616	607 608 610 614 615	lelttrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l < ( K + 1 ) )
617	607 616	ltned	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l =/= ( K + 1 ) )
618	617	neneqd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> -. l = ( K + 1 ) )
619	618	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 ) ) )
620	619	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 ) ) )
621	620	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 ) ) ) )
622	581	nnge1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 <_ j )
623	57	3ad2ant1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ZZ )
624	581	nnzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ZZ )
625		eluz	|- ( ( 1 e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` 1 ) <-> 1 <_ j ) )
626	623 624 625	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j e. ( ZZ>= ` 1 ) <-> 1 <_ j ) )
627	622 626	mpbird	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. ( ZZ>= ` 1 ) )
628		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 ) )
629		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 ) )
630	56	3adant3	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
631		simp1	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ph )
632	631 62	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 <_ K )
633	631 60	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ZZ )
634		eluz	|- ( ( 1 e. ZZ /\ K e. ZZ ) -> ( K e. ( ZZ>= ` 1 ) <-> 1 <_ K ) )
635	623 633 634	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( K e. ( ZZ>= ` 1 ) <-> 1 <_ K ) )
636	632 635	mpbird	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> K e. ( ZZ>= ` 1 ) )
637		eluzfz1	|- ( K e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... K ) )
638	636 637	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ( 1 ... K ) )
639	630 638	ffvelcdmd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. ( 1 ... ( N + K ) ) )
640	639 90	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. NN )
641	640	nnzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. ZZ )
642	641 623	zsubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) - 1 ) e. ZZ )
643	642	zcnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) - 1 ) e. CC )
644	643	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( ( d ` 1 ) - 1 ) e. CC )
645	644	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ l = 1 ) -> ( ( d ` 1 ) - 1 ) e. CC )
646	630	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
647	633	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> K e. ZZ )
648	606	nnzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ZZ )
649	606	nnge1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> 1 <_ l )
650	570 647 648 649 614	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> l e. ( 1 ... K ) )
651	646 650	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
652		elfzelz	|- ( ( d ` l ) e. ( 1 ... ( N + K ) ) -> ( d ` l ) e. ZZ )
653	651 652	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( d ` l ) e. ZZ )
654	653	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` l ) e. ZZ )
655	646	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
656		1zzd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 e. ZZ )
657	647	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> K e. ZZ )
658	648	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l e. ZZ )
659	658 656	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. ZZ )
660		neqne	|- ( -. l = 1 -> l =/= 1 )
661	660	adantl	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l =/= 1 )
662	609	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 e. RR )
663	607	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l e. RR )
664	649	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 <_ l )
665	662 663 664	leltned	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( 1 < l <-> l =/= 1 ) )
666	661 665	mpbird	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 < l )
667	656 658	zltlem1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( 1 < l <-> 1 <_ ( l - 1 ) ) )
668	666 667	mpbid	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> 1 <_ ( l - 1 ) )
669	659	zred	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. RR )
670	608	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> K e. RR )
671	663	lem1d	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) <_ l )
672	614	adantr	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> l <_ K )
673	669 663 670 671 672	letrd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) <_ K )
674	656 657 659 668 673	elfzd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( l - 1 ) e. ( 1 ... K ) )
675	655 674	ffvelcdmd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) )
676		elfzelz	|- ( ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l - 1 ) ) e. ZZ )
677	675 676	syl	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( d ` ( l - 1 ) ) e. ZZ )
678	654 677	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. ZZ )
679	678 656	zsubcld	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. ZZ )
680	679	zcnd	|- ( ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) /\ -. l = 1 ) -> ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) e. CC )
681	628 629 645 680	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 )
682		iftrue	|- ( l = 1 -> if ( l = 1 , ( ( d ` 1 ) - 1 ) , ( ( ( d ` l ) - ( d ` ( l - 1 ) ) ) - 1 ) ) = ( ( d ` 1 ) - 1 ) )
683	627 681 682	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 ) ) ) )
684	683	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 ) ) ) ) )
685	631 137	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. RR )
686	685	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. RR )
687	686 686	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( 1 + 1 ) e. RR )
688		elfzelz	|- ( l e. ( ( 1 + 1 ) ... j ) -> l e. ZZ )
689	688	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. ZZ )
690	689	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. RR )
691	686	ltp1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 < ( 1 + 1 ) )
692		elfzle1	|- ( l e. ( ( 1 + 1 ) ... j ) -> ( 1 + 1 ) <_ l )
693	692	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( 1 + 1 ) <_ l )
694	686 687 690 691 693	ltletrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 < l )
695	686 694	ltned	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 =/= l )
696	695	necomd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l =/= 1 )
697	696	neneqd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> -. l = 1 )
698	697	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 ) )
699	698	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 ) )
700	699	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 ) ) )
701	700	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 ) ) ) )
702		fzfid	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + 1 ) ... j ) e. Fin )
703	630	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
704		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. ZZ )
705	633	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> K e. ZZ )
706	686 687 691	ltled	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ ( 1 + 1 ) )
707	686 687 690 706 693	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ l )
708	582	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> j e. RR )
709	587	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> K e. RR )
710		elfzle2	|- ( l e. ( ( 1 + 1 ) ... j ) -> l <_ j )
711	710	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l <_ j )
712	591	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> j <_ K )
713	690 708 709 711 712	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l <_ K )
714	704 705 689 707 713	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. ( 1 ... K ) )
715	703 714	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
716	715 652	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. ZZ )
717	716	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` l ) e. CC )
718	689 704	zsubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. ZZ )
719		leaddsub	|- ( ( 1 e. RR /\ 1 e. RR /\ l e. RR ) -> ( ( 1 + 1 ) <_ l <-> 1 <_ ( l - 1 ) ) )
720	686 686 690 719	syl3anc	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( 1 + 1 ) <_ l <-> 1 <_ ( l - 1 ) ) )
721	693 720	mpbid	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 <_ ( l - 1 ) )
722	690 686	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. RR )
723	690	lem1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) <_ l )
724	722 690 709 723 713	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) <_ K )
725	704 705 718 721 724	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( l - 1 ) e. ( 1 ... K ) )
726	703 725	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) )
727	676	zcnd	|- ( ( d ` ( l - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l - 1 ) ) e. CC )
728	726 727	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( l - 1 ) ) e. CC )
729	717 728	subcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. CC )
730		1cnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> 1 e. CC )
731	702 729 730	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 ) )
732	731	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 ) ) )
733	732	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 ) ) ) )
734		1cnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. CC )
735		fsumconst	|- ( ( ( ( 1 + 1 ) ... j ) e. Fin /\ 1 e. CC ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) )
736	702 734 735	syl2anc	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) )
737		hashfzp1	|- ( j e. ( ZZ>= ` 1 ) -> ( # ` ( ( 1 + 1 ) ... j ) ) = ( j - 1 ) )
738	627 737	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( # ` ( ( 1 + 1 ) ... j ) ) = ( j - 1 ) )
739	738	oveq1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) = ( ( j - 1 ) x. 1 ) )
740	581	nncnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> j e. CC )
741	740 734	subcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. CC )
742	741	mulridd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) x. 1 ) = ( j - 1 ) )
743	739 742	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( # ` ( ( 1 + 1 ) ... j ) ) x. 1 ) = ( j - 1 ) )
744	736 743	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) 1 = ( j - 1 ) )
745	744	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 ) ) )
746	745	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 ) ) ) )
747	746	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 ) ) ) ) )
748	702 729	fsumcl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> sum_ l e. ( ( 1 + 1 ) ... j ) ( ( d ` l ) - ( d ` ( l - 1 ) ) ) e. CC )
749	643 748 741	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 ) ) ) )
750	749	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 ) ) )
751	750	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 ) ) ) )
752	643 748	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 )
753	740 752 741	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 ) ) ) )
754	753	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 ) ) )
755	740 752 741	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 ) ) ) ) ) )
756	740 734	nncand	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - ( j - 1 ) ) = 1 )
757		1zzd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> 1 e. ZZ )
758	624 623	zsubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. ZZ )
759	630	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
760		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 e. ZZ )
761	633	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> K e. ZZ )
762		elfzelz	|- ( l e. ( 1 ... ( j - 1 ) ) -> l e. ZZ )
763	762	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ZZ )
764	763	peano2zd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ZZ )
765		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 e. RR )
766	763	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. RR )
767	766 765	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. RR )
768		elfzle1	|- ( l e. ( 1 ... ( j - 1 ) ) -> 1 <_ l )
769	768	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 <_ l )
770	766	lep1d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( l + 1 ) )
771	765 766 767 769 770	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> 1 <_ ( l + 1 ) )
772	582	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j e. RR )
773	772 765	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) e. RR )
774	587	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> K e. RR )
775	774 765	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( K - 1 ) e. RR )
776		elfzle2	|- ( l e. ( 1 ... ( j - 1 ) ) -> l <_ ( j - 1 ) )
777	776	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( j - 1 ) )
778	591	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> j <_ K )
779	772 774 765 778	lesub1dd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) <_ ( K - 1 ) )
780	766 773 775 777 779	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ ( K - 1 ) )
781		leaddsub	|- ( ( l e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( l + 1 ) <_ K <-> l <_ ( K - 1 ) ) )
782	766 765 774 781	syl3anc	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( l + 1 ) <_ K <-> l <_ ( K - 1 ) ) )
783	780 782	mpbird	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) <_ K )
784	760 761 764 771 783	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( l + 1 ) e. ( 1 ... K ) )
785	759 784	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` ( l + 1 ) ) e. ( 1 ... ( N + K ) ) )
786		elfzelz	|- ( ( d ` ( l + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( d ` ( l + 1 ) ) e. ZZ )
787	785 786	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` ( l + 1 ) ) e. ZZ )
788	582 685	resubcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) e. RR )
789	582	lem1d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) <_ j )
790	788 582 587 789 591	letrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( j - 1 ) <_ K )
791	790	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( j - 1 ) <_ K )
792	766 773 774 777 791	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l <_ K )
793	760 761 763 769 792	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> l e. ( 1 ... K ) )
794	759 793	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` l ) e. ( 1 ... ( N + K ) ) )
795	794 652	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( d ` l ) e. ZZ )
796	787 795	zsubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) e. ZZ )
797	796	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... ( j - 1 ) ) ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) e. CC )
798		fvoveq1	|- ( l = ( w - 1 ) -> ( d ` ( l + 1 ) ) = ( d ` ( ( w - 1 ) + 1 ) ) )
799		fveq2	|- ( l = ( w - 1 ) -> ( d ` l ) = ( d ` ( w - 1 ) ) )
800	798 799	oveq12d	|- ( l = ( w - 1 ) -> ( ( d ` ( l + 1 ) ) - ( d ` l ) ) = ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) )
801	757 757 758 797 800	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 ) ) ) )
802		oveq1	|- ( w = l -> ( w - 1 ) = ( l - 1 ) )
803	802	fvoveq1d	|- ( w = l -> ( d ` ( ( w - 1 ) + 1 ) ) = ( d ` ( ( l - 1 ) + 1 ) ) )
804	802	fveq2d	|- ( w = l -> ( d ` ( w - 1 ) ) = ( d ` ( l - 1 ) ) )
805	803 804	oveq12d	|- ( w = l -> ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) ) = ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) ) )
806		nfcv	|- F/_ l ( ( d ` ( ( w - 1 ) + 1 ) ) - ( d ` ( w - 1 ) ) )
807		nfcv	|- F/_ w ( ( d ` ( ( l - 1 ) + 1 ) ) - ( d ` ( l - 1 ) ) )
808	805 806 807	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 ) ) )
809	808	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 ) ) ) )
810	801 809	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 ) ) ) )
811	740 734	npcand	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) = j )
812	811	oveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + 1 ) ... ( ( j - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... j ) )
813	812	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 ) ) ) )
814	690	recnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> l e. CC )
815	814 730	npcand	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( ( l - 1 ) + 1 ) = l )
816	815	fveq2d	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ l e. ( ( 1 + 1 ) ... j ) ) -> ( d ` ( ( l - 1 ) + 1 ) ) = ( d ` l ) )
817	816	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 ) ) ) )
818	817	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 ) ) ) )
819	813 818	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 ) ) ) )
820	810 819	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 ) ) ) )
821	820	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 ) ) )
822	821	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 ) ) ) )
823	756 822	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 ) ) ) ) )
824		fveq2	|- ( r = l -> ( d ` r ) = ( d ` l ) )
825		fveq2	|- ( r = ( l + 1 ) -> ( d ` r ) = ( d ` ( l + 1 ) ) )
826		fveq2	|- ( r = 1 -> ( d ` r ) = ( d ` 1 ) )
827		fveq2	|- ( r = ( ( j - 1 ) + 1 ) -> ( d ` r ) = ( d ` ( ( j - 1 ) + 1 ) ) )
828	811 627	eqeltrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
829	630	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
830		1zzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 e. ZZ )
831	633	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> K e. ZZ )
832		elfzelz	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> r e. ZZ )
833	832	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. ZZ )
834		elfzle1	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> 1 <_ r )
835	834	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 <_ r )
836	833	zred	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. RR )
837	582	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> j e. RR )
838		1red	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> 1 e. RR )
839	837 838	resubcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( j - 1 ) e. RR )
840	839 838	readdcld	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( ( j - 1 ) + 1 ) e. RR )
841	587	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> K e. RR )
842		elfzle2	|- ( r e. ( 1 ... ( ( j - 1 ) + 1 ) ) -> r <_ ( ( j - 1 ) + 1 ) )
843	842	adantl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r <_ ( ( j - 1 ) + 1 ) )
844	811 591	eqbrtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( j - 1 ) + 1 ) <_ K )
845	844	adantr	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( ( j - 1 ) + 1 ) <_ K )
846	836 840 841 843 845	letrd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r <_ K )
847	830 831 833 835 846	elfzd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> r e. ( 1 ... K ) )
848	829 847	ffvelcdmd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. ( 1 ... ( N + K ) ) )
849		elfzelz	|- ( ( d ` r ) e. ( 1 ... ( N + K ) ) -> ( d ` r ) e. ZZ )
850	848 849	syl	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. ZZ )
851	850	zcnd	|- ( ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) /\ r e. ( 1 ... ( ( j - 1 ) + 1 ) ) ) -> ( d ` r ) e. CC )
852	824 825 826 827 758 828 851	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 ) ) )
853	852	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 ) ) ) )
854	853	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 ) ) ) ) )
855	811	fveq2d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) = ( d ` j ) )
856	630 579	ffvelcdmd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` j ) e. ( 1 ... ( N + K ) ) )
857		elfzelz	|- ( ( d ` j ) e. ( 1 ... ( N + K ) ) -> ( d ` j ) e. ZZ )
858	856 857	syl	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` j ) e. ZZ )
859	855 858	eqeltrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) e. ZZ )
860	859	zcnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` ( ( j - 1 ) + 1 ) ) e. CC )
861	640	nnred	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. RR )
862	861	recnd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( d ` 1 ) e. CC )
863	860 862	subcld	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) e. CC )
864	734 643 863	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 ) ) ) ) )
865	864	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 ) ) ) )
866	734 862	pncan3d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( d ` 1 ) - 1 ) ) = ( d ` 1 ) )
867	866	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 ) ) ) )
868	862 860	pncan3d	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` ( ( j - 1 ) + 1 ) ) )
869	868 855	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( d ` 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` j ) )
870	867 869	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( ( 1 + ( ( d ` 1 ) - 1 ) ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) = ( d ` j ) )
871	865 870	eqtrd	|- ( ( ph /\ d e. B /\ j e. ( 1 ... K ) ) -> ( 1 + ( ( ( d ` 1 ) - 1 ) + ( ( d ` ( ( j - 1 ) + 1 ) ) - ( d ` 1 ) ) ) ) = ( d ` j ) )
872	854 871	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 ) )
873	823 872	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 ) )
874	755 873	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 ) )
875	754 874	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 ) )
876	751 875	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 ) )
877	747 876	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 ) )
878	733 877	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 ) )
879	701 878	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 ) )
880	684 879	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 ) )
881	621 880	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 ) )
882	604 881	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 ) )
883	882	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 ) )
884	883	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 ) ) )
885		nfcv	|- F/_ q ( d ` j )
886		nfcv	|- F/_ j ( d ` q )
887		fveq2	|- ( j = q -> ( d ` j ) = ( d ` q ) )
888	885 886 887	cbvmpt	|- ( j e. ( 1 ... K ) |-> ( d ` j ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) )
889	888	a1i	|- ( ( ph /\ d e. B ) -> ( j e. ( 1 ... K ) |-> ( d ` j ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
890	884 889	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 ) ) )
891	558 890	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 ) ) )
892	33 891	eqtrd	|- ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
893	56	ffnd	|- ( ( ph /\ d e. B ) -> d Fn ( 1 ... K ) )
894		dffn5	|- ( d Fn ( 1 ... K ) <-> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
895	894	biimpi	|- ( d Fn ( 1 ... K ) -> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
896	893 895	syl	|- ( ( ph /\ d e. B ) -> d = ( q e. ( 1 ... K ) |-> ( d ` q ) ) )
897	896	eqcomd	|- ( ( ph /\ d e. B ) -> ( q e. ( 1 ... K ) |-> ( d ` q ) ) = d )
898	892 897	eqtrd	|- ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = d )
899	898	ralrimiva	|- ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )