Metamath Proof Explorer

Theorem ovolicc2lem4

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc2.4 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolicc2.5 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovolicc2.6 
|- ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
ovolicc2.7 
|- ( ph -> ( A [,] B ) C_ U. U )
ovolicc2.8 
|- ( ph -> G : U --> NN )
ovolicc2.9 
|- ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
ovolicc2.10 
|- T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
ovolicc2.11 
|- ( ph -> H : T --> T )
ovolicc2.12 
|- ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
ovolicc2.13 
|- ( ph -> A e. C )
ovolicc2.14 
|- ( ph -> C e. T )
ovolicc2.15 
|- K = seq 1 ( ( H o. 1st ) , ( NN X. { C } ) )
ovolicc2.16 
|- W = { n e. NN | B e. ( K ` n ) }
ovolicc2.17 
|- M = inf ( W , RR , < )
Assertion ovolicc2lem4 
|- ( ph -> ( B - A ) <_ sup ( ran S , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc2.4 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolicc2.5 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
6 ovolicc2.6 
 |-  ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
7 ovolicc2.7 
 |-  ( ph -> ( A [,] B ) C_ U. U )
8 ovolicc2.8 
 |-  ( ph -> G : U --> NN )
9 ovolicc2.9 
 |-  ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
10 ovolicc2.10 
 |-  T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
11 ovolicc2.11 
 |-  ( ph -> H : T --> T )
12 ovolicc2.12 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
13 ovolicc2.13 
 |-  ( ph -> A e. C )
14 ovolicc2.14 
 |-  ( ph -> C e. T )
15 ovolicc2.15 
 |-  K = seq 1 ( ( H o. 1st ) , ( NN X. { C } ) )
16 ovolicc2.16 
 |-  W = { n e. NN | B e. ( K ` n ) }
17 ovolicc2.17 
 |-  M = inf ( W , RR , < )
18 arch 
 |-  ( x e. RR -> E. z e. NN x < z )
19 18 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x ) -> E. z e. NN x < z )
20 df-ima 
 |-  ( ( G o. K ) " ( 1 ... M ) ) = ran ( ( G o. K ) |` ( 1 ... M ) )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 1zzd 
 |-  ( ph -> 1 e. ZZ )
23 21 15 22 14 11 algrf 
 |-  ( ph -> K : NN --> T )
24 10 ssrab3 
 |-  T C_ U
25 fss 
 |-  ( ( K : NN --> T /\ T C_ U ) -> K : NN --> U )
26 23 24 25 sylancl 
 |-  ( ph -> K : NN --> U )
27 fco 
 |-  ( ( G : U --> NN /\ K : NN --> U ) -> ( G o. K ) : NN --> NN )
28 8 26 27 syl2anc 
 |-  ( ph -> ( G o. K ) : NN --> NN )
29 fz1ssnn 
 |-  ( 1 ... M ) C_ NN
30 fssres 
 |-  ( ( ( G o. K ) : NN --> NN /\ ( 1 ... M ) C_ NN ) -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) --> NN )
31 28 29 30 sylancl 
 |-  ( ph -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) --> NN )
32 31 frnd 
 |-  ( ph -> ran ( ( G o. K ) |` ( 1 ... M ) ) C_ NN )
33 20 32 eqsstrid 
 |-  ( ph -> ( ( G o. K ) " ( 1 ... M ) ) C_ NN )
34 nnssre 
 |-  NN C_ RR
35 33 34 sstrdi 
 |-  ( ph -> ( ( G o. K ) " ( 1 ... M ) ) C_ RR )
36 35 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( G o. K ) " ( 1 ... M ) ) C_ RR )
37 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> y e. ( ( G o. K ) " ( 1 ... M ) ) )
38 36 37 sseldd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> y e. RR )
39 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> x e. RR )
40 nnre 
 |-  ( z e. NN -> z e. RR )
41 40 ad2antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> z e. RR )
42 lelttr 
 |-  ( ( y e. RR /\ x e. RR /\ z e. RR ) -> ( ( y <_ x /\ x < z ) -> y < z ) )
43 38 39 41 42 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( y <_ x /\ x < z ) -> y < z ) )
44 43 ancomsd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( x < z /\ y <_ x ) -> y < z ) )
45 44 expdimp 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) /\ x < z ) -> ( y <_ x -> y < z ) )
46 45 an32s 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ x < z ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( y <_ x -> y < z ) )
47 46 ralimdva 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ x < z ) -> ( A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x -> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) )
48 47 impancom 
 |-  ( ( ( ( ph /\ x e. RR ) /\ z e. NN ) /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x ) -> ( x < z -> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) )
49 48 an32s 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x ) /\ z e. NN ) -> ( x < z -> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) )
50 49 reximdva 
 |-  ( ( ( ph /\ x e. RR ) /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x ) -> ( E. z e. NN x < z -> E. z e. NN A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) )
51 19 50 mpd 
 |-  ( ( ( ph /\ x e. RR ) /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x ) -> E. z e. NN A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z )
52 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
53 fvres 
 |-  ( i e. ( 1 ... M ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( G o. K ) ` i ) )
