Metamath Proof Explorer

Theorem sticksstones12

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

Ref Expression
Hypotheses sticksstones12.1 
|- ( ph -> N e. NN0 )
sticksstones12.2 
|- ( ph -> K e. NN )
sticksstones12.3 
|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
sticksstones12.4 
|- G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
sticksstones12.5 
|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
sticksstones12.6 
|- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion sticksstones12 
|- ( ph -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 sticksstones12.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones12.2 
 |-  ( ph -> K e. NN )
3 sticksstones12.3 
 |-  F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
4 sticksstones12.4 
 |-  G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
5 sticksstones12.5 
 |-  A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
6 sticksstones12.6 
 |-  B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
7 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
8 1 7 3 5 6 sticksstones8 
 |-  ( ph -> F : A --> B )
9 1 2 4 5 6 sticksstones10 
 |-  ( ph -> G : B --> A )
10 4 a1i 
 |-  ( ph -> 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 ) ) ) ) ) ) )
11 0red 
 |-  ( ph -> 0 e. RR )
12 2 nngt0d 
 |-  ( ph -> 0 < K )
13 11 12 ltned 
 |-  ( ph -> 0 =/= K )
14 13 necomd 
 |-  ( ph -> K =/= 0 )
15 14 neneqd 
 |-  ( ph -> -. K = 0 )
16 15 iffalsed 
 |-  ( ph -> 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 ) ) ) ) )
17 16 adantr 
 |-  ( ( 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 ) ) ) ) )
18 17 mpteq2dva 
 |-  ( 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 ) ) ) ) ) ) = ( 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 ) ) ) ) ) )
19 10 18 eqtrd 
 |-  ( ph -> G = ( 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 ) ) ) ) ) )
20 19 adantr 
 |-  ( ( ph /\ c e. A ) -> G = ( 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 ) ) ) ) ) )
21 fveq1 
 |-  ( b = ( F ` c ) -> ( b ` K ) = ( ( F ` c ) ` K ) )
22 21 oveq2d 
 |-  ( b = ( F ` c ) -> ( ( N + K ) - ( b ` K ) ) = ( ( N + K ) - ( ( F ` c ) ` K ) ) )
23 fveq1 
 |-  ( b = ( F ` c ) -> ( b ` 1 ) = ( ( F ` c ) ` 1 ) )
24 23 oveq1d 
 |-  ( b = ( F ` c ) -> ( ( b ` 1 ) - 1 ) = ( ( ( F ` c ) ` 1 ) - 1 ) )
25 fveq1 
 |-  ( b = ( F ` c ) -> ( b ` k ) = ( ( F ` c ) ` k ) )
26 fveq1 
 |-  ( b = ( F ` c ) -> ( b ` ( k - 1 ) ) = ( ( F ` c ) ` ( k - 1 ) ) )
27 25 26 oveq12d 
 |-  ( b = ( F ` c ) -> ( ( b ` k ) - ( b ` ( k - 1 ) ) ) = ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) )
28 27 oveq1d 
 |-  ( b = ( F ` c ) -> ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) = ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) )
29 24 28 ifeq12d 
 |-  ( b = ( F ` c ) -> if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) = if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) )
30 22 29 ifeq12d 
 |-  ( b = ( F ` c ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) )
31 30 adantr 
 |-  ( ( b = ( F ` c ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) = if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) )
32 31 mpteq2dva 
 |-  ( b = ( F ` c ) -> ( 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 ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) )
33 32 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ b = ( F ` c ) ) -> ( 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 ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) )
34 8 ffvelrnda 
 |-  ( ( ph /\ c e. A ) -> ( F ` c ) e. B )
35 fzfid 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... ( K + 1 ) ) e. Fin )
36 35 mptexd 
 |-  ( ( ph /\ c e. A ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) e. _V )
37 20 33 34 36 fvmptd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) )
38 3 a1i 
 |-  ( ( ph /\ c e. A ) -> F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) ) )
