Metamath Proof Explorer

Theorem ovolicc2lem3

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

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 ) }
Assertion ovolicc2lem3 
|- ( ( ph /\ ( N e. { n e. NN | A. m e. W n <_ m } /\ P e. { n e. NN | A. m e. W n <_ m } ) ) -> ( N = P <-> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` P ) ) ) ) ) )

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 2fveq3 
 |-  ( y = k -> ( G ` ( K ` y ) ) = ( G ` ( K ` k ) ) )
18 17 fveq2d 
 |-  ( y = k -> ( F ` ( G ` ( K ` y ) ) ) = ( F ` ( G ` ( K ` k ) ) ) )
19 18 fveq2d 
 |-  ( y = k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) )
20 2fveq3 
 |-  ( y = N -> ( G ` ( K ` y ) ) = ( G ` ( K ` N ) ) )
21 20 fveq2d 
 |-  ( y = N -> ( F ` ( G ` ( K ` y ) ) ) = ( F ` ( G ` ( K ` N ) ) ) )
22 21 fveq2d 
 |-  ( y = N -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) )
23 2fveq3 
 |-  ( y = P -> ( G ` ( K ` y ) ) = ( G ` ( K ` P ) ) )
24 23 fveq2d 
 |-  ( y = P -> ( F ` ( G ` ( K ` y ) ) ) = ( F ` ( G ` ( K ` P ) ) ) )
25 24 fveq2d 
 |-  ( y = P -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` P ) ) ) ) )
26 ssrab2 
 |-  { n e. NN | A. m e. W n <_ m } C_ NN
27 nnssre 
 |-  NN C_ RR
28 26 27 sstri 
 |-  { n e. NN | A. m e. W n <_ m } C_ RR
29 26 sseli 
 |-  ( y e. { n e. NN | A. m e. W n <_ m } -> y e. NN )
30 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
31 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> F : NN --> ( RR X. RR ) )
32 5 30 31 sylancl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
33 32 adantr 
 |-  ( ( ph /\ y e. NN ) -> F : NN --> ( RR X. RR ) )
34 8 adantr 
 |-  ( ( ph /\ y e. NN ) -> G : U --> NN )
35 nnuz 
 |-  NN = ( ZZ>= ` 1 )
36 1zzd 
 |-  ( ph -> 1 e. ZZ )
37 35 15 36 14 11 algrf 
 |-  ( ph -> K : NN --> T )
38 37 adantr 
 |-  ( ( ph /\ y e. NN ) -> K : NN --> T )
39 10 ssrab3 
 |-  T C_ U
40 fss 
 |-  ( ( K : NN --> T /\ T C_ U ) -> K : NN --> U )
41 38 39 40 sylancl 
 |-  ( ( ph /\ y e. NN ) -> K : NN --> U )
42 ffvelrn 
 |-  ( ( K : NN --> U /\ y e. NN ) -> ( K ` y ) e. U )
43 41 42 sylancom 
 |-  ( ( ph /\ y e. NN ) -> ( K ` y ) e. U )
44 34 43 ffvelrnd 
 |-  ( ( ph /\ y e. NN ) -> ( G ` ( K ` y ) ) e. NN )
45 33 44 ffvelrnd 
 |-  ( ( ph /\ y e. NN ) -> ( F ` ( G ` ( K ` y ) ) ) e. ( RR X. RR ) )
46 xp2nd 
 |-  ( ( F ` ( G ` ( K ` y ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) e. RR )
47 45 46 syl 
 |-  ( ( ph /\ y e. NN ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) e. RR )
48 29 47 sylan2 
 |-  ( ( ph /\ y e. { n e. NN | A. m e. W n <_ m } ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) e. RR )
49 26 sseli 
 |-  ( k e. { n e. NN | A. m e. W n <_ m } -> k e. NN )
50 49 ad2antll 
 |-  ( ( ph /\ ( y e. { n e. NN | A. m e. W n <_ m } /\ k e. { n e. NN | A. m e. W n <_ m } ) ) -> k e. NN )
51 29 anim2i 
 |-  ( ( ph /\ y e. { n e. NN | A. m e. W n <_ m } ) -> ( ph /\ y e. NN ) )
52 51 adantrr 
 |-  ( ( ph /\ ( y e. { n e. NN | A. m e. W n <_ m } /\ k e. { n e. NN | A. m e. W n <_ m } ) ) -> ( ph /\ y e. NN ) )
53 breq1 
 |-  ( n = k -> ( n <_ m <-> k <_ m ) )
54 53 ralbidv 
 |-  ( n = k -> ( A. m e. W n <_ m <-> A. m e. W k <_ m ) )
55 54 elrab 
 |-  ( k e. { n e. NN | A. m e. W n <_ m } <-> ( k e. NN /\ A. m e. W k <_ m ) )
56 55 simprbi 
 |-  ( k e. { n e. NN | A. m e. W n <_ m } -> A. m e. W k <_ m )
57 56 ad2antll 
 |-  ( ( ph /\ ( y e. { n e. NN | A. m e. W n <_ m } /\ k e. { n e. NN | A. m e. W n <_ m } ) ) -> A. m e. W k <_ m )
58 breq1 
 |-  ( x = 1 -> ( x <_ m <-> 1 <_ m ) )
59 58 ralbidv 
 |-  ( x = 1 -> ( A. m e. W x <_ m <-> A. m e. W 1 <_ m ) )
60 breq2 
 |-  ( x = 1 -> ( y < x <-> y < 1 ) )
61 2fveq3 
 |-  ( x = 1 -> ( G ` ( K ` x ) ) = ( G ` ( K ` 1 ) ) )
62 61 fveq2d 
 |-  ( x = 1 -> ( F ` ( G ` ( K ` x ) ) ) = ( F ` ( G ` ( K ` 1 ) ) ) )
63 62 fveq2d 
 |-  ( x = 1 -> ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) )
64 63 breq2d 
 |-  ( x = 1 -> ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) <-> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) )
65 60 64 imbi12d 
 |-  ( x = 1 -> ( ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) <-> ( y < 1 -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) ) )
66 59 65 imbi12d 
 |-  ( x = 1 -> ( ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) <-> ( A. m e. W 1 <_ m -> ( y < 1 -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) ) ) )
67 66 imbi2d 
 |-  ( x = 1 -> ( ( ( ph /\ y e. NN ) -> ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) ) <-> ( ( ph /\ y e. NN ) -> ( A. m e. W 1 <_ m -> ( y < 1 -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) ) ) ) )
68 breq1 
 |-  ( x = k -> ( x <_ m <-> k <_ m ) )
69 68 ralbidv 
 |-  ( x = k -> ( A. m e. W x <_ m <-> A. m e. W k <_ m ) )
70 breq2 
 |-  ( x = k -> ( y < x <-> y < k ) )
71 2fveq3 
 |-  ( x = k -> ( G ` ( K ` x ) ) = ( G ` ( K ` k ) ) )
72 71 fveq2d 
 |-  ( x = k -> ( F ` ( G ` ( K ` x ) ) ) = ( F ` ( G ` ( K ` k ) ) ) )
73 72 fveq2d 
 |-  ( x = k -> ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) )
74 73 breq2d 
 |-  ( x = k -> ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) <-> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) )
75 70 74 imbi12d 
 |-  ( x = k -> ( ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) <-> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) )
76 69 75 imbi12d 
 |-  ( x = k -> ( ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) <-> ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) )
77 76 imbi2d 
 |-  ( x = k -> ( ( ( ph /\ y e. NN ) -> ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) ) <-> ( ( ph /\ y e. NN ) -> ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) ) )
78 breq1 
 |-  ( x = ( k + 1 ) -> ( x <_ m <-> ( k + 1 ) <_ m ) )
79 78 ralbidv 
 |-  ( x = ( k + 1 ) -> ( A. m e. W x <_ m <-> A. m e. W ( k + 1 ) <_ m ) )
80 breq2 
 |-  ( x = ( k + 1 ) -> ( y < x <-> y < ( k + 1 ) ) )
81 2fveq3 
 |-  ( x = ( k + 1 ) -> ( G ` ( K ` x ) ) = ( G ` ( K ` ( k + 1 ) ) ) )
82 81 fveq2d 
 |-  ( x = ( k + 1 ) -> ( F ` ( G ` ( K ` x ) ) ) = ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) )
83 82 fveq2d 
 |-  ( x = ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) )
84 83 breq2d 
 |-  ( x = ( k + 1 ) -> ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) <-> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
85 80 84 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) <-> ( y < ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
86 79 85 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) <-> ( A. m e. W ( k + 1 ) <_ m -> ( y < ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) ) )
87 86 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ( ph /\ y e. NN ) -> ( A. m e. W x <_ m -> ( y < x -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` x ) ) ) ) ) ) ) <-> ( ( ph /\ y e. NN ) -> ( A. m e. W ( k + 1 ) <_ m -> ( y < ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) ) ) )
88 nnnlt1 
 |-  ( y e. NN -> -. y < 1 )
89 88 adantl 
 |-  ( ( ph /\ y e. NN ) -> -. y < 1 )
90 89 pm2.21d 
 |-  ( ( ph /\ y e. NN ) -> ( y < 1 -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) )
91 90 a1d 
 |-  ( ( ph /\ y e. NN ) -> ( A. m e. W 1 <_ m -> ( y < 1 -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` 1 ) ) ) ) ) ) )
