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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ( c ` l )
131 nfcv 
 |-  F/_ l ( c ` i )
132 129 130 131 cbvsum 
 |-  sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i )
133 132 a1i 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) )
134 96 simprd 
 |-  ( ( ph /\ c e. A ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( c ` i ) = N )
135 133 134 eqtrd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... ( K + 1 ) ) ( c ` l ) = N )
136 128 135 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( sum_ l e. ( 1 ... K ) ( c ` l ) + ( c ` ( K + 1 ) ) ) = N )
137 1zzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ZZ )
138 53 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. ZZ )
139 138 peano2zd 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) e. ZZ )
140 1e0p1 
 |-  1 = ( 0 + 1 )
141 140 a1i 
 |-  ( ( ph /\ c e. A ) -> 1 = ( 0 + 1 ) )
142 0red 
 |-  ( ( ph /\ c e. A ) -> 0 e. RR )
143 55 adantr 
 |-  ( ( ph /\ c e. A ) -> K e. RR )
144 1red 
 |-  ( ( ph /\ c e. A ) -> 1 e. RR )
145 11 55 12 ltled 
 |-  ( ph -> 0 <_ K )
146 145 adantr 
 |-  ( ( ph /\ c e. A ) -> 0 <_ K )
147 142 143 144 146 leadd1dd 
 |-  ( ( ph /\ c e. A ) -> ( 0 + 1 ) <_ ( K + 1 ) )
148 141 147 eqbrtrd 
 |-  ( ( ph /\ c e. A ) -> 1 <_ ( K + 1 ) )
149 55 55 108 56 leadd1dd 
 |-  ( ph -> ( K + 1 ) <_ ( K + 1 ) )
150 149 adantr 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) <_ ( K + 1 ) )
151 137 139 139 148 150 elfzd 
 |-  ( ( ph /\ c e. A ) -> ( K + 1 ) e. ( 1 ... ( K + 1 ) ) )
152 97 151 ffvelcdmd 
 |-  ( ( ph /\ c e. A ) -> ( c ` ( K + 1 ) ) e. NN0 )
153 152 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` ( K + 1 ) ) e. CC )
154 63 102 153 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 ) )
155 136 154 mpbird 
 |-  ( ( ph /\ c e. A ) -> ( N - sum_ l e. ( 1 ... K ) ( c ` l ) ) = ( c ` ( K + 1 ) ) )
156 103 155 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( K + N ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( c ` ( K + 1 ) ) )
157 67 156 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( K + sum_ l e. ( 1 ... K ) ( c ` l ) ) ) = ( c ` ( K + 1 ) ) )
158 61 157 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
159 158 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
160 159 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` ( K + 1 ) ) )
161 simpr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> k = ( K + 1 ) )
162 161 fveq2d 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( c ` k ) = ( c ` ( K + 1 ) ) )
163 162 eqcomd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( c ` ( K + 1 ) ) = ( c ` k ) )
164 160 163 eqtrd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ k = ( K + 1 ) ) -> ( ( N + K ) - ( ( F ` c ) ` K ) ) = ( c ` k ) )
165 47 fveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( F ` c ) ` 1 ) = ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) )
166 165 oveq1d 
 |-  ( ( ph /\ c e. A ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) - 1 ) )
167 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 ) ) ) )
168 simpr 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> j = 1 )
169 168 oveq2d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> ( 1 ... j ) = ( 1 ... 1 ) )
170 169 sumeq1d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> sum_ l e. ( 1 ... j ) ( c ` l ) = sum_ l e. ( 1 ... 1 ) ( c ` l ) )
171 168 170 oveq12d 
 |-  ( ( ( ph /\ c e. A ) /\ j = 1 ) -> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) = ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) )
172 144 leidd 
 |-  ( ( ph /\ c e. A ) -> 1 <_ 1 )
173 54 adantr 
 |-  ( ( ph /\ c e. A ) -> 1 <_ K )
174 137 138 137 172 173 elfzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ( 1 ... K ) )
175 ovexd 
 |-  ( ( ph /\ c e. A ) -> ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) e. _V )
176 167 171 174 175 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 ) ) )
177 176 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 ) )
178 fzfid 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... 1 ) e. Fin )
179 1zzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 e. ZZ )
180 138 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> K e. ZZ )
181 180 peano2zd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( K + 1 ) e. ZZ )
182 elfzelz 
 |-  ( l e. ( 1 ... 1 ) -> l e. ZZ )
183 182 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. ZZ )
184 elfzle1 
 |-  ( l e. ( 1 ... 1 ) -> 1 <_ l )
185 184 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 <_ l )
186 183 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. RR )
187 0red 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 0 e. RR )
188 1red 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 e. RR )
189 187 188 readdcld 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( 0 + 1 ) e. RR )
190 181 zred 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( K + 1 ) e. RR )
191 elfzle2 
 |-  ( l e. ( 1 ... 1 ) -> l <_ 1 )
192 191 adantl 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ 1 )
193 140 a1i 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> 1 = ( 0 + 1 ) )
194 192 193 breqtrd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ ( 0 + 1 ) )
195 147 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( 0 + 1 ) <_ ( K + 1 ) )
196 186 189 190 194 195 letrd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l <_ ( K + 1 ) )
197 179 181 183 185 196 elfzd 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> l e. ( 1 ... ( K + 1 ) ) )
198 118 adantlr 
 |-  ( ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) /\ l e. ( 1 ... ( K + 1 ) ) ) -> ( c ` l ) e. NN0 )