39 simpllr 
 |-  ( ( ( ( ( ph /\ c e. A ) /\ a = c ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> a = c )
40 39 fveq1d 
 |-  ( ( ( ( ( ph /\ c e. A ) /\ a = c ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( a ` l ) = ( c ` l ) )
41 40 sumeq2dv 
 |-  ( ( ( ( ph /\ c e. A ) /\ a = c ) /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) ( a ` l ) = sum_ l e. ( 1 ... j ) ( c ` l ) )
42 41 oveq2d 
 |-  ( ( ( ( ph /\ c e. A ) /\ a = c ) /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) = ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) )
43 42 mpteq2dva 
 |-  ( ( ( ph /\ c e. A ) /\ a = c ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
44 simpr 
 |-  ( ( ph /\ c e. A ) -> c e. A )
45 fzfid 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... K ) e. Fin )
46 45 mptexd 
 |-  ( ( ph /\ c e. A ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) e. _V )
47 38 43 44 46 fvmptd 
 |-  ( ( ph /\ c e. A ) -> ( F ` c ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
48 simpr 
 |-  ( ( ( ph /\ c e. A ) /\ j = K ) -> j = K )
49 48 oveq2d 
 |-  ( ( ( ph /\ c e. A ) /\ j = K ) -> ( 1 ... j ) = ( 1 ... K ) )
50 49 sumeq1d 
 |-  ( ( ( ph /\ c e. A ) /\ j = K ) -> sum_ l e. ( 1 ... j ) ( c ` l ) = sum_ l e. ( 1 ... K ) ( c ` l ) )
51 48 50 oveq12d 
 |-  ( ( ( ph /\ c e. A ) /\ j = K ) -> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) = ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) )
52 1zzd 
 |-  ( ph -> 1 e. ZZ )
53 7 nn0zd 
 |-  ( ph -> K e. ZZ )
54 2 nnge1d 
 |-  ( ph -> 1 <_ K )
55 2 nnred 
 |-  ( ph -> K e. RR )
56 55 leidd 
 |-  ( ph -> K <_ K )
57 52 53 53 54 56 elfzd 
 |-  ( ph -> K e. ( 1 ... K ) )
58 57 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. ( 1 ... K ) )
59 ovexd 
 |-  ( ( ph /\ c e. A ) -> ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) e. _V )
60 47 51 58 59 fvmptd 
 |-  ( ( ph /\ c e. A ) -> ( ( F ` c ) ` K ) = ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) )
61 60 oveq2d 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( ( N + K ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) )
62 1 nn0cnd 
 |-  ( ph -> N e. CC )
63 62 adantr 
 |-  ( ( ph /\ c e. A ) -> N e. CC )
64 55 recnd 
 |-  ( ph -> K e. CC )
65 64 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. CC )
66 63 65 addcomd 
 |-  ( ( ph /\ c e. A ) -> ( N + K ) = ( K + N ) )
67 66 oveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( ( K + N ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) )
68 1zzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> 1 e. ZZ )
69 53 ad2antrr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> K e. ZZ )
70 69 peano2zd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> ( K + 1 ) e. ZZ )
71 elfzelz 
 |-  ( l e. ( 1 ... K ) -> l e. ZZ )
72 71 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> l e. ZZ )
73 elfzle1 
 |-  ( l e. ( 1 ... K ) -> 1 <_ l )
74 73 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> 1 <_ l )
75 72 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> l e. RR )
76 55 ad2antrr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> K e. RR )
77 70 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> ( K + 1 ) e. RR )
78 elfzle2 
 |-  ( l e. ( 1 ... K ) -> l <_ K )
79 78 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> l <_ K )
80 76 lep1d 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> K <_ ( K + 1 ) )
81 75 76 77 79 80 letrd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> l <_ ( K + 1 ) )
82 68 70 72 74 81 elfzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> l e. ( 1 ... ( K + 1 ) ) )
83 5 eleq2i 
 |-  ( c e. A <-> c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
84 83 biimpi 
 |-  ( c e. A -> c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
85 84 adantl 
 |-  ( ( ph /\ c e. A ) -> c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
86 vex 
 |-  c e. _V
87 feq1 
 |-  ( g = c -> ( g : ( 1 ... ( K + 1 ) ) --> NN0 <-> c : ( 1 ... ( K + 1 ) ) --> NN0 ) )
88 simpl 
 |-  ( ( g = c /\ i e. ( 1 ... ( K + 1 ) ) ) -> g = c )
89 88 fveq1d 
 |-  ( ( g = c /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( g ` i ) = ( c ` i ) )
90 89 sumeq2dv 
 |-  ( g = c -> sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) )
91 90 eqeq1d 
 |-  ( g = c -> ( sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N <-> sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) )
92 87 91 anbi12d 
 |-  ( g = c -> ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) <-> ( c : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) ) )
93 86 92 elab 
 |-  ( c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( c : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) )
94 93 a1i 
 |-  ( ( ph /\ c e. A ) -> ( c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( c : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) ) )
95 94 biimpd 
 |-  ( ( ph /\ c e. A ) -> ( c e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } -> ( c : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) ) )
96 85 95 mpd 
 |-  ( ( ph /\ c e. A ) -> ( c : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N ) )
97 96 simpld 
 |-  ( ( ph /\ c e. A ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
98 97 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
99 98 ffvelrnda 
 |-  ( ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
100 82 99 mpdan 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... K ) ) -> ( c ` l ) e. NN0 )
101 45 100 fsumnn0cl 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... K ) ( c ` l ) e. NN0 )
102 101 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... K ) ( c ` l ) e. CC )
103 65 63 102 pnpcand 
 |-  ( ( ph /\ c e. A ) -> ( ( K + N ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( N - sum_ l e. ( 1 ... K ) ( c ` l ) ) )
104 eqid 
 |-  1 = 1
105 1p0e1 
 |-  ( 1 + 0 ) = 1
106 104 105 eqtr4i 
 |-  1 = ( 1 + 0 )
107 106 a1i 
 |-  ( ph -> 1 = ( 1 + 0 ) )
108 1red 
 |-  ( ph -> 1 e. RR )
109 0le1 
 |-  0 <_ 1
110 109 a1i 
 |-  ( ph -> 0 <_ 1 )
111 108 11 55 108 54 110 le2addd 
 |-  ( ph -> ( 1 + 0 ) <_ ( K + 1 ) )
112 107 111 eqbrtrd 
 |-  ( ph -> 1 <_ ( K + 1 ) )
113 53 peano2zd 
 |-  ( ph -> ( K + 1 ) e. ZZ )
114 eluz 
 |-  ( ( 1 e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( ( K + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( K + 1 ) ) )
115 52 113 114 syl2anc 
 |-  ( ph -> ( ( K + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( K + 1 ) ) )
116 112 115 mpbird 
 |-  ( ph -> ( K + 1 ) e. ( ZZ>= ` 1 ) )
117 116 adantr 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) e. ( ZZ>= ` 1 ) )
118 97 ffvelrnda 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
119 118 nn0cnd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. CC )
120 fveq2 
 |-  ( l = ( K + 1 ) -> ( c ` l ) = ( c ` ( K + 1 ) ) )
121 117 119 120 fsumm1 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = ( sum_ l e. ( 1 ... ( ( K + 1 ) - 1 ) ) ( c ` l ) + ( c ` ( K + 1 ) ) ) )
122 1cnd 
 |-  ( ( ph /\ c e. A ) -> 1 e. CC )
123 65 122 pncand 
 |-  ( ( ph /\ c e. A ) -> ( ( K + 1 ) - 1 ) = K )
124 123 oveq2d 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... ( ( K + 1 ) - 1 ) ) = ( 1 ... K ) )
125 124 sumeq1d 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( ( K + 1 ) - 1 ) ) ( c ` l ) = sum_ l e. ( 1 ... K ) ( c ` l ) )
126 125 oveq1d 
 |-  ( ( ph /\ c e. A ) -> ( sum_ l e. ( 1 ... ( ( K + 1 ) - 1 ) ) ( c ` l ) + ( c ` ( K + 1 ) ) ) = ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) )
127 121 126 eqtrd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) )
128 127 eqcomd 
 |-  ( ( ph /\ c e. A ) -> ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) = sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) )
129 fveq2 
 |-  ( l = i -> ( c ` l ) = ( c ` i ) )
130 nfcv 
 |-  F/_ i ( 1 ... ( K + 1 ) )
131 nfcv 
 |-  F/_ l ( 1 ... ( K + 1 ) )
132 nfcv 
 |-  F/_ i ( c ` l )
133 nfcv 
 |-  F/_ l ( c ` i )
134 129 130 131 132 133 cbvsum 
 |-  sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i )
135 134 a1i 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) )
136 96 simprd 
 |-  ( ( ph /\ c e. A ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N )
137 135 136 eqtrd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = N )
138 128 137 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) = N )
139 1zzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ZZ )
140 53 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. ZZ )
141 140 peano2zd 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) e. ZZ )
142 1e0p1 
 |-  1 = ( 0 + 1 )
143 142 a1i 
 |-  ( ( ph /\ c e. A ) -> 1 = ( 0 + 1 ) )
144 0red 
 |-  ( ( ph /\ c e. A ) -> 0 e. RR )
145 55 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. RR )
146 1red 
 |-  ( ( ph /\ c e. A ) -> 1 e. RR )
147 11 55 12 ltled 
 |-  ( ph -> 0 <_ K )
148 147 adantr 
 |-  ( ( ph /\ c e. A ) -> 0 <_ K )
149 144 145 146 148 leadd1dd 
 |-  ( ( ph /\ c e. A ) -> ( 0 + 1 ) <_ ( K + 1 ) )
150 143 149 eqbrtrd 
 |-  ( ( ph /\ c e. A ) -> 1 <_ ( K + 1 ) )
151 55 55 108 56 leadd1dd 
 |-  ( ph -> ( K + 1 ) <_ ( K + 1 ) )
152 151 adantr 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) <_ ( K + 1 ) )
153 139 141 141 150 152 elfzd 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) e. ( 1 ... ( K + 1 ) ) )
154 97 153 ffvelrnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` ( K + 1 ) ) e. NN0 )
155 154 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` ( K + 1 ) ) e. CC )
156 63 102 155 subaddd 
 |-  ( ( ph /\ c e. A ) -> ( ( N - sum_ l e. ( 1 ... K ) ( c ` l ) ) = ( c ` ( K + 1 ) ) <-> ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) = N ) )
157 138 156 mpbird 
 |-  ( ( ph /\ c e. A ) -> ( N - sum_ l e. ( 1 ... K ) ( c ` l ) ) = ( c ` ( K + 1 ) ) )
158 103 157 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( K + N ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( c ` ( K + 1 ) ) )
159 67 158 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( c ` ( K + 1 ) ) )
160 61 159 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
161 160 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
162 161 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
163 simpr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> k = ( K + 1 ) )
164 163 fveq2d 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( c ` k ) = ( c ` ( K + 1 ) ) )
165 164 eqcomd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( c ` ( K + 1 ) ) = ( c ` k ) )
166 162 165 eqtrd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` k ) )
167 47 fveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( F ` c ) ` 1 ) = ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) )
168 167 oveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) - 1 ) )
169 eqidd 
 |-  ( ( ph /\ c e. A ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
170 simpr 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> j = 1 )
171 170 oveq2d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> ( 1 ... j ) = ( 1 ... 1 ) )
172 171 sumeq1d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> sum_ l e. ( 1 ... j ) ( c ` l ) = sum_ l e. ( 1 ... 1 ) ( c ` l ) )
173 170 172 oveq12d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) = ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) )
174 146 leidd 
 |-  ( ( ph /\ c e. A ) -> 1 <_ 1 )
