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