Metamath Proof Explorer

Theorem sticksstones10

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

Ref Expression
Hypotheses sticksstones10.1 
|- ( ph -> N e. NN0 )
sticksstones10.2 
|- ( ph -> K e. NN )
sticksstones10.3 
|- 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 ) ) ) ) ) )
sticksstones10.4 
|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
sticksstones10.5 
|- 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 sticksstones10 
|- ( ph -> G : B --> A )

Proof

Step Hyp Ref Expression
1 sticksstones10.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones10.2 
 |-  ( ph -> K e. NN )
3 sticksstones10.3 
 |-  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 ) ) ) ) ) )
4 sticksstones10.4 
 |-  A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
5 sticksstones10.5 
 |-  B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
6 2 nnne0d 
 |-  ( ph -> K =/= 0 )
7 6 adantr 
 |-  ( ( ph /\ b e. B ) -> K =/= 0 )
8 7 neneqd 
 |-  ( ( ph /\ b e. B ) -> -. K = 0 )
9 8 iffalsed 
 |-  ( ( ph /\ 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 ) ) ) ) ) = ( 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 ) ) ) ) )
10 9 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( 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 = 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 ) ) ) ) ) )
11 eleq1 
 |-  ( ( ( N + K ) - ( b ` K ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) -> ( ( ( N + K ) - ( b ` K ) ) e. NN0 <-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) e. NN0 ) )
12 eleq1 
 |-  ( if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) -> ( if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) e. NN0 <-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) e. NN0 ) )
13 1 nn0zd 
 |-  ( ph -> N e. ZZ )
14 13 adantr 
 |-  ( ( ph /\ b e. B ) -> N e. ZZ )
15 2 nnzd 
 |-  ( ph -> K e. ZZ )
16 15 adantr 
 |-  ( ( ph /\ b e. B ) -> K e. ZZ )
17 14 16 zaddcld 
 |-  ( ( ph /\ b e. B ) -> ( N + K ) e. ZZ )
18 5 eleq2i 
 |-  ( b e. B <-> b e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
19 vex 
 |-  b e. _V
20 feq1 
 |-  ( f = b -> ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) ) )
21 fveq1 
 |-  ( f = b -> ( f ` x ) = ( b ` x ) )
22 fveq1 
 |-  ( f = b -> ( f ` y ) = ( b ` y ) )
23 21 22 breq12d 
 |-  ( f = b -> ( ( f ` x ) < ( f ` y ) <-> ( b ` x ) < ( b ` y ) ) )
24 23 imbi2d 
 |-  ( f = b -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( b ` x ) < ( b ` y ) ) ) )
25 24 2ralbidv 
 |-  ( f = b -> ( 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 -> ( b ` x ) < ( b ` y ) ) ) )
26 20 25 anbi12d 
 |-  ( f = b -> ( ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) ) ) )
27 19 26 elab 
 |-  ( b e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> ( b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) ) )
28 18 27 bitri 
 |-  ( b e. B <-> ( b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) ) )
29 28 bilani 
 |-  ( ( ph /\ b e. B ) -> ( b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) ) )
30 29 simpld 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
31 1zzd 
 |-  ( ( ph /\ b e. B ) -> 1 e. ZZ )
32 2 nnge1d 
 |-  ( ph -> 1 <_ K )
33 32 adantr 
 |-  ( ( ph /\ b e. B ) -> 1 <_ K )
34 16 zred 
 |-  ( ( ph /\ b e. B ) -> K e. RR )
35 34 leidd 
 |-  ( ( ph /\ b e. B ) -> K <_ K )
36 31 16 16 33 35 elfzd 
 |-  ( ( ph /\ b e. B ) -> K e. ( 1 ... K ) )
37 30 36 ffvelcdmd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. ( 1 ... ( N + K ) ) )
38 elfznn 
 |-  ( ( b ` K ) e. ( 1 ... ( N + K ) ) -> ( b ` K ) e. NN )
39 37 38 syl 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. NN )
40 39 nnzd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. ZZ )
41 17 40 zsubcld 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) e. ZZ )
42 39 nnred 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. RR )
43 42 recnd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. CC )
44 43 addridd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` K ) + 0 ) = ( b ` K ) )
45 elfzle2 
 |-  ( ( b ` K ) e. ( 1 ... ( N + K ) ) -> ( b ` K ) <_ ( N + K ) )
46 37 45 syl 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) <_ ( N + K ) )
47 44 46 eqbrtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` K ) + 0 ) <_ ( N + K ) )
48 0red 
 |-  ( ( ph /\ b e. B ) -> 0 e. RR )
49 17 zred 
 |-  ( ( ph /\ b e. B ) -> ( N + K ) e. RR )
50 42 48 49 leaddsub2d 
 |-  ( ( ph /\ b e. B ) -> ( ( ( b ` K ) + 0 ) <_ ( N + K ) <-> 0 <_ ( ( N + K ) - ( b ` K ) ) ) )
51 47 50 mpbid 
 |-  ( ( ph /\ b e. B ) -> 0 <_ ( ( N + K ) - ( b ` K ) ) )
52 41 51 jca 
 |-  ( ( ph /\ b e. B ) -> ( ( ( N + K ) - ( b ` K ) ) e. ZZ /\ 0 <_ ( ( N + K ) - ( b ` K ) ) ) )
53 elnn0z 
 |-  ( ( ( N + K ) - ( b ` K ) ) e. NN0 <-> ( ( ( N + K ) - ( b ` K ) ) e. ZZ /\ 0 <_ ( ( N + K ) - ( b ` K ) ) ) )
54 52 53 sylibr 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) e. NN0 )
55 54 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( b ` K ) ) e. NN0 )
56 55 3impa 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( b ` K ) ) e. NN0 )
57 56 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( b ` K ) ) e. NN0 )
58 eleq1 
 |-  ( ( ( b ` 1 ) - 1 ) = if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( b ` 1 ) - 1 ) e. NN0 <-> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) e. NN0 ) )