175 54 adantr 
 |-  ( ( ph /\ c e. A ) -> 1 <_ K )
176 139 140 139 174 175 elfzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ( 1 ... K ) )
177 ovexd 
 |-  ( ( ph /\ c e. A ) -> ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) e. _V )
178 169 173 176 177 fvmptd 
 |-  ( ( ph /\ c e. A ) -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) = ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) )
179 178 oveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) - 1 ) = ( ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) - 1 ) )
180 fzfid 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... 1 ) e. Fin )
181 1zzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 e. ZZ )
182 140 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> K e. ZZ )
183 182 peano2zd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( K + 1 ) e. ZZ )
184 elfzelz 
 |-  ( l e. ( 1 ... 1 ) -> l e. ZZ )
185 184 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. ZZ )
186 elfzle1 
 |-  ( l e. ( 1 ... 1 ) -> 1 <_ l )
187 186 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 <_ l )
188 185 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. RR )
189 0red 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 0 e. RR )
190 1red 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 e. RR )
191 189 190 readdcld 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( 0 + 1 ) e. RR )
192 183 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( K + 1 ) e. RR )
193 elfzle2 
 |-  ( l e. ( 1 ... 1 ) -> l <_ 1 )
194 193 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ 1 )
195 142 a1i 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 = ( 0 + 1 ) )
196 194 195 breqtrd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ ( 0 + 1 ) )
197 149 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( 0 + 1 ) <_ ( K + 1 ) )
198 188 191 192 196 197 letrd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ ( K + 1 ) )
199 181 183 185 187 198 elfzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. ( 1 ... ( K + 1 ) ) )
200 118 adantlr 
 |-  ( ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
201 199 200 mpdan 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( c ` l ) e. NN0 )
202 180 201 fsumnn0cl 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) e. NN0 )
203 202 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) e. CC )
204 122 203 pncan2d 
 |-  ( ( ph /\ c e. A ) -> ( ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) - 1 ) = sum_ l e. ( 1 ... 1 ) ( c ` l ) )
