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 14 zcnd 
 |-  ( ( ph /\ b e. B ) -> N e. CC )
347 54 nn0cnd 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) e. CC )
348 fzfid 
 |-  ( ( ph /\ b e. B ) -> ( 1 ... K ) e. Fin )
349 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 ) )
350 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 ) )
351 66 ad2antrr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ i = 1 ) -> ( b ` 1 ) e. ZZ )
352 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
353 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. ( 1 ... K ) )
354 352 353 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( b ` i ) e. ( 1 ... ( N + K ) ) )
355 265 nnzd 
 |-  ( ( b ` i ) e. ( 1 ... ( N + K ) ) -> ( b ` i ) e. ZZ )
356 354 355 syl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( b ` i ) e. ZZ )
357 356 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` i ) e. ZZ )
358 352 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
359 1zzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 e. ZZ )
360 16 ad2antrr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> K e. ZZ )
361 315 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. ZZ )
362 361 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i e. ZZ )
363 362 359 zsubcld 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ZZ )
364 315 nnge1d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 <_ i )
365 364 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 <_ i )
366 338 273 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i =/= 1 )
367 365 366 jca 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 <_ i /\ i =/= 1 ) )
368 318 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 e. RR )
369 316 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> i e. RR )
370 368 369 ltlend 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 < i <-> ( 1 <_ i /\ i =/= 1 ) ) )
371 367 370 mpbird 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 < i )
372 zltlem1 
 |-  ( ( 1 e. ZZ /\ i e. ZZ ) -> ( 1 < i <-> 1 <_ ( i - 1 ) ) )
373 359 362 372 syl2anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( 1 < i <-> 1 <_ ( i - 1 ) ) )
374 371 373 mpbid 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> 1 <_ ( i - 1 ) )
375 316 318 resubcld 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) e. RR )
376 316 lem1d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) <_ i )
377 375 316 317 376 321 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( i - 1 ) <_ K )
378 377 adantr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) <_ K )
379 359 360 363 374 378 elfzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( i - 1 ) e. ( 1 ... K ) )
380 358 379 ffvelcdmd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ( 1 ... ( N + K ) ) )
381 380 293 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. NN )
382 381 nnzd 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( b ` ( i - 1 ) ) e. ZZ )
383 357 382 zsubcld 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ -. i = 1 ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) e. ZZ )
384 349 350 351 383 ifbothda 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. ZZ )
385 384 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) e. CC )
386 68 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> 1 e. CC )
387 348 385 386 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 ) )
388 id 
 |-  ( i = 1 -> i = 1 )
389 388 iftrued 
 |-  ( i = 1 -> if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` 1 ) )
390 214 385 389 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 ) ) ) ) ) )
391 60 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 e. RR )
392 elfzle1 
 |-  ( i e. ( ( 1 + 1 ) ... K ) -> ( 1 + 1 ) <_ i )
393 392 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> ( 1 + 1 ) <_ i )
394 31 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 e. ZZ )
395 elfzelz 
 |-  ( i e. ( ( 1 + 1 ) ... K ) -> i e. ZZ )
396 395 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> i e. ZZ )
397 394 396 280 syl2anc 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> ( 1 < i <-> ( 1 + 1 ) <_ i ) )
398 393 397 mpbird 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 < i )
399 391 398 ltned 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> 1 =/= i )
400 399 necomd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> i =/= 1 )
401 400 neneqd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... K ) ) -> -. i = 1 )
402 401 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 ) ) ) )
403 402 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 ) ) ) )
404 403 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 ) ) ) ) )
405 34 recnd 
 |-  ( ( ph /\ b e. B ) -> K e. CC )
406 405 68 npcand 
 |-  ( ( ph /\ b e. B ) -> ( ( K - 1 ) + 1 ) = K )
407 406 eqcomd 
 |-  ( ( ph /\ b e. B ) -> K = ( ( K - 1 ) + 1 ) )
