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