205 139 141 139 174 150 elfzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ( 1 ... ( K + 1 ) ) )
206 97 205 ffvelrnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. NN0 )
207 206 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. CC )
208 fveq2 
 |-  ( l = 1 -> ( c ` l ) = ( c ` 1 ) )
209 208 fsum1 
 |-  ( ( 1 e. ZZ /\ ( c ` 1 ) e. CC ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) = ( c ` 1 ) )
210 139 207 209 syl2anc 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) = ( c ` 1 ) )
211 204 210 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) - 1 ) = ( c ` 1 ) )
212 179 211 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) - 1 ) = ( c ` 1 ) )
213 168 212 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
214 213 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
215 214 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
216 215 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
217 simpr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> k = 1 )
218 217 fveq2d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( c ` k ) = ( c ` 1 ) )
219 218 eqcomd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( c ` 1 ) = ( c ` k ) )
220 216 219 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` k ) )
221 3 a1i 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) ) )
222 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ a = c ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> a = c )
223 222 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ a = c ) /\ j e. ( 1 ... K ) ) /\ l e. ( 1 ... j ) ) -> ( a ` l ) = ( c ` l ) )
224 223 sumeq2dv 
 |-  ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ a = c ) /\ j e. ( 1 ... K ) ) -> sum_ l e. ( 1 ... j ) ( a ` l ) = sum_ l e. ( 1 ... j ) ( c ` l ) )