408 407 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 + 1 ) ... K ) = ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) )
409 408 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 ) ) ) )
410 409 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 ) ) ) ) )
411 elfzelz 
 |-  ( i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) -> i e. ZZ )
412 411 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i e. ZZ )
413 412 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i e. CC )
414 1cnd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. CC )
415 413 414 npcand 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( i - 1 ) + 1 ) = i )
416 415 eqcomd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> i = ( ( i - 1 ) + 1 ) )
417 416 fveq2d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` i ) = ( b ` ( ( i - 1 ) + 1 ) ) )
418 eqidd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` ( i - 1 ) ) = ( b ` ( i - 1 ) ) )
419 417 418 oveq12d 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ) -> ( ( b ` i ) - ( b ` ( i - 1 ) ) ) = ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
420 419 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 ) ) ) )
421 420 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 ) ) ) ) )
422 16 31 zsubcld 
 |-  ( ( ph /\ b e. B ) -> ( K - 1 ) e. ZZ )
423 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
424 1zzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. ZZ )
425 16 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. ZZ )
426 elfznn 
 |-  ( s e. ( 1 ... ( K - 1 ) ) -> s e. NN )
427 426 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. NN )
428 427 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ZZ )
429 428 peano2zd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ZZ )
430 1red 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 e. RR )
431 427 nnred 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. RR )
432 431 430 readdcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. RR )
433 427 nnge1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ s )
434 431 lep1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( s + 1 ) )
435 430 431 432 433 434 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> 1 <_ ( s + 1 ) )
436 elfzle2 
 |-  ( s e. ( 1 ... ( K - 1 ) ) -> s <_ ( K - 1 ) )
437 436 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ ( K - 1 ) )
438 34 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> K e. RR )
439 leaddsub 
 |-  ( ( s e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
440 431 430 438 439 syl3anc 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( s + 1 ) <_ K <-> s <_ ( K - 1 ) ) )
441 437 440 mpbird 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) <_ K )
442 424 425 429 435 441 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( s + 1 ) e. ( 1 ... K ) )
443 423 442 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) )
444 elfznn 
 |-  ( ( b ` ( s + 1 ) ) e. ( 1 ... ( N + K ) ) -> ( b ` ( s + 1 ) ) e. NN )
445 443 444 syl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. NN )
446 445 nnzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` ( s + 1 ) ) e. ZZ )
447 438 430 resubcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
448 438 lem1d 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( K - 1 ) <_ K )
449 431 447 438 437 448 letrd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s <_ K )
450 424 425 428 433 449 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> s e. ( 1 ... K ) )
451 423 450 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` s ) e. ( 1 ... ( N + K ) ) )
452 elfznn 
 |-  ( ( b ` s ) e. ( 1 ... ( N + K ) ) -> ( b ` s ) e. NN )
453 452 nnzd 
 |-  ( ( b ` s ) e. ( 1 ... ( N + K ) ) -> ( b ` s ) e. ZZ )