59 eleq1 
 |-  ( ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) = if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) -> ( ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. NN0 <-> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) e. NN0 ) )
60 1red 
 |-  ( ( ph /\ b e. B ) -> 1 e. RR )
61 60 leidd 
 |-  ( ( ph /\ b e. B ) -> 1 <_ 1 )
62 31 16 31 61 33 elfzd 
 |-  ( ( ph /\ b e. B ) -> 1 e. ( 1 ... K ) )
63 30 62 ffvelcdmd 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. ( 1 ... ( N + K ) ) )
64 elfznn 
 |-  ( ( b ` 1 ) e. ( 1 ... ( N + K ) ) -> ( b ` 1 ) e. NN )
65 64 nnzd 
 |-  ( ( b ` 1 ) e. ( 1 ... ( N + K ) ) -> ( b ` 1 ) e. ZZ )
66 63 65 syl 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. ZZ )
67 66 31 zsubcld 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) - 1 ) e. ZZ )
68 1cnd 
 |-  ( ( ph /\ b e. B ) -> 1 e. CC )
69 68 addridd 
 |-  ( ( ph /\ b e. B ) -> ( 1 + 0 ) = 1 )
70 elfzle1 
 |-  ( ( b ` 1 ) e. ( 1 ... ( N + K ) ) -> 1 <_ ( b ` 1 ) )
71 63 70 syl 
 |-  ( ( ph /\ b e. B ) -> 1 <_ ( b ` 1 ) )
72 69 71 eqbrtrd 
 |-  ( ( ph /\ b e. B ) -> ( 1 + 0 ) <_ ( b ` 1 ) )
73 66 zred 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. RR )
74 60 48 73 leaddsub2d 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 + 0 ) <_ ( b ` 1 ) <-> 0 <_ ( ( b ` 1 ) - 1 ) ) )
75 72 74 mpbid 
 |-  ( ( ph /\ b e. B ) -> 0 <_ ( ( b ` 1 ) - 1 ) )
76 67 75 jca 
 |-  ( ( ph /\ b e. B ) -> ( ( ( b ` 1 ) - 1 ) e. ZZ /\ 0 <_ ( ( b ` 1 ) - 1 ) ) )
77 elnn0z 
 |-  ( ( ( b ` 1 ) - 1 ) e. NN0 <-> ( ( ( b ` 1 ) - 1 ) e. ZZ /\ 0 <_ ( ( b ` 1 ) - 1 ) ) )
78 76 77 sylibr 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) - 1 ) e. NN0 )
79 78 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( b ` 1 ) - 1 ) e. NN0 )
80 79 3impa 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( b ` 1 ) - 1 ) e. NN0 )
81 80 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( ( b ` 1 ) - 1 ) e. NN0 )
82 81 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( b ` 1 ) - 1 ) e. NN0 )
83 30 3adant3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
84 83 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
85 1zzd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 e. ZZ )
86 16 3adant3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> K e. ZZ )
87 86 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. ZZ )
88 simp3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ( 1 ... ( K + 1 ) ) )
89 elfznn 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k e. NN )
90 88 89 syl 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. NN )
91 90 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. NN )
92 91 nnzd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ZZ )
93 91 nnge1d 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 <_ k )
94 elfzle2 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k <_ ( K + 1 ) )
95 88 94 syl 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> k <_ ( K + 1 ) )
96 95 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ ( K + 1 ) )
97 neqne 
 |-  ( -. k = ( K + 1 ) -> k =/= ( K + 1 ) )
98 97 adantl 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k =/= ( K + 1 ) )
99 98 necomd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) =/= k )
100 96 99 jca 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) )
101 91 nnred 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. RR )
102 87 zred 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. RR )
103 1red 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 e. RR )
104 102 103 readdcld 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. RR )
105 101 104 ltlend 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k < ( K + 1 ) <-> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) ) )
106 100 105 mpbird 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k < ( K + 1 ) )
107 90 nnzd 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
108 zleltp1 
 |-  ( ( k e. ZZ /\ K e. ZZ ) -> ( k <_ K <-> k < ( K + 1 ) ) )
109 107 86 108 syl2anc 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( k <_ K <-> k < ( K + 1 ) ) )
110 109 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ K <-> k < ( K + 1 ) ) )
111 106 110 mpbird 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ K )
112 85 87 92 93 111 elfzd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ( 1 ... K ) )
113 84 112 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( b ` k ) e. ( 1 ... ( N + K ) ) )
114 elfznn 
 |-  ( ( b ` k ) e. ( 1 ... ( N + K ) ) -> ( b ` k ) e. NN )
115 113 114 syl 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( b ` k ) e. NN )
116 115 nnzd 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( b ` k ) e. ZZ )
117 116 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` k ) e. ZZ )
118 84 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
119 1zzd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
120 87 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
121 92 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
122 121 119 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
123 93 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
124 neqne 
 |-  ( -. k = 1 -> k =/= 1 )
125 124 adantl 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k =/= 1 )
126 123 125 jca 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 <_ k /\ k =/= 1 ) )
127 103 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
128 101 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. RR )
129 127 128 ltlend 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 <_ k /\ k =/= 1 ) ) )
130 126 129 mpbird 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 < k )
131 119 121 zltlem1d 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> 1 <_ ( k - 1 ) ) )
132 130 131 mpbid 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
133 90 nnred 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. RR )
134 60 3adant3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> 1 e. RR )
135 34 3adant3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> K e. RR )
136 lesubadd 
 |-  ( ( k e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( k - 1 ) <_ K <-> k <_ ( K + 1 ) ) )