225 224 oveq2d 
 |-  ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ a = c ) /\ j e. ( 1 ... K ) ) -> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) = ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) )
226 225 mpteq2dva 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ a = c ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
227 simpll2 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> c e. A )
228 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... K ) e. Fin )
229 228 mptexd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) e. _V )
230 221 226 227 229 fvmptd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( F ` c ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
231 230 fveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( F ` c ) ` k ) = ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) )
232 230 fveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( F ` c ) ` ( k - 1 ) ) = ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) )
233 231 232 oveq12d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) = ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) - ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) ) )
234 233 oveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) = ( ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) - ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) ) - 1 ) )
235 eqidd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) = ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) )
236 simpr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> j = k )
237 236 oveq2d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> ( 1 ... j ) = ( 1 ... k ) )
238 237 sumeq1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> sum_ l e. ( 1 ... j ) ( c ` l ) = sum_ l e. ( 1 ... k ) ( c ` l ) )
239 236 238 oveq12d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) = ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) )
240 1zzd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
241 140 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> K e. ZZ )
242 241 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. ZZ )
243 242 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
244 elfznn 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k e. NN )
245 244 3ad2ant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. NN )
246 245 nnzd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
247 246 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ZZ )
248 247 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
249 245 nnge1d 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> 1 <_ k )
250 249 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 <_ k )
251 250 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
252 simpl3 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ( 1 ... ( K + 1 ) ) )
253 1zzd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 e. ZZ )
254 242 peano2zd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. ZZ )
255 elfz 
 |-  ( ( k e. ZZ /\ 1 e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( k e. ( 1 ... ( K + 1 ) ) <-> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
256 247 253 254 255 syl3anc 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k e. ( 1 ... ( K + 1 ) ) <-> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
257 256 biimpd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k e. ( 1 ... ( K + 1 ) ) -> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
258 252 257 mpd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( 1 <_ k /\ k <_ ( K + 1 ) ) )
259 258 simprd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ ( K + 1 ) )
260 neqne 
 |-  ( -. k = ( K + 1 ) -> k =/= ( K + 1 ) )
261 260 adantl 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k =/= ( K + 1 ) )
262 261 necomd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) =/= k )
263 259 262 jca 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) )
264 247 zred 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. RR )
265 254 zred 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. RR )
266 264 265 ltlend 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k < ( K + 1 ) <-> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) ) )
267 263 266 mpbird 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k < ( K + 1 ) )
268 zleltp1 
 |-  ( ( k e. ZZ /\ K e. ZZ ) -> ( k <_ K <-> k < ( K + 1 ) ) )
269 247 242 268 syl2anc 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ K <-> k < ( K + 1 ) ) )
270 267 269 mpbird 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ K )
271 270 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k <_ K )
272 240 243 248 251 271 elfzd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... K ) )
273 ovexd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) e. _V )
274 235 239 272 273 fvmptd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) = ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) )
275 simpr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> j = ( k - 1 ) )
276 275 oveq2d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> ( 1 ... j ) = ( 1 ... ( k - 1 ) ) )
277 276 sumeq1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> sum_ l e. ( 1 ... j ) ( c ` l ) = sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) )
278 275 277 oveq12d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) = ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) )
279 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
280 53 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> K e. ZZ )
281 280 3impa 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
282 244 nnzd 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k e. ZZ )
283 282 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
284 283 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> k e. ZZ )
285 284 3impa 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
286 285 279 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
287 neqne 
 |-  ( -. k = 1 -> k =/= 1 )
