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