137 133 134 135 136 syl3anc 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( k - 1 ) <_ K <-> k <_ ( K + 1 ) ) )
138 95 137 mpbird 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( k - 1 ) <_ K )
139 138 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k - 1 ) <_ K )
140 139 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
141 119 120 122 132 140 elfzd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
142 118 141 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) )
143 elfznn 
 |-  ( ( b ` ( k - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( b ` ( k - 1 ) ) e. NN )
144 142 143 syl 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) e. NN )
145 144 nnzd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) e. ZZ )
146 117 145 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( b ` k ) - ( b ` ( k - 1 ) ) ) e. ZZ )
147 146 119 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. ZZ )
148 0p1e1 
 |-  ( 0 + 1 ) = 1
149 148 a1i 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 0 + 1 ) = 1 )
150 1cnd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
151 150 subidd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 - 1 ) = 0 )
152 145 zred 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) e. RR )
153 152 recnd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) e. CC )
154 153 addridd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( b ` ( k - 1 ) ) + 0 ) = ( b ` ( k - 1 ) ) )
155 128 ltm1d 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) < k )
156 112 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... K ) )
157 141 156 jca 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - 1 ) e. ( 1 ... K ) /\ k e. ( 1 ... K ) ) )
158 29 simprd 
 |-  ( ( ph /\ b e. B ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) )
159 158 3adant3 
 |-  ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) )
160 159 adantr 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) )
161 160 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) )
162 breq1 
 |-  ( x = ( k - 1 ) -> ( x < y <-> ( k - 1 ) < y ) )
163 fveq2 
 |-  ( x = ( k - 1 ) -> ( b ` x ) = ( b ` ( k - 1 ) ) )
164 163 breq1d 
 |-  ( x = ( k - 1 ) -> ( ( b ` x ) < ( b ` y ) <-> ( b ` ( k - 1 ) ) < ( b ` y ) ) )
165 162 164 imbi12d 
 |-  ( x = ( k - 1 ) -> ( ( x < y -> ( b ` x ) < ( b ` y ) ) <-> ( ( k - 1 ) < y -> ( b ` ( k - 1 ) ) < ( b ` y ) ) ) )
166 breq2 
 |-  ( y = k -> ( ( k - 1 ) < y <-> ( k - 1 ) < k ) )
167 fveq2 
 |-  ( y = k -> ( b ` y ) = ( b ` k ) )
168 167 breq2d 
 |-  ( y = k -> ( ( b ` ( k - 1 ) ) < ( b ` y ) <-> ( b ` ( k - 1 ) ) < ( b ` k ) ) )
169 166 168 imbi12d 
 |-  ( y = k -> ( ( ( k - 1 ) < y -> ( b ` ( k - 1 ) ) < ( b ` y ) ) <-> ( ( k - 1 ) < k -> ( b ` ( k - 1 ) ) < ( b ` k ) ) ) )
170 165 169 rspc2va 
 |-  ( ( ( ( k - 1 ) e. ( 1 ... K ) /\ k e. ( 1 ... K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( b ` x ) < ( b ` y ) ) ) -> ( ( k - 1 ) < k -> ( b ` ( k - 1 ) ) < ( b ` k ) ) )
171 157 161 170 syl2anc 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - 1 ) < k -> ( b ` ( k - 1 ) ) < ( b ` k ) ) )
172 155 171 mpd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` ( k - 1 ) ) < ( b ` k ) )
173 154 172 eqbrtrd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( b ` ( k - 1 ) ) + 0 ) < ( b ` k ) )
174 0red 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 e. RR )
175 117 zred 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( b ` k ) e. RR )
176 152 174 175 ltaddsub2d 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( b ` ( k - 1 ) ) + 0 ) < ( b ` k ) <-> 0 < ( ( b ` k ) - ( b ` ( k - 1 ) ) ) ) )
177 173 176 mpbid 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 < ( ( b ` k ) - ( b ` ( k - 1 ) ) ) )
178 151 177 eqbrtrd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 - 1 ) < ( ( b ` k ) - ( b ` ( k - 1 ) ) ) )
179 zlem1lt 
 |-  ( ( 1 e. ZZ /\ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) e. ZZ ) -> ( 1 <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) <-> ( 1 - 1 ) < ( ( b ` k ) - ( b ` ( k - 1 ) ) ) ) )
180 119 146 179 syl2anc 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) <-> ( 1 - 1 ) < ( ( b ` k ) - ( b ` ( k - 1 ) ) ) ) )
181 178 180 mpbird 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) )
182 149 181 eqbrtrd 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 0 + 1 ) <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) )
183 146 zred 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( b ` k ) - ( b ` ( k - 1 ) ) ) e. RR )
184 leaddsub 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) e. RR ) -> ( ( 0 + 1 ) <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) <-> 0 <_ ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) )
185 174 127 183 184 syl3anc 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 0 + 1 ) <_ ( ( b ` k ) - ( b ` ( k - 1 ) ) ) <-> 0 <_ ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) )
186 182 185 mpbid 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 0 <_ ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) )
187 147 186 jca 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. ZZ /\ 0 <_ ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) )
188 elnn0z 
 |-  ( ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. NN0 <-> ( ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. ZZ /\ 0 <_ ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) )
189 187 188 sylibr 
 |-  ( ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) e. NN0 )
190 58 59 82 189 ifbothda 
 |-  ( ( ( ph /\ b e. B /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) e. NN0 )
191 11 12 57 190 ifbothda 
 |-  ( ( ph /\ b e. B /\ 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 ) ) ) e. NN0 )
192 191 3expa 
 |-  ( ( ( ph /\ b e. B ) /\ 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 ) ) ) e. NN0 )
193 192 fmpttd 
 |-  ( ( ph /\ b e. B ) -> ( 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 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 )
194 eqidd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 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 ) ) ) ) = ( 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 ) ) ) ) )
195 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> k = i )
196 195 eqeq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( k = ( K + 1 ) <-> i = ( K + 1 ) ) )
197 195 eqeq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( k = 1 <-> i = 1 ) )
198 195 fveq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( b ` k ) = ( b ` i ) )
199 195 fvoveq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( b ` ( k - 1 ) ) = ( b ` ( i - 1 ) ) )
200 198 199 oveq12d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( ( b ` k ) - ( b ` ( k - 1 ) ) ) = ( ( b ` i ) - ( b ` ( i - 1 ) ) ) )
201 200 oveq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) = ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) )
202 197 201 ifbieq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) )
203 196 202 ifbieq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) /\ k = i ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) )
204 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. ( 1 ... ( K + 1 ) ) )
205 ovexd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( b ` K ) ) e. _V )
206 ovexd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( b ` 1 ) - 1 ) e. _V )
207 ovexd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) e. _V )
208 206 207 ifcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) e. _V )
209 205 208 ifcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. _V )
210 194 203 204 209 fvmptd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) )
211 210 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) )
212 2 adantr 
 |-  ( ( ph /\ b e. B ) -> K e. NN )
213 nnuz 
 |-  NN = ( ZZ>= ` 1 )