288 287 3ad2ant3 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k =/= 1 )
289 108 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
290 285 zred 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. RR )
291 simp2 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... ( K + 1 ) ) )
292 elfzle1 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> 1 <_ k )
293 291 292 syl 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
294 289 290 293 leltned 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> k =/= 1 ) )
295 288 294 mpbird 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 < k )
296 279 285 zltp1led 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
297 295 296 mpbid 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 + 1 ) <_ k )
298 leaddsub 
 |-  ( ( 1 e. RR /\ 1 e. RR /\ k e. RR ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
299 289 289 290 298 syl3anc 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
300 297 299 mpbid 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
301 286 zred 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
302 55 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. RR )
303 1red 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
304 302 303 readdcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( K + 1 ) e. RR )
305 304 303 resubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) e. RR )
306 elfzle2 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k <_ ( K + 1 ) )
307 306 3ad2ant2 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k <_ ( K + 1 ) )
308 290 304 303 307 lesub1dd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( ( K + 1 ) - 1 ) )
309 64 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. CC )
310 1cnd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
311 309 310 pncand 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) = K )
312 56 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K <_ K )
313 311 312 eqbrtrd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) <_ K )
314 301 305 302 308 313 letrd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
315 279 281 286 300 314 elfzd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
316 315 3expa 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
317 316 3adantl2 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
318 317 adantlr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
319 ovexd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) e. _V )
320 235 278 318 319 fvmptd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) = ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) )
321 274 320 oveq12d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) - ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) ) = ( ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) - ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) )
322 321 oveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) - ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) ) - 1 ) = ( ( ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) - ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) )
323 248 zcnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. CC )
324 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... k ) e. Fin )
325 1zzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> 1 e. ZZ )
326 243 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> K e. ZZ )
327 326 peano2zd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( K + 1 ) e. ZZ )
328 elfznn 
 |-  ( l e. ( 1 ... k ) -> l e. NN )