92 nnre 
 |-  ( k e. NN -> k e. RR )
93 92 adantr 
 |-  ( ( k e. NN /\ m e. W ) -> k e. RR )
94 93 lep1d 
 |-  ( ( k e. NN /\ m e. W ) -> k <_ ( k + 1 ) )
95 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
96 93 95 syl 
 |-  ( ( k e. NN /\ m e. W ) -> ( k + 1 ) e. RR )
97 16 ssrab3 
 |-  W C_ NN
98 97 27 sstri 
 |-  W C_ RR
99 98 sseli 
 |-  ( m e. W -> m e. RR )
100 99 adantl 
 |-  ( ( k e. NN /\ m e. W ) -> m e. RR )
101 letr 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR /\ m e. RR ) -> ( ( k <_ ( k + 1 ) /\ ( k + 1 ) <_ m ) -> k <_ m ) )
102 93 96 100 101 syl3anc 
 |-  ( ( k e. NN /\ m e. W ) -> ( ( k <_ ( k + 1 ) /\ ( k + 1 ) <_ m ) -> k <_ m ) )
103 94 102 mpand 
 |-  ( ( k e. NN /\ m e. W ) -> ( ( k + 1 ) <_ m -> k <_ m ) )
104 103 ralimdva 
 |-  ( k e. NN -> ( A. m e. W ( k + 1 ) <_ m -> A. m e. W k <_ m ) )