214 212 213 eleqtrdi 
 |-  ( ( ph /\ b e. B ) -> K e. ( ZZ>= ` 1 ) )
215 eleq1 
 |-  ( ( ( N + K ) - ( b ` K ) ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) -> ( ( ( N + K ) - ( b ` K ) ) e. ZZ <-> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. ZZ ) )
216 eleq1 
 |-  ( if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) -> ( if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) e. ZZ <-> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. ZZ ) )
217 14 3adant3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> N e. ZZ )
218 217 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> N e. ZZ )
219 16 3adant3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> K e. ZZ )
220 219 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> K e. ZZ )
221 218 220 zaddcld 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> ( N + K ) e. ZZ )
222 39 3adant3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( b ` K ) e. NN )
223 222 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> ( b ` K ) e. NN )
224 223 nnzd 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> ( b ` K ) e. ZZ )
225 221 224 zsubcld 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ i = ( K + 1 ) ) -> ( ( N + K ) - ( b ` K ) ) e. ZZ )
226 eleq1 
 |-  ( ( ( b ` 1 ) - 1 ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) -> ( ( ( b ` 1 ) - 1 ) e. ZZ <-> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) e. ZZ ) )
227 eleq1 
 |-  ( ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) -> ( ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) e. ZZ <-> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) e. ZZ ) )
228 66 3adant3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( b ` 1 ) e. ZZ )
229 228 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( b ` 1 ) e. ZZ )
230 229 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ i = 1 ) -> ( b ` 1 ) e. ZZ )
231 1zzd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ i = 1 ) -> 1 e. ZZ )
232 230 231 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ i = 1 ) -> ( ( b ` 1 ) - 1 ) e. ZZ )
233 30 3adant3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
234 233 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
235 234 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
236 1zzd 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> 1 e. ZZ )
237 219 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> K e. ZZ )
238 elfznn 
 |-  ( i e. ( 1 ... ( K + 1 ) ) -> i e. NN )
239 238 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. NN )
240 239 3impa 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. NN )
241 240 nnzd 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. ZZ )
242 241 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i e. ZZ )
243 240 nnge1d 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> 1 <_ i )
244 243 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> 1 <_ i )
245 simp3 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. ( 1 ... ( K + 1 ) ) )
246 elfzle2 
 |-  ( i e. ( 1 ... ( K + 1 ) ) -> i <_ ( K + 1 ) )
247 245 246 syl 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> i <_ ( K + 1 ) )
248 247 adantr 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i <_ ( K + 1 ) )
249 neqne 
 |-  ( -. i = ( K + 1 ) -> i =/= ( K + 1 ) )
250 249 adantl 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i =/= ( K + 1 ) )
251 250 necomd 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( K + 1 ) =/= i )
252 248 251 jca 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( i <_ ( K + 1 ) /\ ( K + 1 ) =/= i ) )
253 242 zred 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i e. RR )
254 237 zred 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> K e. RR )
255 1red 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> 1 e. RR )
256 254 255 readdcld 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( K + 1 ) e. RR )
257 253 256 ltlend 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( i < ( K + 1 ) <-> ( i <_ ( K + 1 ) /\ ( K + 1 ) =/= i ) ) )
258 252 257 mpbird 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i < ( K + 1 ) )
259 zleltp1 
 |-  ( ( i e. ZZ /\ K e. ZZ ) -> ( i <_ K <-> i < ( K + 1 ) ) )
260 242 237 259 syl2anc 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> ( i <_ K <-> i < ( K + 1 ) ) )
261 258 260 mpbird 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i <_ K )
262 236 237 242 244 261 elfzd 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> i e. ( 1 ... K ) )
263 262 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> i e. ( 1 ... K ) )
264 235 263 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` i ) e. ( 1 ... ( N + K ) ) )
265 elfznn 
 |-  ( ( b ` i ) e. ( 1 ... ( N + K ) ) -> ( b ` i ) e. NN )