329 328 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. NN )
330 329 nnzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. ZZ )
331 329 nnge1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> 1 <_ l )
332 329 nnred 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. RR )
333 264 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> k e. RR )
334 265 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( K + 1 ) e. RR )
335 elfzle2 
 |-  ( l e. ( 1 ... k ) -> l <_ k )
336 335 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l <_ k )
337 259 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> k <_ ( K + 1 ) )
338 332 333 334 336 337 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l <_ ( K + 1 ) )
339 325 327 330 331 338 elfzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. ( 1 ... ( K + 1 ) ) )
340 97 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
341 340 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
342 341 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
343 342 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
344 343 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
345 339 344 mpdan 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( c ` l ) e. NN0 )
346 324 345 fsumnn0cl 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... k ) ( c ` l ) e. NN0 )
347 346 nn0cnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... k ) ( c ` l ) e. CC )
348 1cnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
349 323 348 subcld 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. CC )
350 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... ( k - 1 ) ) e. Fin )
351 1zzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 e. ZZ )
352 243 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> K e. ZZ )
353 352 peano2zd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( K + 1 ) e. ZZ )
354 elfznn 
 |-  ( l e. ( 1 ... ( k - 1 ) ) -> l e. NN )
355 354 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. NN )
356 355 nnzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. ZZ )
357 355 nnge1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 <_ l )
358 355 nnred 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. RR )
359 264 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> k e. RR )
360 1red 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 e. RR )
361 359 360 resubcld 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) e. RR )
362 265 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( K + 1 ) e. RR )
363 elfzle2 
 |-  ( l e. ( 1 ... ( k - 1 ) ) -> l <_ ( k - 1 ) )
364 363 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l <_ ( k - 1 ) )
365 359 lem1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) <_ k )
366 259 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> k <_ ( K + 1 ) )
367 361 359 362 365 366 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) <_ ( K + 1 ) )
368 358 361 362 364 367 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l <_ ( K + 1 ) )
369 351 353 356 357 368 elfzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. ( 1 ... ( K + 1 ) ) )
370 342 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
371 370 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
372 369 371 mpdan 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( c ` l ) e. NN0 )
373 350 372 fsumnn0cl 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) e. NN0 )
374 373 nn0cnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) e. CC )
375 323 347 349 374 addsub4d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) - ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) = ( ( k - ( k - 1 ) ) + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) )
376 375 oveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) - ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( ( ( k - ( k - 1 ) ) + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) )
377 323 348 nncand 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - ( k - 1 ) ) = 1 )
378 377 oveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( k - ( k - 1 ) ) + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) = ( 1 + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) )
379 378 oveq1d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( k - ( k - 1 ) ) + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( ( 1 + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) )
380 347 374 subcld 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) e. CC )
381 348 380 pncan2d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 1 + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) )
382 139 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> 1 e. ZZ )
383 382 246 249 3jca 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( 1 e. ZZ /\ k e. ZZ /\ 1 <_ k ) )
384 eluz2 
 |-  ( k e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ k e. ZZ /\ 1 <_ k ) )