54 53 adantl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( G o. K ) ` i ) )
55 elfznn 
 |-  ( i e. ( 1 ... M ) -> i e. NN )
56 fvco3 
 |-  ( ( K : NN --> T /\ i e. NN ) -> ( ( G o. K ) ` i ) = ( G ` ( K ` i ) ) )
57 23 55 56 syl2an 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( G o. K ) ` i ) = ( G ` ( K ` i ) ) )
58 54 57 eqtrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( G ` ( K ` i ) ) )
59 58 adantrr 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( G ` ( K ` i ) ) )
60 fvres 
 |-  ( j e. ( 1 ... M ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) = ( ( G o. K ) ` j ) )
61 60 ad2antll 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) = ( ( G o. K ) ` j ) )
62 elfznn 
 |-  ( j e. ( 1 ... M ) -> j e. NN )
63 62 adantl 
 |-  ( ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) -> j e. NN )
64 fvco3 
 |-  ( ( K : NN --> T /\ j e. NN ) -> ( ( G o. K ) ` j ) = ( G ` ( K ` j ) ) )
65 23 63 64 syl2an 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( G o. K ) ` j ) = ( G ` ( K ` j ) ) )
66 61 65 eqtrd 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) = ( G ` ( K ` j ) ) )
67 59 66 eqeq12d 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) <-> ( G ` ( K ` i ) ) = ( G ` ( K ` j ) ) ) )
68 2fveq3 
 |-  ( ( G ` ( K ` i ) ) = ( G ` ( K ` j ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` j ) ) ) ) )
69 29 a1i 
 |-  ( ph -> ( 1 ... M ) C_ NN )
70 elfznn 
 |-  ( n e. ( 1 ... M ) -> n e. NN )
71 70 ad2antlr 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> n e. NN )
72 71 nnred 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> n e. RR )
73 16 ssrab3 
 |-  W C_ NN
74 73 34 sstri 
 |-  W C_ RR
75 73 21 sseqtri 
 |-  W C_ ( ZZ>= ` 1 )
76 nnnfi 
 |-  -. NN e. Fin
77 6 elin2d 
 |-  ( ph -> U e. Fin )
78 ssfi 
 |-  ( ( U e. Fin /\ T C_ U ) -> T e. Fin )
79 77 24 78 sylancl 
 |-  ( ph -> T e. Fin )
80 79 adantr 
 |-  ( ( ph /\ W = (/) ) -> T e. Fin )
81 23 adantr 
 |-  ( ( ph /\ W = (/) ) -> K : NN --> T )
82 2fveq3 
 |-  ( ( K ` i ) = ( K ` j ) -> ( F ` ( G ` ( K ` i ) ) ) = ( F ` ( G ` ( K ` j ) ) ) )
83 82 fveq2d 
 |-  ( ( K ` i ) = ( K ` j ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` j ) ) ) ) )
84 simpll 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> ph )
85 simprl 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> i e. NN )
86 ral0 
 |-  A. m e. (/) n <_ m
87 simplr 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> W = (/) )
88 87 raleqdv 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> ( A. m e. W n <_ m <-> A. m e. (/) n <_ m ) )
89 86 88 mpbiri 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> A. m e. W n <_ m )
90 89 ralrimivw 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> A. n e. NN A. m e. W n <_ m )
91 rabid2 
 |-  ( NN = { n e. NN | A. m e. W n <_ m } <-> A. n e. NN A. m e. W n <_ m )
92 90 91 sylibr 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> NN = { n e. NN | A. m e. W n <_ m } )
93 85 92 eleqtrd 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> i e. { n e. NN | A. m e. W n <_ m } )
94 simprr 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> j e. NN )
95 94 92 eleqtrd 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> j e. { n e. NN | A. m e. W n <_ m } )
96 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem3 
 |-  ( ( ph /\ ( i e. { n e. NN | A. m e. W n <_ m } /\ j e. { n e. NN | A. m e. W n <_ m } ) ) -> ( i = j <-> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` j ) ) ) ) ) )
97 84 93 95 96 syl12anc 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> ( i = j <-> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` j ) ) ) ) ) )
98 83 97 imbitrrid 
 |-  ( ( ( ph /\ W = (/) ) /\ ( i e. NN /\ j e. NN ) ) -> ( ( K ` i ) = ( K ` j ) -> i = j ) )
99 98 ralrimivva 
 |-  ( ( ph /\ W = (/) ) -> A. i e. NN A. j e. NN ( ( K ` i ) = ( K ` j ) -> i = j ) )
100 dff13 
 |-  ( K : NN -1-1-> T <-> ( K : NN --> T /\ A. i e. NN A. j e. NN ( ( K ` i ) = ( K ` j ) -> i = j ) ) )
101 81 99 100 sylanbrc 
 |-  ( ( ph /\ W = (/) ) -> K : NN -1-1-> T )
102 f1domg 
 |-  ( T e. Fin -> ( K : NN -1-1-> T -> NN ~<_ T ) )
103 80 101 102 sylc 
 |-  ( ( ph /\ W = (/) ) -> NN ~<_ T )