105 104 imim1d 
 |-  ( k e. NN -> ( ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) -> ( A. m e. W ( k + 1 ) <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) )
106 105 adantl 
 |-  ( ( ( ph /\ y e. NN ) /\ k e. NN ) -> ( ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) -> ( A. m e. W ( k + 1 ) <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) )
107 simplr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> y e. NN )
108 simprl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> k e. NN )
109 nnleltp1 
 |-  ( ( y e. NN /\ k e. NN ) -> ( y <_ k <-> y < ( k + 1 ) ) )
110 107 108 109 syl2anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y <_ k <-> y < ( k + 1 ) ) )
111 107 nnred 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> y e. RR )
112 108 nnred 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> k e. RR )
113 111 112 leloed 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y <_ k <-> ( y < k \/ y = k ) ) )
114 110 113 bitr3d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y < ( k + 1 ) <-> ( y < k \/ y = k ) ) )
115 simpll 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ph )
116 ltp1 
 |-  ( k e. RR -> k < ( k + 1 ) )
117 ltnle 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR ) -> ( k < ( k + 1 ) <-> -. ( k + 1 ) <_ k ) )
118 95 117 mpdan 
 |-  ( k e. RR -> ( k < ( k + 1 ) <-> -. ( k + 1 ) <_ k ) )
119 116 118 mpbid 
 |-  ( k e. RR -> -. ( k + 1 ) <_ k )
120 112 119 syl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> -. ( k + 1 ) <_ k )
121 breq2 
 |-  ( m = k -> ( ( k + 1 ) <_ m <-> ( k + 1 ) <_ k ) )
122 121 rspccv 
 |-  ( A. m e. W ( k + 1 ) <_ m -> ( k e. W -> ( k + 1 ) <_ k ) )
123 122 ad2antll 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( k e. W -> ( k + 1 ) <_ k ) )
124 120 123 mtod 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> -. k e. W )
125 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 
 |-  ( ( ph /\ ( k e. NN /\ -. k e. W ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B )
126 115 108 124 125 syl12anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B )
127 126 iftrued 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> if ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) , B ) = ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) )
128 2fveq3 
 |-  ( t = ( K ` k ) -> ( F ` ( G ` t ) ) = ( F ` ( G ` ( K ` k ) ) ) )
129 128 fveq2d 
 |-  ( t = ( K ` k ) -> ( 2nd ` ( F ` ( G ` t ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) )
130 129 breq1d 
 |-  ( t = ( K ` k ) -> ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B <-> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B ) )
131 130 129 ifbieq1d 
 |-  ( t = ( K ` k ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) = if ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) , B ) )