454 451 453 syl 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( b ` s ) e. ZZ )
455 446 454 zsubcld 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) e. ZZ )
456 455 zcnd 
 |-  ( ( ( ph /\ b e. B ) /\ s e. ( 1 ... ( K - 1 ) ) ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) e. CC )
457 fvoveq1 
 |-  ( s = ( i - 1 ) -> ( b ` ( s + 1 ) ) = ( b ` ( ( i - 1 ) + 1 ) ) )
458 fveq2 
 |-  ( s = ( i - 1 ) -> ( b ` s ) = ( b ` ( i - 1 ) ) )
459 457 458 oveq12d 
 |-  ( s = ( i - 1 ) -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) )
460 31 31 422 456 459 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 ) ) ) )
461 460 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 ) ) ) ) )
462 461 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 ) ) ) )
463 fvoveq1 
 |-  ( s = i -> ( b ` ( s + 1 ) ) = ( b ` ( i + 1 ) ) )
464 fveq2 
 |-  ( s = i -> ( b ` s ) = ( b ` i ) )
465 463 464 oveq12d 
 |-  ( s = i -> ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = ( ( b ` ( i + 1 ) ) - ( b ` i ) ) )
466 nfcv 
 |-  F/_ i ( ( b ` ( s + 1 ) ) - ( b ` s ) )
467 nfcv 
 |-  F/_ s ( ( b ` ( i + 1 ) ) - ( b ` i ) )
468 465 466 467 cbvsum 
 |-  sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) = sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) )
469 468 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 ) ) )
470 469 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 ) ) ) )
471 fveq2 
 |-  ( w = i -> ( b ` w ) = ( b ` i ) )
472 fveq2 
 |-  ( w = ( i + 1 ) -> ( b ` w ) = ( b ` ( i + 1 ) ) )
473 fveq2 
 |-  ( w = 1 -> ( b ` w ) = ( b ` 1 ) )
474 fveq2 
 |-  ( w = ( ( K - 1 ) + 1 ) -> ( b ` w ) = ( b ` ( ( K - 1 ) + 1 ) ) )
475 406 214 eqeltrd 
 |-  ( ( ph /\ b e. B ) -> ( ( K - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
476 30 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> b : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
477 1zzd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> 1 e. ZZ )
478 16 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> K e. ZZ )
479 elfzelz 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> w e. ZZ )
480 479 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w e. ZZ )
481 elfzle1 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> 1 <_ w )
482 481 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> 1 <_ w )
483 elfzle2 
 |-  ( w e. ( 1 ... ( ( K - 1 ) + 1 ) ) -> w <_ ( ( K - 1 ) + 1 ) )
484 483 adantl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w <_ ( ( K - 1 ) + 1 ) )
485 406 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( ( K - 1 ) + 1 ) = K )
486 484 485 breqtrd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w <_ K )
487 477 478 480 482 486 elfzd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> w e. ( 1 ... K ) )
488 476 487 ffvelcdmd 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` w ) e. ( 1 ... ( N + K ) ) )
489 elfznn 
 |-  ( ( b ` w ) e. ( 1 ... ( N + K ) ) -> ( b ` w ) e. NN )
490 489 nncnd 
 |-  ( ( b ` w ) e. ( 1 ... ( N + K ) ) -> ( b ` w ) e. CC )
491 488 490 syl 
 |-  ( ( ( ph /\ b e. B ) /\ w e. ( 1 ... ( ( K - 1 ) + 1 ) ) ) -> ( b ` w ) e. CC )
492 471 472 473 474 422 475 491 telfsum2 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) = ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) )
493 492 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 ) ) ) )
494 73 recnd 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. CC )
495 39 nncnd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) e. CC )
496 406 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( b ` ( ( K - 1 ) + 1 ) ) = ( b ` K ) )
497 496 eleq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` ( ( K - 1 ) + 1 ) ) e. CC <-> ( b ` K ) e. CC ) )
498 495 497 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( b ` ( ( K - 1 ) + 1 ) ) e. CC )
499 494 498 pncan3d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) ) = ( b ` ( ( K - 1 ) + 1 ) ) )
500 499 496 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + ( ( b ` ( ( K - 1 ) + 1 ) ) - ( b ` 1 ) ) ) = ( b ` K ) )
501 493 500 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( 1 ... ( K - 1 ) ) ( ( b ` ( i + 1 ) ) - ( b ` i ) ) ) = ( b ` K ) )
502 470 501 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ s e. ( 1 ... ( K - 1 ) ) ( ( b ` ( s + 1 ) ) - ( b ` s ) ) ) = ( b ` K ) )
503 462 502 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` ( ( i - 1 ) + 1 ) ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
504 421 503 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... ( ( K - 1 ) + 1 ) ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
505 410 504 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) + sum_ i e. ( ( 1 + 1 ) ... K ) ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
506 404 505 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 ) )
507 390 506 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) = ( b ` K ) )
508 fsumconst 
 |-  ( ( ( 1 ... K ) e. Fin /\ 1 e. CC ) -> sum_ i e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
509 348 68 508 syl2anc 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) 1 = ( ( # ` ( 1 ... K ) ) x. 1 ) )
510 212 nnnn0d 
 |-  ( ( ph /\ b e. B ) -> K e. NN0 )
511 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
512 510 511 syl 
 |-  ( ( ph /\ b e. B ) -> ( # ` ( 1 ... K ) ) = K )
513 512 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = ( K x. 1 ) )
514 405 mulridd 
 |-  ( ( ph /\ b e. B ) -> ( K x. 1 ) = K )
515 513 514 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( # ` ( 1 ... K ) ) x. 1 ) = K )
516 509 515 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) 1 = K )
517 507 516 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 ) )
518 387 517 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( if ( i = 1 , ( b ` 1 ) , ( ( b ` i ) - ( b ` ( i - 1 ) ) ) ) - 1 ) = ( ( b ` K ) - K ) )
519 43 addlidd 
 |-  ( ( ph /\ b e. B ) -> ( 0 + ( b ` K ) ) = ( b ` K ) )
520 519 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( b ` K ) = ( 0 + ( b ` K ) ) )
521 520 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` K ) - K ) = ( ( 0 + ( b ` K ) ) - K ) )
522 518 521 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 ) )
523 0cnd 
 |-  ( ( ph /\ b e. B ) -> 0 e. CC )