104 domfi 
 |-  ( ( T e. Fin /\ NN ~<_ T ) -> NN e. Fin )
105 79 103 104 syl2an2r 
 |-  ( ( ph /\ W = (/) ) -> NN e. Fin )
106 105 ex 
 |-  ( ph -> ( W = (/) -> NN e. Fin ) )
107 106 necon3bd 
 |-  ( ph -> ( -. NN e. Fin -> W =/= (/) ) )
108 76 107 mpi 
 |-  ( ph -> W =/= (/) )
109 infssuzcl 
 |-  ( ( W C_ ( ZZ>= ` 1 ) /\ W =/= (/) ) -> inf ( W , RR , < ) e. W )
110 75 108 109 sylancr 
 |-  ( ph -> inf ( W , RR , < ) e. W )
111 17 110 eqeltrid 
 |-  ( ph -> M e. W )
112 74 111 sselid 
 |-  ( ph -> M e. RR )
113 112 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> M e. RR )
114 74 sseli 
 |-  ( m e. W -> m e. RR )
115 114 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> m e. RR )
116 elfzle2 
 |-  ( n e. ( 1 ... M ) -> n <_ M )
117 116 ad2antlr 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> n <_ M )
118 infssuzle 
 |-  ( ( W C_ ( ZZ>= ` 1 ) /\ m e. W ) -> inf ( W , RR , < ) <_ m )
119 75 118 mpan 
 |-  ( m e. W -> inf ( W , RR , < ) <_ m )
120 17 119 eqbrtrid 
 |-  ( m e. W -> M <_ m )
121 120 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> M <_ m )
122 72 113 115 117 121 letrd 
 |-  ( ( ( ph /\ n e. ( 1 ... M ) ) /\ m e. W ) -> n <_ m )
123 122 ralrimiva 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> A. m e. W n <_ m )
124 69 123 ssrabdv 
 |-  ( ph -> ( 1 ... M ) C_ { n e. NN | A. m e. W n <_ m } )
125 124 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( 1 ... M ) C_ { n e. NN | A. m e. W n <_ m } )
126 simprl 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> i e. ( 1 ... M ) )
127 125 126 sseldd 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> i e. { n e. NN | A. m e. W n <_ m } )
128 simprr 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> j e. ( 1 ... M ) )
129 125 128 sseldd 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> j e. { n e. NN | A. m e. W n <_ m } )
130 127 129 jca 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( i e. { n e. NN | A. m e. W n <_ m } /\ j e. { n e. NN | A. m e. W n <_ m } ) )
131 130 96 syldan 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( i = j <-> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` j ) ) ) ) ) )
132 68 131 imbitrrid 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( G ` ( K ` i ) ) = ( G ` ( K ` j ) ) -> i = j ) )
133 67 132 sylbid 
 |-  ( ( ph /\ ( i e. ( 1 ... M ) /\ j e. ( 1 ... M ) ) ) -> ( ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) -> i = j ) )
134 133 ralrimivva 
 |-  ( ph -> A. i e. ( 1 ... M ) A. j e. ( 1 ... M ) ( ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) -> i = j ) )
135 dff13 
 |-  ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-> NN <-> ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) --> NN /\ A. i e. ( 1 ... M ) A. j e. ( 1 ... M ) ( ( ( ( G o. K ) |` ( 1 ... M ) ) ` i ) = ( ( ( G o. K ) |` ( 1 ... M ) ) ` j ) -> i = j ) ) )
136 31 134 135 sylanbrc 
 |-  ( ph -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-> NN )
137 f1f1orn 
 |-  ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-> NN -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran ( ( G o. K ) |` ( 1 ... M ) ) )
138 136 137 syl 
 |-  ( ph -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran ( ( G o. K ) |` ( 1 ... M ) ) )
139 f1oeq3 
 |-  ( ( ( G o. K ) " ( 1 ... M ) ) = ran ( ( G o. K ) |` ( 1 ... M ) ) -> ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G o. K ) " ( 1 ... M ) ) <-> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran ( ( G o. K ) |` ( 1 ... M ) ) ) )
140 20 139 ax-mp 
 |-  ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G o. K ) " ( 1 ... M ) ) <-> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran ( ( G o. K ) |` ( 1 ... M ) ) )
141 138 140 sylibr 
 |-  ( ph -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G o. K ) " ( 1 ... M ) ) )
142 f1ofo 
 |-  ( ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G o. K ) " ( 1 ... M ) ) -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G o. K ) " ( 1 ... M ) ) )
143 141 142 syl 
 |-  ( ph -> ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G o. K ) " ( 1 ... M ) ) )