199 197 198 mpdan 
 |-  ( ( ( ph /\ c e. A ) /\ l e. ( 1 ... 1 ) ) -> ( c ` l ) e. NN0 )
200 178 199 fsumnn0cl 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) e. NN0 )
201 200 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) e. CC )
202 122 201 pncan2d 
 |-  ( ( ph /\ c e. A ) -> ( ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) - 1 ) = sum_ l e. ( 1 ... 1 ) ( c ` l ) )
203 137 139 137 172 148 elfzd 
 |-  ( ( ph /\ c e. A ) -> 1 e. ( 1 ... ( K + 1 ) ) )
204 97 203 ffvelcdmd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. NN0 )
205 204 nn0cnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. CC )
206 fveq2 
 |-  ( l = 1 -> ( c ` l ) = ( c ` 1 ) )
207 206 fsum1 
 |-  ( ( 1 e. ZZ /\ ( c ` 1 ) e. CC ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) = ( c ` 1 ) )
208 137 205 207 syl2anc 
 |-  ( ( ph /\ c e. A ) -> sum_ l e. ( 1 ... 1 ) ( c ` l ) = ( c ` 1 ) )
209 202 208 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( 1 + sum_ l e. ( 1 ... 1 ) ( c ` l ) ) - 1 ) = ( c ` 1 ) )
210 177 209 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( c ` l ) ) ) ` 1 ) - 1 ) = ( c ` 1 ) )
211 166 210 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
212 211 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
213 212 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
214 213 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` 1 ) )
215 simpr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> k = 1 )
216 215 fveq2d 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( c ` k ) = ( c ` 1 ) )
217 216 eqcomd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( c ` 1 ) = ( c ` k ) )
218 214 217 eqtrd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ k = 1 ) -> ( ( ( F ` c ) ` 1 ) - 1 ) = ( c ` k ) )
219 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 ) ) ) ) )
220 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 )
221 220 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 ) )
222 221 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 ) )
223 222 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 ) ) )
224 223 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 ) ) ) )
225 simpll2 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> c e. A )
226 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... K ) e. Fin )
227 226 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 )
228 219 224 225 227 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 ) ) ) )
229 228 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 ) )
230 228 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 ) ) )
231 229 230 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 ) ) ) )
232 231 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 ) )
233 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 ) ) ) )
234 simpr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> j = k )
235 234 oveq2d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = k ) -> ( 1 ... j ) = ( 1 ... k ) )
236 235 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 ) )
237 234 236 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 ) ) )
238 1zzd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
239 138 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> K e. ZZ )
240 239 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> K e. ZZ )
241 240 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
242 elfznn 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k e. NN )
243 242 3ad2ant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. NN )
244 243 nnzd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
245 244 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ZZ )
246 245 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
247 243 nnge1d 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> 1 <_ k )
248 247 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 <_ k )
249 248 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
250 simpl3 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ( 1 ... ( K + 1 ) ) )
251 1zzd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> 1 e. ZZ )
252 240 peano2zd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. ZZ )
253 elfz 
 |-  ( ( k e. ZZ /\ 1 e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( k e. ( 1 ... ( K + 1 ) ) <-> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
254 245 251 252 253 syl3anc 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k e. ( 1 ... ( K + 1 ) ) <-> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
255 254 biimpd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k e. ( 1 ... ( K + 1 ) ) -> ( 1 <_ k /\ k <_ ( K + 1 ) ) ) )
256 250 255 mpd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( 1 <_ k /\ k <_ ( K + 1 ) ) )
257 256 simprd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ ( K + 1 ) )
258 neqne 
 |-  ( -. k = ( K + 1 ) -> k =/= ( K + 1 ) )
259 258 adantl 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k =/= ( K + 1 ) )
260 259 necomd 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) =/= k )
261 257 260 jca 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) )
262 245 zred 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. RR )
263 252 zred 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( K + 1 ) e. RR )
264 262 263 ltlend 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k < ( K + 1 ) <-> ( k <_ ( K + 1 ) /\ ( K + 1 ) =/= k ) ) )
265 261 264 mpbird 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k < ( K + 1 ) )
266 zleltp1 
 |-  ( ( k e. ZZ /\ K e. ZZ ) -> ( k <_ K <-> k < ( K + 1 ) ) )
267 245 240 266 syl2anc 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( k <_ K <-> k < ( K + 1 ) ) )
268 265 267 mpbird 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k <_ K )
269 268 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k <_ K )
270 238 241 246 249 269 elfzd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... K ) )
271 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 )
272 233 237 270 271 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 ) ) )
273 simpr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> j = ( k - 1 ) )
274 273 oveq2d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ j = ( k - 1 ) ) -> ( 1 ... j ) = ( 1 ... ( k - 1 ) ) )
275 274 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 ) )
276 273 275 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 ) ) )
277 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. ZZ )
278 53 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> K e. ZZ )
279 278 3impa 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. ZZ )
280 242 nnzd 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k e. ZZ )
281 280 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ZZ )
282 281 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> k e. ZZ )
283 282 3impa 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ZZ )
284 283 277 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ZZ )
285 neqne 
 |-  ( -. k = 1 -> k =/= 1 )
286 285 3ad2ant3 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k =/= 1 )
287 108 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
288 283 zred 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. RR )
289 simp2 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( 1 ... ( K + 1 ) ) )
290 elfzle1 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> 1 <_ k )
291 289 290 syl 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ k )
292 287 288 291 leltned 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> k =/= 1 ) )
293 286 292 mpbird 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 < k )
294 277 283 zltp1led 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
295 293 294 mpbid 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 + 1 ) <_ k )
296 leaddsub 
 |-  ( ( 1 e. RR /\ 1 e. RR /\ k e. RR ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
297 287 287 288 296 syl3anc 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( 1 + 1 ) <_ k <-> 1 <_ ( k - 1 ) ) )
298 295 297 mpbid 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 <_ ( k - 1 ) )
299 284 zred 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
300 55 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. RR )
301 1red 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. RR )
302 300 301 readdcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( K + 1 ) e. RR )
303 302 301 resubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) e. RR )
304 elfzle2 
 |-  ( k e. ( 1 ... ( K + 1 ) ) -> k <_ ( K + 1 ) )
305 304 3ad2ant2 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> k <_ ( K + 1 ) )
306 288 302 301 305 lesub1dd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( ( K + 1 ) - 1 ) )
307 64 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K e. CC )
308 1cnd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
309 307 308 pncand 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) = K )
310 56 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> K <_ K )
311 309 310 eqbrtrd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( ( K + 1 ) - 1 ) <_ K )
312 299 303 300 306 311 letrd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ K )
313 277 279 284 298 312 elfzd 
 |-  ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
314 313 3expa 
 |-  ( ( ( ph /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
315 314 3adantl2 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
316 315 adantlr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. ( 1 ... K ) )
317 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 )
318 233 276 316 317 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 ) ) )
319 272 318 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 ) ) ) )
320 319 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 ) )
321 246 zcnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. CC )
322 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... k ) e. Fin )
323 1zzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> 1 e. ZZ )
324 241 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> K e. ZZ )
325 324 peano2zd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( K + 1 ) e. ZZ )
326 elfznn 
 |-  ( l e. ( 1 ... k ) -> l e. NN )
327 326 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. NN )
328 327 nnzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. ZZ )
329 327 nnge1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> 1 <_ l )
330 327 nnred 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. RR )
331 262 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> k e. RR )
332 263 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( K + 1 ) e. RR )
333 elfzle2 
 |-  ( l e. ( 1 ... k ) -> l <_ k )
334 333 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l <_ k )
335 257 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> k <_ ( K + 1 ) )
336 330 331 332 334 335 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l <_ ( K + 1 ) )
337 323 325 328 329 336 elfzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> l e. ( 1 ... ( K + 1 ) ) )
338 97 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
339 338 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
340 339 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
341 340 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> c : ( 1 ... ( K + 1 ) ) --> NN0 )
342 341 ffvelcdmda 
 |-  ( ( ( ( ( ( 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 )
343 337 342 mpdan 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( c ` l ) e. NN0 )
344 322 343 fsumnn0cl 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... k ) ( c ` l ) e. NN0 )
345 344 nn0cnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> sum_ l e. ( 1 ... k ) ( c ` l ) e. CC )
346 1cnd 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> 1 e. CC )
347 321 346 subcld 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - 1 ) e. CC )
348 fzfid 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( 1 ... ( k - 1 ) ) e. Fin )
349 1zzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 e. ZZ )
350 241 adantr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> K e. ZZ )
351 350 peano2zd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( K + 1 ) e. ZZ )
352 elfznn 
 |-  ( l e. ( 1 ... ( k - 1 ) ) -> l e. NN )