266 264 265 syl 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` i ) e. NN )
267 266 nnzd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` i ) e. ZZ )
268 1zzd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> 1 e. ZZ )
269 237 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> K e. ZZ )
270 242 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> i e. ZZ )
271 270 268 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ZZ )
272 244 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> 1 <_ i )
273 neqne 
 |-  ( -. i = 1 -> i =/= 1 )
274 273 adantl 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> i =/= 1 )
275 272 274 jca 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( 1 <_ i /\ i =/= 1 ) )
276 1red 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> 1 e. RR )
277 270 zred 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> i e. RR )
278 276 277 ltlend 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( 1 < i <-> ( 1 <_ i /\ i =/= 1 ) ) )
279 275 278 mpbird 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> 1 < i )
280 zltp1le 
 |-  ( ( 1 e. ZZ /\ i e. ZZ ) -> ( 1 < i <-> ( 1 + 1 ) <_ i ) )
281 268 270 280 syl2anc 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( 1 < i <-> ( 1 + 1 ) <_ i ) )
282 279 281 mpbid 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( 1 + 1 ) <_ i )
283 leaddsub 
 |-  ( ( 1 e. RR /\ 1 e. RR /\ i e. RR ) -> ( ( 1 + 1 ) <_ i <-> 1 <_ ( i - 1 ) ) )
284 276 276 277 283 syl3anc 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( ( 1 + 1 ) <_ i <-> 1 <_ ( i - 1 ) ) )
285 282 284 mpbid 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> 1 <_ ( i - 1 ) )
286 248 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> i <_ ( K + 1 ) )
287 254 adantr 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> K e. RR )
288 lesubadd 
 |-  ( ( i e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( i - 1 ) <_ K <-> i <_ ( K + 1 ) ) )
289 277 276 287 288 syl3anc 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( ( i - 1 ) <_ K <-> i <_ ( K + 1 ) ) )
290 286 289 mpbird 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( i - 1 ) <_ K )
291 268 269 271 285 290 elfzd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ( 1 ... K ) )
292 235 291 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ( 1 ... ( N + K ) ) )
293 elfznn 
 |-  ( ( b ` ( i - 1 ) ) e. ( 1 ... ( N + K ) ) -> ( b ` ( i - 1 ) ) e. NN )
294 292 293 syl 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. NN )
295 294 nnzd 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ZZ )
296 267 295 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) e. ZZ )
297 296 268 zsubcld 
 |-  ( ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) /\ -. i = 1 ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) e. ZZ )
298 226 227 232 297 ifbothda 
 |-  ( ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) /\ -. i = ( K + 1 ) ) -> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) e. ZZ )
299 215 216 225 298 ifbothda 
 |-  ( ( ph /\ b e. B /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. ZZ )
300 299 3expa 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. ZZ )
301 300 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) e. CC )
302 eqeq1 
 |-  ( i = ( K + 1 ) -> ( i = ( K + 1 ) <-> ( K + 1 ) = ( K + 1 ) ) )
303 eqeq1 
 |-  ( i = ( K + 1 ) -> ( i = 1 <-> ( K + 1 ) = 1 ) )
304 fveq2 
 |-  ( i = ( K + 1 ) -> ( b ` i ) = ( b ` ( K + 1 ) ) )
305 fvoveq1 
 |-  ( i = ( K + 1 ) -> ( b ` ( i - 1 ) ) = ( b ` ( ( K + 1 ) - 1 ) ) )
306 304 305 oveq12d 
 |-  ( i = ( K + 1 ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) )
307 306 oveq1d 
 |-  ( i = ( K + 1 ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) )
308 303 307 ifbieq2d 
 |-  ( i = ( K + 1 ) -> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) )
309 302 308 ifbieq2d 
 |-  ( i = ( K + 1 ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) = if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) )
310 214 301 309 fsump1 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) = ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) )
311 eqidd 
 |-  ( ( ph /\ b e. B ) -> ( K + 1 ) = ( K + 1 ) )
312 311 iftrued 
 |-  ( ( ph /\ b e. B ) -> if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) = ( ( N + K ) - ( b ` K ) ) )
313 312 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) = ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + ( ( N + K ) - ( b ` K ) ) ) )
314 elfznn 
 |-  ( i e. ( 1 ... K ) -> i e. NN )
315 314 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. NN )
316 315 nnred 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. RR )
317 34 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> K e. RR )
318 1red 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 e. RR )
319 317 318 readdcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
320 elfzle2 
 |-  ( i e. ( 1 ... K ) -> i <_ K )
321 320 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i <_ K )
322 317 ltp1d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> K < ( K + 1 ) )
323 316 317 319 321 322 lelttrd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i < ( K + 1 ) )
324 316 323 ltned 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i =/= ( K + 1 ) )
325 324 neneqd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> -. i = ( K + 1 ) )
326 325 iffalsed 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) )
327 326 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) = sum_ i e. ( 1 ... K ) if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) )
328 327 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + ( ( N + K ) - ( b ` K ) ) ) = ( sum_ i e. ( 1 ... K ) if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) + ( ( N + K ) - ( b ` K ) ) ) )
329 eqeq1 
 |-  ( ( ( b ` 1 ) - 1 ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) -> ( ( ( b ` 1 ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) <-> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) ) )
330 eqeq1 
 |-  ( ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) -> ( ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) <-> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) ) )