144 fofi 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( ( G o. K ) |` ( 1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( G o. K ) " ( 1 ... M ) ) e. Fin )
145 52 143 144 syl2anc 
 |-  ( ph -> ( ( G o. K ) " ( 1 ... M ) ) e. Fin )
146 fimaxre2 
 |-  ( ( ( ( G o. K ) " ( 1 ... M ) ) C_ RR /\ ( ( G o. K ) " ( 1 ... M ) ) e. Fin ) -> E. x e. RR A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x )
147 35 145 146 syl2anc 
 |-  ( ph -> E. x e. RR A. y e. ( ( G o. K ) " ( 1 ... M ) ) y <_ x )
148 51 147 r19.29a 
 |-  ( ph -> E. z e. NN A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z )
149 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
150 149 rexrd 
 |-  ( ph -> ( B - A ) e. RR* )
151 150 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( B - A ) e. RR* )
152 fzfid 
 |-  ( ph -> ( 1 ... z ) e. Fin )
153 elfznn 
 |-  ( j e. ( 1 ... z ) -> j e. NN )
154 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
155 154 ovolfsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
156 5 155 syl 
 |-  ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
157 156 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( abs o. - ) o. F ) ` j ) e. ( 0 [,) +oo ) )
158 153 157 sylan2 
 |-  ( ( ph /\ j e. ( 1 ... z ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. ( 0 [,) +oo ) )
159 elrege0 
 |-  ( ( ( ( abs o. - ) o. F ) ` j ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. F ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` j ) ) )
160 158 159 sylib 
 |-  ( ( ph /\ j e. ( 1 ... z ) ) -> ( ( ( ( abs o. - ) o. F ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. F ) ` j ) ) )
161 160 simpld 
 |-  ( ( ph /\ j e. ( 1 ... z ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. RR )
162 152 161 fsumrecl 
 |-  ( ph -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) e. RR )
163 162 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) e. RR )
164 163 rexrd 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) e. RR* )
165 154 4 ovolsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
166 5 165 syl 
 |-  ( ph -> S : NN --> ( 0 [,) +oo ) )
167 166 frnd 
 |-  ( ph -> ran S C_ ( 0 [,) +oo ) )
168 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
169 167 168 sstrdi 
 |-  ( ph -> ran S C_ RR )
170 ressxr 
 |-  RR C_ RR*
171 169 170 sstrdi 
 |-  ( ph -> ran S C_ RR* )
172 supxrcl 
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
173 171 172 syl 
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR* )
174 173 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sup ( ran S , RR* , < ) e. RR* )
175 149 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( B - A ) e. RR )
176 33 sselda 
 |-  ( ( ph /\ j e. ( ( G o. K ) " ( 1 ... M ) ) ) -> j e. NN )
177 168 157 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( abs o. - ) o. F ) ` j ) e. RR )
178 176 177 syldan 
 |-  ( ( ph /\ j e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. RR )
179 145 178 fsumrecl 
 |-  ( ph -> sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) e. RR )
180 179 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) e. RR )
181 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
182 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> F : NN --> ( RR X. RR ) )
183 5 181 182 sylancl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
184 73 111 sselid 
 |-  ( ph -> M e. NN )
185 26 184 ffvelcdmd 
 |-  ( ph -> ( K ` M ) e. U )
186 8 185 ffvelcdmd 
 |-  ( ph -> ( G ` ( K ` M ) ) e. NN )
187 183 186 ffvelcdmd 
 |-  ( ph -> ( F ` ( G ` ( K ` M ) ) ) e. ( RR X. RR ) )
188 xp2nd 
 |-  ( ( F ` ( G ` ( K ` M ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) e. RR )
189 187 188 syl 
 |-  ( ph -> ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) e. RR )
190 24 14 sselid 
 |-  ( ph -> C e. U )
191 8 190 ffvelcdmd 
 |-  ( ph -> ( G ` C ) e. NN )
192 183 191 ffvelcdmd 
 |-  ( ph -> ( F ` ( G ` C ) ) e. ( RR X. RR ) )
193 xp1st 
 |-  ( ( F ` ( G ` C ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` C ) ) ) e. RR )
194 192 193 syl 
 |-  ( ph -> ( 1st ` ( F ` ( G ` C ) ) ) e. RR )
195 189 194 resubcld 
 |-  ( ph -> ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) e. RR )
196 fveq2 
 |-  ( j = ( G ` ( K ` i ) ) -> ( ( ( abs o. - ) o. F ) ` j ) = ( ( ( abs o. - ) o. F ) ` ( G ` ( K ` i ) ) ) )
197 177 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( ( ( abs o. - ) o. F ) ` j ) e. CC )
198 176 197 syldan 
 |-  ( ( ph /\ j e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. CC )
199 196 52 141 58 198 fsumf1o 
 |-  ( ph -> sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) = sum_ i e. ( 1 ... M ) ( ( ( abs o. - ) o. F ) ` ( G ` ( K ` i ) ) ) )
200 8 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> G : U --> NN )
201 ffvelcdm 
 |-  ( ( K : NN --> U /\ i e. NN ) -> ( K ` i ) e. U )
202 26 55 201 syl2an 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) e. U )
203 200 202 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( K ` i ) ) e. NN )
204 154 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( G ` ( K ` i ) ) e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( G ` ( K ` i ) ) ) = ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
205 5 203 204 syl2an2r 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( ( abs o. - ) o. F ) ` ( G ` ( K ` i ) ) ) = ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
206 205 sumeq2dv 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( ( ( abs o. - ) o. F ) ` ( G ` ( K ` i ) ) ) = sum_ i e. ( 1 ... M ) ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
207 183 adantr 
 |-  ( ( ph /\ i e. NN ) -> F : NN --> ( RR X. RR ) )