353 352 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. NN )
354 353 nnzd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. ZZ )
355 353 nnge1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 <_ l )
356 353 nnred 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l e. RR )
357 262 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> k e. RR )
358 1red 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> 1 e. RR )
359 357 358 resubcld 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) e. RR )
360 263 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( K + 1 ) e. RR )
361 elfzle2 
 |-  ( l e. ( 1 ... ( k - 1 ) ) -> l <_ ( k - 1 ) )
362 361 adantl 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l <_ ( k - 1 ) )
363 357 lem1d 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) <_ k )
364 257 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> k <_ ( K + 1 ) )
365 359 357 360 363 364 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( k - 1 ) <_ ( K + 1 ) )
366 356 359 360 362 365 letrd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> l <_ ( K + 1 ) )
367 349 351 354 355 366 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 ) ) )
368 340 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 )
369 368 ffvelcdmda 
 |-  ( ( ( ( ( ( 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 )
370 367 369 mpdan 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... ( k - 1 ) ) ) -> ( c ` l ) e. NN0 )
371 348 370 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 )
372 371 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 )
373 321 345 347 372 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 ) ) ) )
374 373 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 ) )
375 321 346 nncand 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( k - ( k - 1 ) ) = 1 )
376 375 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 ) ) ) )
377 376 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 ) )
378 345 372 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 )
379 346 378 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 ) ) )
380 137 3adant3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> 1 e. ZZ )
381 380 244 247 3jca 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( 1 e. ZZ /\ k e. ZZ /\ 1 <_ k ) )
382 eluz2 
 |-  ( k e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ k e. ZZ /\ 1 <_ k ) )
383 381 382 sylibr 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ( ZZ>= ` 1 ) )
384 383 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> k e. ( ZZ>= ` 1 ) )
385 384 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> k e. ( ZZ>= ` 1 ) )
386 343 nn0cnd 
 |-  ( ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) /\ l e. ( 1 ... k ) ) -> ( c ` l ) e. CC )
387 fveq2 
 |-  ( l = k -> ( c ` l ) = ( c ` k ) )
388 385 386 387 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 ) ) )
389 388 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 ) )
390 simp3 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> k e. ( 1 ... ( K + 1 ) ) )
391 338 390 ffvelcdmd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( c ` k ) e. NN0 )
392 391 nn0cnd 
 |-  ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) -> ( c ` k ) e. CC )
393 392 adantr 
 |-  ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) -> ( c ` k ) e. CC )