331 eqidd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( ( b ` 1 ) - 1 ) = ( ( b ` 1 ) - 1 ) )
332 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> i = 1 )
333 332 iftrued 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` 1 ) )
334 333 eqcomd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( b ` 1 ) = if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) )
335 334 oveq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( ( b ` 1 ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
336 331 335 eqtrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( ( b ` 1 ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
337 eqidd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) )
338 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> -. i = 1 )
339 338 iffalsed 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` i ) - ( b ` ( i - 1 ) ) ) )
340 339 oveq1d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) )
341 340 eqcomd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
342 337 341 eqtrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
343 329 330 336 342 ifbothda 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
344 343 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) = sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) )
345 344 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) + ( ( N + K ) - ( b ` K ) ) ) = ( sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) + ( ( N + K ) - ( b ` K ) ) ) )
346 fzfid 
 |-  ( ( ph /\ b e. B ) -> ( 1 ... K ) e. Fin )
347 eleq1 
 |-  ( ( b ` 1 ) = if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) -> ( ( b ` 1 ) e. ZZ <-> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. ZZ ) )
348 eleq1 
 |-  ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) -> ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) e. ZZ <-> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. ZZ ) )
349 66 ad2antrr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( b ` 1 ) e. ZZ )
350 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
351 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. ( 1 ... K ) )
352 350 351 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( b ` i ) e. ( 1 ... ( N + K ) ) )
353 265 nnzd 
 |-  ( ( b ` i ) e. ( 1 ... ( N + K ) ) -> ( b ` i ) e. ZZ )
354 352 353 syl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( b ` i ) e. ZZ )
355 354 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` i ) e. ZZ )
356 350 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
357 1zzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 e. ZZ )
358 16 ad2antrr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> K e. ZZ )
359 315 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. ZZ )
360 359 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i e. ZZ )
361 360 357 zsubcld 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ZZ )
362 315 nnge1d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 <_ i )
363 362 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 <_ i )
364 338 273 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i =/= 1 )
365 363 364 jca 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 <_ i /\ i =/= 1 ) )
366 318 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 e. RR )
367 316 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i e. RR )
368 366 367 ltlend 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 < i <-> ( 1 <_ i /\ i =/= 1 ) ) )
369 365 368 mpbird 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 < i )
370 zltlem1 
 |-  ( ( 1 e. ZZ /\ i e. ZZ ) -> ( 1 < i <-> 1 <_ ( i - 1 ) ) )
371 357 360 370 syl2anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 < i <-> 1 <_ ( i - 1 ) ) )
372 369 371 mpbid 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 <_ ( i - 1 ) )
373 316 318 resubcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) e. RR )
374 316 lem1d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) <_ i )
375 373 316 317 374 321 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) <_ K )
376 375 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) <_ K )
377 357 358 361 372 376 elfzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ( 1 ... K ) )
378 356 377 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ( 1 ... ( N + K ) ) )
379 378 293 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. NN )
380 379 nnzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ZZ )
381 355 380 zsubcld 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) e. ZZ )
382 347 348 349 381 ifbothda 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. ZZ )
383 382 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. CC )
384 68 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 e. CC )
385 346 383 384 fsumsub 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( sum_ i e. ( 1 ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - sum_ i e. ( 1 ... K ) 1 ) )
386 id 
 |-  ( i = 1 -> i = 1 )
387 386 iftrued 
 |-  ( i = 1 -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` 1 ) )
388 214 383 387 fsum1p 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) ) )
389 60 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 e. RR )
390 elfzle1 
 |-  ( i e. ( ( 1 + 1 ) ... K ) -> ( 1 + 1 ) <_ i )
391 390 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> ( 1 + 1 ) <_ i )
392 31 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 e. ZZ )
393 elfzelz 
 |-  ( i e. ( ( 1 + 1 ) ... K ) -> i e. ZZ )
394 393 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> i e. ZZ )
395 392 394 280 syl2anc 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> ( 1 < i <-> ( 1 + 1 ) <_ i ) )
396 391 395 mpbird 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 < i )
397 389 396 ltned 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 =/= i )
398 397 necomd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> i =/= 1 )
399 398 neneqd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> -. i = 1 )
400 399 iffalsed 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` i ) - ( b ` ( i - 1 ) ) ) )
401 400 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( ( 1 + 1 ) ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) )
402 401 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) ) = ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) )
403 34 recnd 
 |-  ( ( ph /\ b e. B ) -> K e. CC )
404 403 68 npcand 
 |-  ( ( ph /\ b e. B ) -> ( ( K - 1 ) + 1 ) = K )
405 404 eqcomd 
 |-  ( ( ph /\ b e. B ) -> K = ( ( K - 1 ) + 1 ) )
406 405 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 + 1 ) ... K ) = ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) )
407 406 sumeq1d 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) )
408 407 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) )
409 elfzelz 
 |-  ( i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) -> i e. ZZ )
410 409 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i e. ZZ )
411 410 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i e. CC )
412 1cnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. CC )
413 411 412 npcand 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( i - 1 ) + 1 ) = i )
414 413 eqcomd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i = ( ( i - 1 ) + 1 ) )
415 414 fveq2d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` i ) = ( b ` ( ( i - 1 ) + 1 ) ) )
416 eqidd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` ( i - 1 ) ) = ( b ` ( i - 1 ) ) )
417 415 416 oveq12d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
418 417 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
419 418 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) ) )
420 16 31 zsubcld 
 |-  ( ( ph /\ b e. B ) -> ( K - 1 ) e. ZZ )
421 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
422 1zzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. ZZ )
423 16 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. ZZ )
424 elfznn 
 |-  ( s e. ( 1 ... ( K - 1 ) ) -> s e. NN )
425 424 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. NN )
426 425 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ZZ )
427 426 peano2zd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ZZ )
428 1red 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. RR )
429 425 nnred 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. RR )
430 429 428 readdcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. RR )
431 425 nnge1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ s )
432 429 lep1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( s + 1 ) )
433 428 429 430 431 432 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ ( s + 1 ) )
434 elfzle2 
 |-  ( s e. ( 1 ... ( K - 1 ) ) -> s <_ ( K - 1 ) )
435 434 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( K - 1 ) )
436 34 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. RR )
437 leaddsub 
 |-  ( ( s e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
438 429 428 436 437 syl3anc 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
439 435 438 mpbird 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) <_ K )
440 422 423 427 433 439 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ( 1 ... K ) )
441 421 440 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) )
442 elfznn 
 |-  ( ( b ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( b ` ( s + 1 ) ) e. NN )