208 8 adantr 
 |-  ( ( ph /\ i e. NN ) -> G : U --> NN )
209 26 ffvelcdmda 
 |-  ( ( ph /\ i e. NN ) -> ( K ` i ) e. U )
210 208 209 ffvelcdmd 
 |-  ( ( ph /\ i e. NN ) -> ( G ` ( K ` i ) ) e. NN )
211 207 210 ffvelcdmd 
 |-  ( ( ph /\ i e. NN ) -> ( F ` ( G ` ( K ` i ) ) ) e. ( RR X. RR ) )
212 xp2nd 
 |-  ( ( F ` ( G ` ( K ` i ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
213 211 212 syl 
 |-  ( ( ph /\ i e. NN ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
214 55 213 sylan2 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
215 214 recnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. CC )
216 183 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> F : NN --> ( RR X. RR ) )
217 216 203 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( F ` ( G ` ( K ` i ) ) ) e. ( RR X. RR ) )
218 xp1st 
 |-  ( ( F ` ( G ` ( K ` i ) ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
219 217 218 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
220 219 recnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) e. CC )
221 52 215 220 fsumsub 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) = ( sum_ i e. ( 1 ... M ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
222 fzfid 
 |-  ( ph -> ( 1 ... ( M - 1 ) ) e. Fin )
223 elfznn 
 |-  ( i e. ( 1 ... ( M - 1 ) ) -> i e. NN )
224 223 213 sylan2 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
225 222 224 fsumrecl 
 |-  ( ph -> sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR )
226 225 recnd 
 |-  ( ph -> sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. CC )
227 189 recnd 
 |-  ( ph -> ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) e. CC )
228 75 111 sselid 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
229 2fveq3 
 |-  ( i = M -> ( G ` ( K ` i ) ) = ( G ` ( K ` M ) ) )
230 229 fveq2d 
 |-  ( i = M -> ( F ` ( G ` ( K ` i ) ) ) = ( F ` ( G ` ( K ` M ) ) ) )
231 230 fveq2d 
 |-  ( i = M -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) )
232 228 215 231 fsumm1 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) + ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) ) )
233 226 227 232 comraddd 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) = ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
234 2fveq3 
 |-  ( i = 1 -> ( G ` ( K ` i ) ) = ( G ` ( K ` 1 ) ) )
235 234 fveq2d 
 |-  ( i = 1 -> ( F ` ( G ` ( K ` i ) ) ) = ( F ` ( G ` ( K ` 1 ) ) ) )
236 235 fveq2d 
 |-  ( i = 1 -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 1st ` ( F ` ( G ` ( K ` 1 ) ) ) ) )
237 228 220 236 fsum1p 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = ( ( 1st ` ( F ` ( G ` ( K ` 1 ) ) ) ) + sum_ i e. ( ( 1 + 1 ) ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
238 21 15 22 14 algr0 
 |-  ( ph -> ( K ` 1 ) = C )
239 238 fveq2d 
 |-  ( ph -> ( G ` ( K ` 1 ) ) = ( G ` C ) )
240 239 fveq2d 
 |-  ( ph -> ( F ` ( G ` ( K ` 1 ) ) ) = ( F ` ( G ` C ) ) )
241 240 fveq2d 
 |-  ( ph -> ( 1st ` ( F ` ( G ` ( K ` 1 ) ) ) ) = ( 1st ` ( F ` ( G ` C ) ) ) )
242 22 peano2zd 
 |-  ( ph -> ( 1 + 1 ) e. ZZ )
243 184 nnzd 
 |-  ( ph -> M e. ZZ )
244 1z 
 |-  1 e. ZZ
245 fzp1ss 
 |-  ( 1 e. ZZ -> ( ( 1 + 1 ) ... M ) C_ ( 1 ... M ) )
246 244 245 mp1i 
 |-  ( ph -> ( ( 1 + 1 ) ... M ) C_ ( 1 ... M ) )
247 246 sselda 
 |-  ( ( ph /\ i e. ( ( 1 + 1 ) ... M ) ) -> i e. ( 1 ... M ) )
248 247 220 syldan 
 |-  ( ( ph /\ i e. ( ( 1 + 1 ) ... M ) ) -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) e. CC )
249 2fveq3 
 |-  ( i = ( j + 1 ) -> ( G ` ( K ` i ) ) = ( G ` ( K ` ( j + 1 ) ) ) )
250 249 fveq2d 
 |-  ( i = ( j + 1 ) -> ( F ` ( G ` ( K ` i ) ) ) = ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) )
251 250 fveq2d 
 |-  ( i = ( j + 1 ) -> ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) )
252 22 242 243 248 251 fsumshftm 
 |-  ( ph -> sum_ i e. ( ( 1 + 1 ) ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = sum_ j e. ( ( ( 1 + 1 ) - 1 ) ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) )
253 ax-1cn 
 |-  1 e. CC
254 253 253 pncan3oi 
 |-  ( ( 1 + 1 ) - 1 ) = 1
255 254 oveq1i 
 |-  ( ( ( 1 + 1 ) - 1 ) ... ( M - 1 ) ) = ( 1 ... ( M - 1 ) )
256 255 sumeq1i 
 |-  sum_ j e. ( ( ( 1 + 1 ) - 1 ) ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) = sum_ j e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) )
257 fvoveq1 
 |-  ( j = i -> ( K ` ( j + 1 ) ) = ( K ` ( i + 1 ) ) )
258 257 fveq2d 
 |-  ( j = i -> ( G ` ( K ` ( j + 1 ) ) ) = ( G ` ( K ` ( i + 1 ) ) ) )
259 258 fveq2d 
 |-  ( j = i -> ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) = ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) )