132 fveq2 
 |-  ( t = ( K ` k ) -> ( H ` t ) = ( H ` ( K ` k ) ) )
133 131 132 eleq12d 
 |-  ( t = ( K ` k ) -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) <-> if ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) , B ) e. ( H ` ( K ` k ) ) ) )
134 12 ralrimiva 
 |-  ( ph -> A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
135 134 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
136 37 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> K : NN --> T )
137 136 108 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( K ` k ) e. T )
138 133 135 137 rspcdva 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> if ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) <_ B , ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) , B ) e. ( H ` ( K ` k ) ) )
139 127 138 eqeltrrd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. ( H ` ( K ` k ) ) )
140 35 15 36 14 11 algrp1 
 |-  ( ( ph /\ k e. NN ) -> ( K ` ( k + 1 ) ) = ( H ` ( K ` k ) ) )
141 140 ad2ant2r 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( K ` ( k + 1 ) ) = ( H ` ( K ` k ) ) )
142 139 141 eleqtrrd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. ( K ` ( k + 1 ) ) )
143 136 39 40 sylancl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> K : NN --> U )
144 108 peano2nnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( k + 1 ) e. NN )
145 143 144 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( K ` ( k + 1 ) ) e. U )
146 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ ( K ` ( k + 1 ) ) e. U ) -> ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. ( K ` ( k + 1 ) ) <-> ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
147 115 145 146 syl2anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. ( K ` ( k + 1 ) ) <-> ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
148 142 147 mpbid 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR /\ ( 1st ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
149 148 simp3d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) )
150 47 adantr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) e. RR )
151 32 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> F : NN --> ( RR X. RR ) )
152 8 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> G : U --> NN )
153 143 108 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( K ` k ) e. U )
154 152 153 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( G ` ( K ` k ) ) e. NN )
155 151 154 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( F ` ( G ` ( K ` k ) ) ) e. ( RR X. RR ) )
156 xp2nd 
 |-  ( ( F ` ( G ` ( K ` k ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR )
157 155 156 syl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR )
158 152 145 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( G ` ( K ` ( k + 1 ) ) ) e. NN )
159 151 158 ffvelrnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) e. ( RR X. RR ) )
160 xp2nd 
 |-  ( ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) e. RR )
161 159 160 syl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) e. RR )
162 lttr 
 |-  ( ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) e. RR /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) e. RR /\ ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) e. RR ) -> ( ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
163 150 157 161 162 syl3anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) /\ ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
164 149 163 mpan2d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
165 164 imim2d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
166 165 com23 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y < k -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
167 19 breq1d 
 |-  ( y = k -> ( ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) <-> ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
168 149 167 syl5ibrcom 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y = k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) )
169 168 a1dd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y = k -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
170 166 169 jaod 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( y < k \/ y = k ) -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
171 114 170 sylbid 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( y < ( k + 1 ) -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
172 171 com23 
 |-  ( ( ( ph /\ y e. NN ) /\ ( k e. NN /\ A. m e. W ( k + 1 ) <_ m ) ) -> ( ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) -> ( y < ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) )
173 106 172 animpimp2impd 
 |-  ( k e. NN -> ( ( ( ph /\ y e. NN ) -> ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) -> ( ( ph /\ y e. NN ) -> ( A. m e. W ( k + 1 ) <_ m -> ( y < ( k + 1 ) -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` ( k + 1 ) ) ) ) ) ) ) ) ) )
174 67 77 87 77 91 173 nnind 
 |-  ( k e. NN -> ( ( ph /\ y e. NN ) -> ( A. m e. W k <_ m -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) ) ) )
175 50 52 57 174 syl3c 
 |-  ( ( ph /\ ( y e. { n e. NN | A. m e. W n <_ m } /\ k e. { n e. NN | A. m e. W n <_ m } ) ) -> ( y < k -> ( 2nd ` ( F ` ( G ` ( K ` y ) ) ) ) < ( 2nd ` ( F ` ( G ` ( K ` k ) ) ) ) ) )
176 19 22 25 28 48 175 eqord1 
 |-  ( ( ph /\ ( N e. { n e. NN | A. m e. W n <_ m } /\ P e. { n e. NN | A. m e. W n <_ m } ) ) -> ( N = P <-> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) = ( 2nd ` ( F ` ( G ` ( K ` P ) ) ) ) ) )