385 383 384 sylibr 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ( ZZ>= ` 1 ) )
386 385 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ( ZZ>= ` 1 ) )
387 386 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( ZZ>= ` 1 ) )
388 345 nn0cnd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( c ` l ) e. CC )
389 fveq2 
 |-  ( l = k -> ( c ` l ) = ( c ` k ) )
390 387 388 389 fsumm1 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... k ) ( c ` l ) = ( sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) + ( c ` k ) ) )
391 390 eqcomd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) + ( c ` k ) ) = sum_ l e. ( 1 ... k ) ( c ` l ) )
392 simp3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ( 1 ... ( K + 1 ) ) )
393 340 392 ffvelrnd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( c ` k ) e. NN0 )
394 393 nn0cnd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( c ` k ) e. CC )
395 394 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( c ` k ) e. CC )
396 395 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( c ` k ) e. CC )
397 347 374 396 subaddd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) = ( c ` k ) <-> ( sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) + ( c ` k ) ) = sum_ l e. ( 1 ... k ) ( c ` l ) ) )
398 391 397 mpbird 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) = ( c ` k ) )
399 381 398 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 1 + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( c ` k ) )
400 379 399 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( k - ( k - 1 ) ) + ( sum_ l e. ( 1 ... k ) ( c ` l ) - sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( c ` k ) )
401 376 400 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( k + sum_ l e. ( 1 ... k ) ( c ` l ) ) - ( ( k - 1 ) + sum_ l e. ( 1 ... ( k - 1 ) ) ( c ` l ) ) ) - 1 ) = ( c ` k ) )
402 322 401 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` k ) - ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` ( k - 1 ) ) ) - 1 ) = ( c ` k ) )
403 234 402 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) = ( c ` k ) )
404 220 403 ifeqda 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) = ( c ` k ) )
405 166 404 ifeqda 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) = ( c ` k ) )
406 405 3expa 
 |-  ( ( ( ph /\ c e. A ) /\ k e. ( 1 ... ( K + 1 ) ) ) -> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) = ( c ` k ) )
407 406 mpteq2dva 
 |-  ( ( ph /\ c e. A ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
408 97 ffnd 
 |-  ( ( ph /\ c e. A ) -> c Fn ( 1 ... ( K + 1 ) ) )
409 dffn5 
 |-  ( c Fn ( 1 ... ( K + 1 ) ) <-> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
410 409 biimpi 
 |-  ( c Fn ( 1 ... ( K + 1 ) ) -> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
411 408 410 syl 
 |-  ( ( ph /\ c e. A ) -> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
412 411 eqcomd 
 |-  ( ( ph /\ c e. A ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) = c )
413 407 412 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( ( F ` c ) ` K ) ) , if ( k = 1 , ( ( ( F ` c ) ` 1 ) - 1 ) , ( ( ( ( F ` c ) ` k ) - ( ( F ` c ) ` ( k - 1 ) ) ) - 1 ) ) ) ) = c )
414 37 413 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = c )
415 414 ralrimiva 
 |-  ( ph -> A. c e. A ( G ` ( F ` c ) ) = c )
416 1 2 3 4 5 6 sticksstones12a 
 |-  ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )
417 8 9 415 416 2fvidf1od 
 |-  ( ph -> F : A -1-1-onto-> B )