260 259 fveq2d 
 |-  ( j = i -> ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) = ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) )
261 260 cbvsumv 
 |-  sum_ j e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) = sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) )
262 256 261 eqtri 
 |-  sum_ j e. ( ( ( 1 + 1 ) - 1 ) ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( j + 1 ) ) ) ) ) = sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) )
263 252 262 eqtrdi 
 |-  ( ph -> sum_ i e. ( ( 1 + 1 ) ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) )
264 241 263 oveq12d 
 |-  ( ph -> ( ( 1st ` ( F ` ( G ` ( K ` 1 ) ) ) ) + sum_ i e. ( ( 1 + 1 ) ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) = ( ( 1st ` ( F ` ( G ` C ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) )
265 237 264 eqtrd 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) = ( ( 1st ` ( F ` ( G ` C ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) )
266 233 265 oveq12d 
 |-  ( ph -> ( sum_ i e. ( 1 ... M ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... M ) ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) = ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) ) - ( ( 1st ` ( F ` ( G ` C ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
267 194 recnd 
 |-  ( ph -> ( 1st ` ( F ` ( G ` C ) ) ) e. CC )
268 peano2nn 
 |-  ( i e. NN -> ( i + 1 ) e. NN )
269 ffvelcdm 
 |-  ( ( K : NN --> U /\ ( i + 1 ) e. NN ) -> ( K ` ( i + 1 ) ) e. U )
270 26 268 269 syl2an 
 |-  ( ( ph /\ i e. NN ) -> ( K ` ( i + 1 ) ) e. U )
271 208 270 ffvelcdmd 
 |-  ( ( ph /\ i e. NN ) -> ( G ` ( K ` ( i + 1 ) ) ) e. NN )
272 207 271 ffvelcdmd 
 |-  ( ( ph /\ i e. NN ) -> ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) e. ( RR X. RR ) )
273 xp1st 
 |-  ( ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) e. RR )
274 272 273 syl 
 |-  ( ( ph /\ i e. NN ) -> ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) e. RR )
275 223 274 sylan2 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) e. RR )
276 222 275 fsumrecl 
 |-  ( ph -> sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) e. RR )
277 276 recnd 
 |-  ( ph -> sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) e. CC )
278 227 226 267 277 addsub4d 
 |-  ( ph -> ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) ) - ( ( 1st ` ( F ` ( G ` C ) ) ) + sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) = ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
279 221 266 278 3eqtrd 
 |-  ( ph -> sum_ i e. ( 1 ... M ) ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - ( 1st ` ( F ` ( G ` ( K ` i ) ) ) ) ) = ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
280 199 206 279 3eqtrd 
 |-  ( ph -> sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) = ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
281 280 179 eqeltrrd 
 |-  ( ph -> ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) e. RR )
282 fveq2 
 |-  ( n = M -> ( K ` n ) = ( K ` M ) )
283 282 eleq2d 
 |-  ( n = M -> ( B e. ( K ` n ) <-> B e. ( K ` M ) ) )
284 283 16 elrab2 
 |-  ( M e. W <-> ( M e. NN /\ B e. ( K ` M ) ) )
285 111 284 sylib 
 |-  ( ph -> ( M e. NN /\ B e. ( K ` M ) ) )
286 285 simprd 
 |-  ( ph -> B e. ( K ` M ) )
287 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ ( K ` M ) e. U ) -> ( B e. ( K ` M ) <-> ( B e. RR /\ ( 1st ` ( F ` ( G ` ( K ` M ) ) ) ) < B /\ B < ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) ) ) )
288 185 287 mpdan 
 |-  ( ph -> ( B e. ( K ` M ) <-> ( B e. RR /\ ( 1st ` ( F ` ( G ` ( K ` M ) ) ) ) < B /\ B < ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) ) ) )
289 286 288 mpbid 
 |-  ( ph -> ( B e. RR /\ ( 1st ` ( F ` ( G ` ( K ` M ) ) ) ) < B /\ B < ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) ) )
290 289 simp3d 
 |-  ( ph -> B < ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) )
291 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ C e. U ) -> ( A e. C <-> ( A e. RR /\ ( 1st ` ( F ` ( G ` C ) ) ) < A /\ A < ( 2nd ` ( F ` ( G ` C ) ) ) ) ) )
292 190 291 mpdan 
 |-  ( ph -> ( A e. C <-> ( A e. RR /\ ( 1st ` ( F ` ( G ` C ) ) ) < A /\ A < ( 2nd ` ( F ` ( G ` C ) ) ) ) ) )
293 13 292 mpbid 
 |-  ( ph -> ( A e. RR /\ ( 1st ` ( F ` ( G ` C ) ) ) < A /\ A < ( 2nd ` ( F ` ( G ` C ) ) ) ) )
294 293 simp2d 
 |-  ( ph -> ( 1st ` ( F ` ( G ` C ) ) ) < A )
295 2 194 189 1 290 294 lt2subd 
 |-  ( ph -> ( B - A ) < ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) )
296 149 195 295 ltled 
 |-  ( ph -> ( B - A ) <_ ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) )
297 223 adantl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. NN )
298 simpr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. ( 1 ... ( M - 1 ) ) )
299 243 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> M e. ZZ )
300 elfzm11 
 |-  ( ( 1 e. ZZ /\ M e. ZZ ) -> ( i e. ( 1 ... ( M - 1 ) ) <-> ( i e. ZZ /\ 1 <_ i /\ i < M ) ) )