443 441 442 syl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. NN )
444 443 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. ZZ )
445 436 428 resubcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
446 436 lem1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) <_ K )
447 429 445 436 435 446 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ K )
448 422 423 426 431 447 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ( 1 ... K ) )
449 421 448 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` s ) e. ( 1 ... ( N + K ) ) )
450 elfznn 
 |-  ( ( b ` s ) e. ( 1 ... ( N + K ) ) -> ( b ` s ) e. NN )
451 450 nnzd 
 |-  ( ( b ` s ) e. ( 1 ... ( N + K ) ) -> ( b ` s ) e. ZZ )
452 449 451 syl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` s ) e. ZZ )
453 444 452 zsubcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) e. ZZ )
454 453 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) e. CC )
455 fvoveq1 
 |-  ( s = ( i - 1 ) -> ( b ` ( s + 1 ) ) = ( b ` ( ( i - 1 ) + 1 ) ) )
456 fveq2 
 |-  ( s = ( i - 1 ) -> ( b ` s ) = ( b ` ( i - 1 ) ) )
457 455 456 oveq12d 
 |-  ( s = ( i - 1 ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
458 31 31 420 454 457 fsumshft 
 |-  ( ( ph /\ b e. B ) -> sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
459 458 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) ) = ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) ) )
460 459 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) ) = ( ( b ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) ) )
461 fvoveq1 
 |-  ( s = i -> ( b ` ( s + 1 ) ) = ( b ` ( i + 1 ) ) )
462 fveq2 
 |-  ( s = i -> ( b ` s ) = ( b ` i ) )
463 461 462 oveq12d 
 |-  ( s = i -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = ( ( b ` ( i + 1 ) ) - ( b ` i ) ) )
464 nfcv 
 |-  F/_ i ( ( b ` ( s + 1 ) ) - ( b ` s ) )
465 nfcv 
 |-  F/_ s ( ( b ` ( i + 1 ) ) - ( b ` i ) )
466 463 464 465 cbvsum 
 |-  sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) )
467 466 a1i 
 |-  ( ( ph /\ b e. B ) -> sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) )
468 467 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) ) = ( ( b ` 1 ) + sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) ) )
469 fveq2 
 |-  ( w = i -> ( b ` w ) = ( b ` i ) )
470 fveq2 
 |-  ( w = ( i + 1 ) -> ( b ` w ) = ( b ` ( i + 1 ) ) )
471 fveq2 
 |-  ( w = 1 -> ( b ` w ) = ( b ` 1 ) )
472 fveq2 
 |-  ( w = ( ( K - 1 ) + 1 ) -> ( b ` w ) = ( b ` ( ( K - 1 ) + 1 ) ) )
473 404 214 eqeltrd 
 |-  ( ( ph /\ b e. B ) -> ( ( K - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
474 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
475 1zzd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. ZZ )
476 16 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> K e. ZZ )
477 elfzelz 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> w e. ZZ )
478 477 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w e. ZZ )
479 elfzle1 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> 1 <_ w )
480 479 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> 1 <_ w )
481 elfzle2 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> w <_ ( ( K - 1 ) + 1 ) )
482 481 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w <_ ( ( K - 1 ) + 1 ) )
483 404 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( ( K - 1 ) + 1 ) = K )
484 482 483 breqtrd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w <_ K )
485 475 476 478 480 484 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w e. ( 1 ... K ) )
486 474 485 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` w ) e. ( 1 ... ( N + K ) ) )
487 elfznn 
 |-  ( ( b ` w ) e. ( 1 ... ( N + K ) ) -> ( b ` w ) e. NN )
488 487 nncnd 
 |-  ( ( b ` w ) e. ( 1 ... ( N + K ) ) -> ( b ` w ) e. CC )
489 486 488 syl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` w ) e. CC )
490 469 470 471 472 420 473 489 telfsum2 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) = ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) )
491 490 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) ) = ( ( b ` 1 ) + ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) ) )
492 73 recnd 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. CC )
493 39 nncnd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. CC )
494 404 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( b ` ( ( K - 1 ) + 1 ) ) = ( b ` K ) )
495 494 eleq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` ( ( K - 1 ) + 1 ) ) e. CC <-> ( b ` K ) e. CC ) )
496 493 495 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( b ` ( ( K - 1 ) + 1 ) ) e. CC )
497 492 496 pncan3d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) ) = ( b ` ( ( K - 1 ) + 1 ) ) )
498 497 494 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) ) = ( b ` K ) )
499 491 498 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) ) = ( b ` K ) )
500 468 499 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) ) = ( b ` K ) )
501 460 500 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
502 419 501 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
503 408 502 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
504 402 503 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) ) = ( b ` K ) )
505 388 504 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
506 fsumconst 
 |-  ( ( ( 1 ... K ) e. Fin /\ 1 e. CC ) -> sum_ i e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
507 346 68 506 syl2anc 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
508 212 nnnn0d 
 |-  ( ( ph /\ b e. B ) -> K e. NN0 )
509 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
510 508 509 syl 
 |-  ( ( ph /\ b e. B ) -> ( # ` ( 1 ... K ) ) = K )
511 510 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = ( K x. 1 ) )
512 403 mulridd 
 |-  ( ( ph /\ b e. B ) -> ( K x. 1 ) = K )
513 511 512 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = K )
514 507 513 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) 1 = K )
515 505 514 oveq12d 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - sum_ i e. ( 1 ... K ) 1 ) = ( ( b ` K ) - K ) )
516 385 515 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( ( b ` K ) - K ) )
517 43 addlidd 
 |-  ( ( ph /\ b e. B ) -> ( 0 + ( b ` K ) ) = ( b ` K ) )
518 517 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) = ( 0 + ( b ` K ) ) )
519 518 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` K ) - K ) = ( ( 0 + ( b ` K ) ) - K ) )
520 516 519 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( ( 0 + ( b ` K ) ) - K ) )
521 0cnd 
 |-  ( ( ph /\ b e. B ) -> 0 e. CC )