524 523 405 43 subsub3d 
 |-  ( ( ph /\ b e. B ) -> ( 0 - ( K - ( b ` K ) ) ) = ( ( 0 + ( b ` K ) ) - K ) )
525 524 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( ( 0 + ( b ` K ) ) - K ) = ( 0 - ( K - ( b ` K ) ) ) )
526 522 525 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 ) ) ) )
527 346 subidd 
 |-  ( ( ph /\ b e. B ) -> ( N - N ) = 0 )
528 527 eqcomd 
 |-  ( ( ph /\ b e. B ) -> 0 = ( N - N ) )
529 528 oveq1d 
 |-  ( ( ph /\ b e. B ) -> ( 0 - ( K - ( b ` K ) ) ) = ( ( N - N ) - ( K - ( b ` K ) ) ) )
530 526 529 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 ) ) ) )
531 405 43 subcld 
 |-  ( ( ph /\ b e. B ) -> ( K - ( b ` K ) ) e. CC )
532 346 346 531 subsub4d 
 |-  ( ( ph /\ b e. B ) -> ( ( N - N ) - ( K - ( b ` K ) ) ) = ( N - ( N + ( K - ( b ` K ) ) ) ) )
533 530 532 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 ) ) ) ) )
534 346 405 43 addsubassd 
 |-  ( ( ph /\ b e. B ) -> ( ( N + K ) - ( b ` K ) ) = ( N + ( K - ( b ` K ) ) ) )
535 534 eqcomd 
 |-  ( ( ph /\ b e. B ) -> ( N + ( K - ( b ` K ) ) ) = ( ( N + K ) - ( b ` K ) ) )
536 535 oveq2d 
 |-  ( ( ph /\ b e. B ) -> ( N - ( N + ( K - ( b ` K ) ) ) ) = ( N - ( ( N + K ) - ( b ` K ) ) ) )
537 533 536 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 ) ) ) )
538 346 347 537 mvrrsubd 
 |-  ( ( 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 )
539 345 538 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 )
540 328 539 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 )
541 313 540 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 )
542 310 541 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 )
543 211 542 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 )
544 193 543 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 ) )
545 ovex 
 |-  ( 1 ... ( K + 1 ) ) e. _V
546 545 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
547 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 ) )
548 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 ) ) ) ) )
549 548 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 ) )
550 549 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 ) )
551 550 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 ) )
552 547 551 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 ) ) )
553 546 552 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 ) )
554 544 553 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 ) } )
555 4 a1i 
 |-  ( ( ph /\ b e. B ) -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
556 554 555 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 )
557 10 556 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 )
558 557 3 fmptd 
 |-  ( ph -> G : B --> A )