394 393 adantr 
 |-  ( ( ( ( ph /\ c e. A /\ k e. ( 1 ... ( K + 1 ) ) ) /\ -. k = ( K + 1 ) ) /\ -. k = 1 ) -> ( c ` k ) e. CC )
395 345 372 394 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 ) ) )
396 389 395 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 ) )
397 379 396 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 ) )
398 377 397 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 ) )
399 374 398 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 ) )
400 320 399 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 ) )
401 232 400 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 ) )
402 218 401 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 ) )
403 164 402 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 ) )
404 403 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 ) )
405 404 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 ) ) )
406 97 ffnd 
 |-  ( ( ph /\ c e. A ) -> c Fn ( 1 ... ( K + 1 ) ) )
407 dffn5 
 |-  ( c Fn ( 1 ... ( K + 1 ) ) <-> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
408 407 biimpi 
 |-  ( c Fn ( 1 ... ( K + 1 ) ) -> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
409 406 408 syl 
 |-  ( ( ph /\ c e. A ) -> c = ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) )
410 409 eqcomd 
 |-  ( ( ph /\ c e. A ) -> ( k e. ( 1 ... ( K + 1 ) ) |-> ( c ` k ) ) = c )
411 405 410 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 )
412 37 411 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = c )
413 412 ralrimiva 
 |-  ( ph -> A. c e. A ( G ` ( F ` c ) ) = c )
414 1 2 3 4 5 6 sticksstones12a 
 |-  ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )
415 8 9 413 414 2fvidf1od 
 |-  ( ph -> F : A -1-1-onto-> B )