301 244 299 300 sylancr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i e. ( 1 ... ( M - 1 ) ) <-> ( i e. ZZ /\ 1 <_ i /\ i < M ) ) )
302 298 301 mpbid 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i e. ZZ /\ 1 <_ i /\ i < M ) )
303 302 simp3d 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i < M )
304 297 nnred 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> i e. RR )
305 112 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> M e. RR )
306 304 305 ltnled 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i < M <-> -. M <_ i ) )
307 303 306 mpbid 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> -. M <_ i )
308 infssuzle 
 |-  ( ( W C_ ( ZZ>= ` 1 ) /\ i e. W ) -> inf ( W , RR , < ) <_ i )
309 75 308 mpan 
 |-  ( i e. W -> inf ( W , RR , < ) <_ i )
310 17 309 eqbrtrid 
 |-  ( i e. W -> M <_ i )
311 307 310 nsyl 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> -. i e. W )
312 297 311 jca 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( i e. NN /\ -. i e. W ) )
313 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 
 |-  ( ( ph /\ ( i e. NN /\ -. i e. W ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B )
314 312 313 syldan 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B )
315 314 iftrued 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> if ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) , B ) = ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) )
316 2fveq3 
 |-  ( t = ( K ` i ) -> ( F ` ( G ` t ) ) = ( F ` ( G ` ( K ` i ) ) ) )
317 316 fveq2d 
 |-  ( t = ( K ` i ) -> ( 2nd ` ( F ` ( G ` t ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) )
318 317 breq1d 
 |-  ( t = ( K ` i ) -> ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B <-> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B ) )
319 318 317 ifbieq1d 
 |-  ( t = ( K ` i ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) = if ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) , B ) )
320 fveq2 
 |-  ( t = ( K ` i ) -> ( H ` t ) = ( H ` ( K ` i ) ) )
321 319 320 eleq12d 
 |-  ( t = ( K ` i ) -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) <-> if ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) , B ) e. ( H ` ( K ` i ) ) ) )
322 12 ralrimiva 
 |-  ( ph -> A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
323 322 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
324 ffvelcdm 
 |-  ( ( K : NN --> T /\ i e. NN ) -> ( K ` i ) e. T )
325 23 223 324 syl2an 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( K ` i ) e. T )
326 321 323 325 rspcdva 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> if ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) , B ) e. ( H ` ( K ` i ) ) )
327 315 326 eqeltrrd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. ( H ` ( K ` i ) ) )
328 21 15 22 14 11 algrp1 
 |-  ( ( ph /\ i e. NN ) -> ( K ` ( i + 1 ) ) = ( H ` ( K ` i ) ) )
329 223 328 sylan2 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( K ` ( i + 1 ) ) = ( H ` ( K ` i ) ) )
330 327 329 eleqtrrd 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. ( K ` ( i + 1 ) ) )
331 223 270 sylan2 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( K ` ( i + 1 ) ) e. U )
332 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ ( K ` ( i + 1 ) ) e. U ) -> ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. ( K ` ( i + 1 ) ) <-> ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
333 331 332 syldan 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. ( K ` ( i + 1 ) ) <-> ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
334 330 333 mpbid 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) )
335 334 simp2d 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) )
336 275 224 335 ltled 
 |-  ( ( ph /\ i e. ( 1 ... ( M - 1 ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) <_ ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) )
337 222 275 224 336 fsumle 
 |-  ( ph -> sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) <_ sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) )
338 225 276 subge0d 
 |-  ( ph -> ( 0 <_ ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) <-> sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) <_ sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) ) )
339 337 338 mpbird 
 |-  ( ph -> 0 <_ ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) )
340 225 276 resubcld 
 |-  ( ph -> ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) e. RR )
341 195 340 addge01d 
 |-  ( ph -> ( 0 <_ ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) <-> ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) <_ ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) ) )
342 339 341 mpbid 
 |-  ( ph -> ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) <_ ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
343 149 195 281 296 342 letrd 
 |-  ( ph -> ( B - A ) <_ ( ( ( 2nd ` ( F ` ( G ` ( K ` M ) ) ) ) - ( 1st ` ( F ` ( G ` C ) ) ) ) + ( sum_ i e. ( 1 ... ( M - 1 ) ) ( 2nd ` ( F ` ( G ` ( K ` i ) ) ) ) - sum_ i e. ( 1 ... ( M - 1 ) ) ( 1st ` ( F ` ( G ` ( K ` ( i + 1 ) ) ) ) ) ) ) )