522 521 403 43 subsub3d 
 |-  ( ( ph /\ b e. B ) -> ( 0 - ( K - ( b ` K ) ) ) = ( ( 0 + ( b ` K ) ) - K ) )
523 522 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( ( 0 + ( b ` K ) ) - K ) = ( 0 - ( K - ( b ` K ) ) ) )
524 520 523 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( 0 - ( K - ( b ` K ) ) ) )
525 14 zcnd 
 |-  ( ( ph /\ b e. B ) -> N e. CC )
526 525 subidd 
 |-  ( ( ph /\ b e. B ) -> ( N - N ) = 0 )
527 526 eqcomd 
 |-  ( ( ph /\ b e. B ) -> 0 = ( N - N ) )
528 527 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( 0 - ( K - ( b ` K ) ) ) = ( ( N - N ) - ( K - ( b ` K ) ) ) )
529 524 528 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( ( N - N ) - ( K - ( b ` K ) ) ) )
530 403 43 subcld 
 |-  ( ( ph /\ b e. B ) -> ( K - ( b ` K ) ) e. CC )
531 525 525 530 subsub4d 
 |-  ( ( ph /\ b e. B ) -> ( ( N - N ) - ( K - ( b ` K ) ) ) = ( N - ( N + ( K - ( b ` K ) ) ) ) )
532 529 531 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( N - ( N + ( K - ( b ` K ) ) ) ) )
533 525 403 43 addsubassd 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) = ( N + ( K - ( b ` K ) ) ) )
534 533 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( N + ( K - ( b ` K ) ) ) = ( ( N + K ) - ( b ` K ) ) )
535 534 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( N - ( N + ( K - ( b ` K ) ) ) ) = ( N - ( ( N + K ) - ( b ` K ) ) ) )
536 532 535 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( N - ( ( N + K ) - ( b ` K ) ) ) )
537 1zzd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 e. ZZ )
538 382 537 zsubcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) e. ZZ )
539 346 538 fsumzcl 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) e. ZZ )
540 539 zcnd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) e. CC )
541 54 nn0cnd 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) e. CC )
542 540 541 525 addlsub 
 |-  ( ( ph /\ b e. B ) -> ( ( sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) + ( ( N + K ) - ( b ` K ) ) ) = N <-> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( N - ( ( N + K ) - ( b ` K ) ) ) ) )
543 536 542 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) + ( ( N + K ) - ( b ` K ) ) ) = N )
544 345 543 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) + ( ( N + K ) - ( b ` K ) ) ) = N )
545 328 544 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + ( ( N + K ) - ( b ` K ) ) ) = N )
546 313 545 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( sum_ i e. ( 1 ... K ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) + if ( ( K + 1 ) = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( ( K + 1 ) = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` ( K + 1 ) ) - ( b ` ( ( K + 1 ) - 1 ) ) ) - 1 ) ) ) ) = N )
547 310 546 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K + 1 ) ) if ( i = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( i = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` i ) - ( b ` ( i - 1 ) ) ) - 1 ) ) ) = N )
548 211 547 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = N )
549 193 548 jca 
 |-  ( ( ph /\ b e. B ) -> ( ( 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 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = N ) )
550 ovex 
 |-  ( 1 ... ( K + 1 ) ) e. _V
551 550 mptex 
 |-  ( 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 ) ) ) ) e. _V
552 feq1 
 |-  ( g = ( 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 ) ) ) ) -> ( g : ( 1 ... ( K + 1 ) ) --> NN0 <-> ( 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 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 ) )
553 simpl 
 |-  ( ( g = ( 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 ) ) ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> g = ( 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 ) ) ) ) )
554 553 fveq1d 
 |-  ( ( g = ( 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 ) ) ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( g ` i ) = ( ( 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 ) ) ) ) ` i ) )
555 554 sumeq2dv 
 |-  ( g = ( 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 ) ) ) ) -> 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 ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) )
556 555 eqeq1d 
 |-  ( g = ( 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 ) ) ) ) -> ( 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 ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ` i ) = N ) )
557 552 556 anbi12d 
 |-  ( g = ( 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 ) ) ) ) -> ( ( 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 ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = N ) ) )
558 551 557 elab 
 |-  ( ( 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 ) ) ) ) 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 ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 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 ) ) ) ) ` i ) = N ) )
559 549 558 sylibr 
 |-  ( ( ph /\ b e. B ) -> ( 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 ) ) ) ) e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
560 4 a1i 
 |-  ( ( ph /\ b e. B ) -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
561 559 560 eleqtrrd 
 |-  ( ( ph /\ b e. B ) -> ( 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 ) ) ) ) e. A )
562 10 561 eqeltrrd 
 |-  ( ( ph /\ 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 ) ) ) ) ) e. A )
563 562 3 fmptd 
 |-  ( ph -> G : B --> A )