344 343 280 breqtrrd 
 |-  ( ph -> ( B - A ) <_ sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) )
345 344 adantr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( B - A ) <_ sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) )
346 fzfid 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( 1 ... z ) e. Fin )
347 161 adantlr 
 |-  ( ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) /\ j e. ( 1 ... z ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. RR )
348 160 simprd 
 |-  ( ( ph /\ j e. ( 1 ... z ) ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` j ) )
349 348 adantlr 
 |-  ( ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) /\ j e. ( 1 ... z ) ) -> 0 <_ ( ( ( abs o. - ) o. F ) ` j ) )
350 33 adantr 
 |-  ( ( ph /\ z e. NN ) -> ( ( G o. K ) " ( 1 ... M ) ) C_ NN )
351 350 sselda 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> y e. NN )
352 351 nnred 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> y e. RR )
353 40 ad2antlr 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> z e. RR )
354 ltle 
 |-  ( ( y e. RR /\ z e. RR ) -> ( y < z -> y <_ z ) )
355 352 353 354 syl2anc 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( y < z -> y <_ z ) )
356 351 21 eleqtrdi 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> y e. ( ZZ>= ` 1 ) )
357 nnz 
 |-  ( z e. NN -> z e. ZZ )
358 357 ad2antlr 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> z e. ZZ )
359 elfz5 
 |-  ( ( y e. ( ZZ>= ` 1 ) /\ z e. ZZ ) -> ( y e. ( 1 ... z ) <-> y <_ z ) )
360 356 358 359 syl2anc 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( y e. ( 1 ... z ) <-> y <_ z ) )
361 355 360 sylibrd 
 |-  ( ( ( ph /\ z e. NN ) /\ y e. ( ( G o. K ) " ( 1 ... M ) ) ) -> ( y < z -> y e. ( 1 ... z ) ) )
362 361 ralimdva 
 |-  ( ( ph /\ z e. NN ) -> ( A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z -> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y e. ( 1 ... z ) ) )
363 362 impr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y e. ( 1 ... z ) )
364 dfss3 
 |-  ( ( ( G o. K ) " ( 1 ... M ) ) C_ ( 1 ... z ) <-> A. y e. ( ( G o. K ) " ( 1 ... M ) ) y e. ( 1 ... z ) )
365 363 364 sylibr 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( ( G o. K ) " ( 1 ... M ) ) C_ ( 1 ... z ) )
366 346 347 349 365 fsumless 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( ( G o. K ) " ( 1 ... M ) ) ( ( ( abs o. - ) o. F ) ` j ) <_ sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) )
367 175 180 163 345 366 letrd 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( B - A ) <_ sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) )
368 eqidd 
 |-  ( ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) /\ j e. ( 1 ... z ) ) -> ( ( ( abs o. - ) o. F ) ` j ) = ( ( ( abs o. - ) o. F ) ` j ) )
369 simprl 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> z e. NN )
370 369 21 eleqtrdi 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> z e. ( ZZ>= ` 1 ) )
371 347 recnd 
 |-  ( ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) /\ j e. ( 1 ... z ) ) -> ( ( ( abs o. - ) o. F ) ` j ) e. CC )
372 368 370 371 fsumser 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` z ) )
373 4 fveq1i 
 |-  ( S ` z ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` z )
374 372 373 eqtr4di 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) = ( S ` z ) )
375 166 ffnd 
 |-  ( ph -> S Fn NN )
376 fnfvelrn 
 |-  ( ( S Fn NN /\ z e. NN ) -> ( S ` z ) e. ran S )
377 375 369 376 syl2an2r 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( S ` z ) e. ran S )
378 supxrub 
 |-  ( ( ran S C_ RR* /\ ( S ` z ) e. ran S ) -> ( S ` z ) <_ sup ( ran S , RR* , < ) )
379 171 377 378 syl2an2r 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( S ` z ) <_ sup ( ran S , RR* , < ) )
380 374 379 eqbrtrd 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> sum_ j e. ( 1 ... z ) ( ( ( abs o. - ) o. F ) ` j ) <_ sup ( ran S , RR* , < ) )
381 151 164 174 367 380 xrletrd 
 |-  ( ( ph /\ ( z e. NN /\ A. y e. ( ( G o. K ) " ( 1 ... M ) ) y < z ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) )
382 148 381 rexlimddv 
 |-  ( ph -> ( B - A ) <_ sup ( ran S , RR* , < ) )