MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolicc2lem3 Unicode version

Theorem ovolicc2lem3 18931
Description: Lemma for ovolicc2 18934. (Contributed by Mario Carneiro, 14-Jun-2014.)
Hypotheses
Ref Expression
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
Ref Expression
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
) ) ) ) ) )
Distinct variable groups:    m, n, t, u, A    B, m, n, t, u    t, H    C, m, n, t    n, F, t    n, K, t, u    n, G, t   
m, W, n    ph, m, n, t    T, n, t   
n, N, t, u    U, n, t, u
Allowed substitution hints:    ph( u)    C( u)    P( u, t, m, n)    S( u, t, m, n)    T( u, m)    U( m)    F( u, m)    G( u, m)    H( u, m, n)    K( m)    N( m)    W( u, t)

Proof of Theorem ovolicc2lem3
Dummy variables  k  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5563 . . . . 5  |-  ( y  =  k  ->  ( K `  y )  =  ( K `  k ) )
21fveq2d 5567 . . . 4  |-  ( y  =  k  ->  ( G `  ( K `  y ) )  =  ( G `  ( K `  k )
) )
32fveq2d 5567 . . 3  |-  ( y  =  k  ->  ( F `  ( G `  ( K `  y
) ) )  =  ( F `  ( G `  ( K `  k ) ) ) )
43fveq2d 5567 . 2  |-  ( y  =  k  ->  ( 2nd `  ( F `  ( G `  ( K `
 y ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  k ) ) ) ) )
5 fveq2 5563 . . . . 5  |-  ( y  =  N  ->  ( K `  y )  =  ( K `  N ) )
65fveq2d 5567 . . . 4  |-  ( y  =  N  ->  ( G `  ( K `  y ) )  =  ( G `  ( K `  N )
) )
76fveq2d 5567 . . 3  |-  ( y  =  N  ->  ( F `  ( G `  ( K `  y
) ) )  =  ( F `  ( G `  ( K `  N ) ) ) )
87fveq2d 5567 . 2  |-  ( y  =  N  ->  ( 2nd `  ( F `  ( G `  ( K `
 y ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  N ) ) ) ) )
9 fveq2 5563 . . . . 5  |-  ( y  =  P  ->  ( K `  y )  =  ( K `  P ) )
109fveq2d 5567 . . . 4  |-  ( y  =  P  ->  ( G `  ( K `  y ) )  =  ( G `  ( K `  P )
) )
1110fveq2d 5567 . . 3  |-  ( y  =  P  ->  ( F `  ( G `  ( K `  y
) ) )  =  ( F `  ( G `  ( K `  P ) ) ) )
1211fveq2d 5567 . 2  |-  ( y  =  P  ->  ( 2nd `  ( F `  ( G `  ( K `
 y ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  P ) ) ) ) )
13 ssrab2 3292 . . 3  |-  { n  e.  NN  |  A. m  e.  W  n  <_  m }  C_  NN
14 nnssre 9795 . . 3  |-  NN  C_  RR
1513, 14sstri 3222 . 2  |-  { n  e.  NN  |  A. m  e.  W  n  <_  m }  C_  RR
1613sseli 3210 . . 3  |-  ( y  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  ->  y  e.  NN )
17 ovolicc2.5 . . . . . . 7  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
18 inss2 3424 . . . . . . 7  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
19 fss 5435 . . . . . . 7  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR ) )  ->  F : NN --> ( RR  X.  RR ) )
2017, 18, 19sylancl 643 . . . . . 6  |-  ( ph  ->  F : NN --> ( RR 
X.  RR ) )
2120adantr 451 . . . . 5  |-  ( (
ph  /\  y  e.  NN )  ->  F : NN
--> ( RR  X.  RR ) )
22 ovolicc2.8 . . . . . . 7  |-  ( ph  ->  G : U --> NN )
2322adantr 451 . . . . . 6  |-  ( (
ph  /\  y  e.  NN )  ->  G : U
--> NN )
24 nnuz 10310 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
25 ovolicc2.15 . . . . . . . . . 10  |-  K  =  seq  1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
26 1z 10100 . . . . . . . . . . 11  |-  1  e.  ZZ
2726a1i 10 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
28 ovolicc2.14 . . . . . . . . . 10  |-  ( ph  ->  C  e.  T )
29 ovolicc2.11 . . . . . . . . . 10  |-  ( ph  ->  H : T --> T )
3024, 25, 27, 28, 29algrf 12790 . . . . . . . . 9  |-  ( ph  ->  K : NN --> T )
3130adantr 451 . . . . . . . 8  |-  ( (
ph  /\  y  e.  NN )  ->  K : NN
--> T )
32 ovolicc2.10 . . . . . . . . 9  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
33 ssrab2 3292 . . . . . . . . 9  |-  { u  e.  U  |  (
u  i^i  ( A [,] B ) )  =/=  (/) }  C_  U
3432, 33eqsstri 3242 . . . . . . . 8  |-  T  C_  U
35 fss 5435 . . . . . . . 8  |-  ( ( K : NN --> T  /\  T  C_  U )  ->  K : NN --> U )
3631, 34, 35sylancl 643 . . . . . . 7  |-  ( (
ph  /\  y  e.  NN )  ->  K : NN
--> U )
37 ffvelrn 5701 . . . . . . 7  |-  ( ( K : NN --> U  /\  y  e.  NN )  ->  ( K `  y
)  e.  U )
3836, 37sylancom 648 . . . . . 6  |-  ( (
ph  /\  y  e.  NN )  ->  ( K `
 y )  e.  U )
39 ffvelrn 5701 . . . . . 6  |-  ( ( G : U --> NN  /\  ( K `  y )  e.  U )  -> 
( G `  ( K `  y )
)  e.  NN )
4023, 38, 39syl2anc 642 . . . . 5  |-  ( (
ph  /\  y  e.  NN )  ->  ( G `
 ( K `  y ) )  e.  NN )
41 ffvelrn 5701 . . . . 5  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 y ) )  e.  NN )  -> 
( F `  ( G `  ( K `  y ) ) )  e.  ( RR  X.  RR ) )
4221, 40, 41syl2anc 642 . . . 4  |-  ( (
ph  /\  y  e.  NN )  ->  ( F `
 ( G `  ( K `  y ) ) )  e.  ( RR  X.  RR ) )
43 xp2nd 6192 . . . 4  |-  ( ( F `  ( G `
 ( K `  y ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  y ) ) ) )  e.  RR )
4442, 43syl 15 . . 3  |-  ( (
ph  /\  y  e.  NN )  ->  ( 2nd `  ( F `  ( G `  ( K `  y ) ) ) )  e.  RR )
4516, 44sylan2 460 . 2  |-  ( (
ph  /\  y  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )  ->  ( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  e.  RR )
4613sseli 3210 . . . 4  |-  ( k  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  ->  k  e.  NN )
4746ad2antll 709 . . 3  |-  ( (
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 )
4816anim2i 552 . . . 4  |-  ( (
ph  /\  y  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )  ->  ( ph  /\  y  e.  NN )
)
4948adantrr 697 . . 3  |-  ( (
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 ) )
50 breq1 4063 . . . . . . 7  |-  ( n  =  k  ->  (
n  <_  m  <->  k  <_  m ) )
5150ralbidv 2597 . . . . . 6  |-  ( n  =  k  ->  ( A. m  e.  W  n  <_  m  <->  A. m  e.  W  k  <_  m ) )
5251elrab 2957 . . . . 5  |-  ( k  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  <->  ( k  e.  NN  /\  A. m  e.  W  k  <_  m ) )
5352simprbi 450 . . . 4  |-  ( k  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  ->  A. m  e.  W  k  <_  m )
5453ad2antll 709 . . 3  |-  ( (
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 )
55 breq1 4063 . . . . . . 7  |-  ( x  =  1  ->  (
x  <_  m  <->  1  <_  m ) )
5655ralbidv 2597 . . . . . 6  |-  ( x  =  1  ->  ( A. m  e.  W  x  <_  m  <->  A. m  e.  W  1  <_  m ) )
57 breq2 4064 . . . . . . 7  |-  ( x  =  1  ->  (
y  <  x  <->  y  <  1 ) )
58 fveq2 5563 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( K `  x )  =  ( K ` 
1 ) )
5958fveq2d 5567 . . . . . . . . . 10  |-  ( x  =  1  ->  ( G `  ( K `  x ) )  =  ( G `  ( K `  1 )
) )
6059fveq2d 5567 . . . . . . . . 9  |-  ( x  =  1  ->  ( F `  ( G `  ( K `  x
) ) )  =  ( F `  ( G `  ( K `  1 ) ) ) )
6160fveq2d 5567 . . . . . . . 8  |-  ( x  =  1  ->  ( 2nd `  ( F `  ( G `  ( K `
 x ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  1 ) ) ) ) )
6261breq2d 4072 . . . . . . 7  |-  ( x  =  1  ->  (
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  x
) ) ) )  <-> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  1
) ) ) ) ) )
6357, 62imbi12d 311 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
6456, 63imbi12d 311 . . . . 5  |-  ( 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 ) ) ) ) ) ) ) )
6564imbi2d 307 . . . 4  |-  ( 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 ) ) ) ) ) ) ) ) )
66 breq1 4063 . . . . . . 7  |-  ( x  =  k  ->  (
x  <_  m  <->  k  <_  m ) )
6766ralbidv 2597 . . . . . 6  |-  ( x  =  k  ->  ( A. m  e.  W  x  <_  m  <->  A. m  e.  W  k  <_  m ) )
68 breq2 4064 . . . . . . 7  |-  ( x  =  k  ->  (
y  <  x  <->  y  <  k ) )
69 fveq2 5563 . . . . . . . . . . 11  |-  ( x  =  k  ->  ( K `  x )  =  ( K `  k ) )
7069fveq2d 5567 . . . . . . . . . 10  |-  ( x  =  k  ->  ( G `  ( K `  x ) )  =  ( G `  ( K `  k )
) )
7170fveq2d 5567 . . . . . . . . 9  |-  ( x  =  k  ->  ( F `  ( G `  ( K `  x
) ) )  =  ( F `  ( G `  ( K `  k ) ) ) )
7271fveq2d 5567 . . . . . . . 8  |-  ( x  =  k  ->  ( 2nd `  ( F `  ( G `  ( K `
 x ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  k ) ) ) ) )
7372breq2d 4072 . . . . . . 7  |-  ( x  =  k  ->  (
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  x
) ) ) )  <-> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) ) ) )
7468, 73imbi12d 311 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
7567, 74imbi12d 311 . . . . 5  |-  ( 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 ) ) ) ) ) ) ) )
7675imbi2d 307 . . . 4  |-  ( 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 ) ) ) ) ) ) ) ) )
77 breq1 4063 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
x  <_  m  <->  ( k  +  1 )  <_  m ) )
7877ralbidv 2597 . . . . . 6  |-  ( x  =  ( k  +  1 )  ->  ( A. m  e.  W  x  <_  m  <->  A. m  e.  W  ( k  +  1 )  <_  m ) )
79 breq2 4064 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
y  <  x  <->  y  <  ( k  +  1 ) ) )
80 fveq2 5563 . . . . . . . . . . 11  |-  ( x  =  ( k  +  1 )  ->  ( K `  x )  =  ( K `  ( k  +  1 ) ) )
8180fveq2d 5567 . . . . . . . . . 10  |-  ( x  =  ( k  +  1 )  ->  ( G `  ( K `  x ) )  =  ( G `  ( K `  ( k  +  1 ) ) ) )
8281fveq2d 5567 . . . . . . . . 9  |-  ( x  =  ( k  +  1 )  ->  ( F `  ( G `  ( K `  x
) ) )  =  ( F `  ( G `  ( K `  ( k  +  1 ) ) ) ) )
8382fveq2d 5567 . . . . . . . 8  |-  ( x  =  ( k  +  1 )  ->  ( 2nd `  ( F `  ( G `  ( K `
 x ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  ( k  +  1 ) ) ) ) ) )
8483breq2d 4072 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  x
) ) ) )  <-> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) ) ) )
8579, 84imbi12d 311 . . . . . 6  |-  ( 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 ) ) ) ) ) ) ) )
8678, 85imbi12d 311 . . . . 5  |-  ( 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 ) ) ) ) ) ) ) ) )
8786imbi2d 307 . . . 4  |-  ( 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 9821 . . . . . . 7  |-  ( y  e.  NN  ->  -.  y  <  1 )
8988adantl 452 . . . . . 6  |-  ( (
ph  /\  y  e.  NN )  ->  -.  y  <  1 )
9089pm2.21d 98 . . . . 5  |-  ( (
ph  /\  y  e.  NN )  ->  ( y  <  1  ->  ( 2nd `  ( F `  ( G `  ( K `
 y ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 1 ) ) ) ) ) )
9190a1d 22 . . . 4  |-  ( (
ph  /\  y  e.  NN )  ->  ( A. m  e.  W  1  <_  m  ->  ( y  <  1  ->  ( 2nd `  ( F `  ( G `  ( K `  y ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  1 ) ) ) ) ) ) )
92 nnre 9798 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
9392adantr 451 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  k  e.  RR )
9493lep1d 9733 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  k  <_  ( k  +  1 ) )
95 peano2re 9030 . . . . . . . . . . . . 13  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
9693, 95syl 15 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  ( k  +  1 )  e.  RR )
97 ovolicc2.16 . . . . . . . . . . . . . . . 16  |-  W  =  { n  e.  NN  |  B  e.  ( K `  n ) }
98 ssrab2 3292 . . . . . . . . . . . . . . . 16  |-  { n  e.  NN  |  B  e.  ( K `  n
) }  C_  NN
9997, 98eqsstri 3242 . . . . . . . . . . . . . . 15  |-  W  C_  NN
10099, 14sstri 3222 . . . . . . . . . . . . . 14  |-  W  C_  RR
101100sseli 3210 . . . . . . . . . . . . 13  |-  ( m  e.  W  ->  m  e.  RR )
102101adantl 452 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  m  e.  RR )
103 letr 8959 . . . . . . . . . . . 12  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR  /\  m  e.  RR )  ->  ( ( k  <_ 
( k  +  1 )  /\  ( k  +  1 )  <_  m )  ->  k  <_  m ) )
10493, 96, 102, 103syl3anc 1182 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  ( ( k  <_ 
( k  +  1 )  /\  ( k  +  1 )  <_  m )  ->  k  <_  m ) )
10594, 104mpand 656 . . . . . . . . . 10  |-  ( ( k  e.  NN  /\  m  e.  W )  ->  ( ( k  +  1 )  <_  m  ->  k  <_  m )
)
106105ralimdva 2655 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( A. m  e.  W  ( k  +  1 )  <_  m  ->  A. m  e.  W  k  <_  m ) )
107106imim1d 69 . . . . . . . 8  |-  ( 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
) ) ) ) ) ) ) )
108107adantl 452 . . . . . . 7  |-  ( ( ( 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
) ) ) ) ) ) ) )
109 simplr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  y  e.  NN )
110 simprl 732 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  k  e.  NN )
111 nnleltp1 10118 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  e.  NN )  ->  ( y  <_  k  <->  y  <  ( k  +  1 ) ) )
112109, 110, 111syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( y  <_ 
k  <->  y  <  (
k  +  1 ) ) )
113109nnred 9806 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  y  e.  RR )
114110nnred 9806 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  k  e.  RR )
115113, 114leloed 9007 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( y  <_ 
k  <->  ( y  < 
k  \/  y  =  k ) ) )
116112, 115bitr3d 246 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( y  < 
( k  +  1 )  <->  ( y  < 
k  \/  y  =  k ) ) )
117 simpll 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ph )
118 ltp1 9639 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  RR  ->  k  <  ( k  +  1 ) )
119 ltnle 8947 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR )  ->  ( k  < 
( k  +  1 )  <->  -.  ( k  +  1 )  <_ 
k ) )
12095, 119mpdan 649 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  RR  ->  (
k  <  ( k  +  1 )  <->  -.  (
k  +  1 )  <_  k ) )
121118, 120mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  RR  ->  -.  ( k  +  1 )  <_  k )
122114, 121syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  -.  ( k  +  1 )  <_ 
k )
123 breq2 4064 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  =  k  ->  (
( k  +  1 )  <_  m  <->  ( k  +  1 )  <_ 
k ) )
124123rspccv 2915 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. m  e.  W  (
k  +  1 )  <_  m  ->  (
k  e.  W  -> 
( k  +  1 )  <_  k )
)
125124ad2antll 709 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( k  e.  W  ->  ( k  +  1 )  <_ 
k ) )
126122, 125mtod 168 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  -.  k  e.  W )
127 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  RR )
128 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  RR )
129 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  <_  B )
130 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . 22  |-  S  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
131 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  U  e.  ( ~P
ran  ( (,)  o.  F )  i^i  Fin ) )
132 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
133 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  U )  ->  (
( (,)  o.  F
) `  ( G `  t ) )  =  t )
134 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
135 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  C )
136127, 128, 129, 130, 17, 131, 132, 22, 133, 32, 29, 134, 135, 28, 25, 97ovolicc2lem2 18930 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( k  e.  NN  /\  -.  k  e.  W ) )  -> 
( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  <_  B )
137117, 110, 126, 136syl12anc 1180 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  <_  B )
138 iftrue 3605 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2nd `  ( F `
 ( G `  ( K `  k ) ) ) )  <_  B  ->  if ( ( 2nd `  ( F `
 ( G `  ( K `  k ) ) ) )  <_  B ,  ( 2nd `  ( F `  ( G `  ( K `  k ) ) ) ) ,  B )  =  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) ) )
139137, 138syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) ) ) )
14030ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  K : NN --> T )
141 ffvelrn 5701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( K : NN --> T  /\  k  e.  NN )  ->  ( K `  k
)  e.  T )
142140, 110, 141syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( K `  k )  e.  T
)
143134ralrimiva 2660 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
144143ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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
) )
145 fveq2 5563 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  ( K `  k )  ->  ( G `  t )  =  ( G `  ( K `  k ) ) )
146145fveq2d 5567 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  ( K `  k )  ->  ( F `  ( G `  t ) )  =  ( F `  ( G `  ( K `  k ) ) ) )
147146fveq2d 5567 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  ( K `  k )  ->  ( 2nd `  ( F `  ( G `  t ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  k ) ) ) ) )
148147breq1d 4070 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  ( K `  k )  ->  (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B  <->  ( 2nd `  ( F `  ( G `  ( K `  k ) ) ) )  <_  B )
)
149 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  ( K `  k )  ->  B  =  B )
150148, 147, 149ifbieq12d 3621 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) )
151 fveq2 5563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  k )  ->  ( H `  t )  =  ( H `  ( K `  k ) ) )
152150, 151eleq12d 2384 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 )
) ) )
153152rspcv 2914 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K `  k )  e.  T  ->  ( A. t  e.  T  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 ) ) ) )
154142, 144, 153sylc 56 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
155139, 154eqeltrrd 2391 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  e.  ( H `  ( K `  k ) ) )
15624, 25, 27, 28, 29algrp1 12791 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( K `
 ( k  +  1 ) )  =  ( H `  ( K `  k )
) )
157156ad2ant2r 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( K `  ( k  +  1 ) )  =  ( H `  ( K `
 k ) ) )
158155, 157eleqtrrd 2393 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  e.  ( K `  ( k  +  1 ) ) )
159140, 34, 35sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  K : NN --> U )
160110peano2nnd 9808 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( k  +  1 )  e.  NN )
161 ffvelrn 5701 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K : NN --> U  /\  ( k  +  1 )  e.  NN )  ->  ( K `  ( k  +  1 ) )  e.  U
)
162159, 160, 161syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( K `  ( k  +  1 ) )  e.  U
)
163127, 128, 129, 130, 17, 131, 132, 22, 133ovolicc2lem1 18929 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) ) ) ) ) ) )
164117, 162, 163syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) ) ) ) ) )
165158, 164mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) ) ) ) )
166165simp3d 969 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) ) ) )
16744adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  e.  RR )
16820ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  F : NN --> ( RR  X.  RR ) )
16922ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  G : U --> NN )
170 ffvelrn 5701 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K : NN --> U  /\  k  e.  NN )  ->  ( K `  k
)  e.  U )
171159, 110, 170syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( K `  k )  e.  U
)
172 ffvelrn 5701 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G : U --> NN  /\  ( K `  k )  e.  U )  -> 
( G `  ( K `  k )
)  e.  NN )
173169, 171, 172syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( G `  ( K `  k ) )  e.  NN )
174 ffvelrn 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 k ) )  e.  NN )  -> 
( F `  ( G `  ( K `  k ) ) )  e.  ( RR  X.  RR ) )
175168, 173, 174syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( F `  ( G `  ( K `
 k ) ) )  e.  ( RR 
X.  RR ) )
176 xp2nd 6192 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  ( G `
 ( K `  k ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  k ) ) ) )  e.  RR )
177175, 176syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  e.  RR )
178 ffvelrn 5701 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G : U --> NN  /\  ( K `  ( k  +  1 ) )  e.  U )  -> 
( G `  ( K `  ( k  +  1 ) ) )  e.  NN )
179169, 162, 178syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( G `  ( K `  ( k  +  1 ) ) )  e.  NN )
180 ffvelrn 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 ( k  +  1 ) ) )  e.  NN )  -> 
( F `  ( G `  ( K `  ( k  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
181168, 179, 180syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( F `  ( G `  ( K `
 ( k  +  1 ) ) ) )  e.  ( RR 
X.  RR ) )
182 xp2nd 6192 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  ( G `
 ( K `  ( k  +  1 ) ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  ( k  +  1 ) ) ) ) )  e.  RR )
183181, 182syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  NN )  /\  (
k  e.  NN  /\  A. m  e.  W  ( k  +  1 )  <_  m ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) )  e.  RR )
184 lttr 8944 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) ) ) ) )
185167, 177, 183, 184syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) ) ) ) )
186166, 185mpan2d 655 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) ) ) ) )
187186imim2d 48 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) ) ) ) )
188187com23 72 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) ) ) ) )
1894breq1d 4070 . . . . . . . . . . . . . 14  |-  ( y  =  k  ->  (
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) )  <-> 
( 2nd `  ( F `  ( G `  ( K `  k
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) ) ) )
190166, 189syl5ibrcom 213 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) ) ) )
191190a1dd 42 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) ) ) ) )
192188, 191jaod 369 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) ) ) ) )
193116, 192sylbid 206 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) ) ) ) )
194193com23 72 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) ) ) )
195194expr 598 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) ) ) ) ) )
196195a2d 23 . . . . . . 7  |-  ( ( ( 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
) ) ) ) ) )  ->  ( A. m  e.  W  ( k  +  1 )  <_  m  ->  ( y  <  ( k  +  1 )  -> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) ) ) ) ) )
197108, 196syld 40 . . . . . 6  |-  ( ( ( 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  +  1 )  -> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) ) ) ) ) )
198197expcom 424 . . . . 5  |-  ( 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
) ) ) ) ) )  ->  ( A. m  e.  W  ( k  +  1 )  <_  m  ->  ( y  <  ( k  +  1 )  -> 
( 2nd `  ( F `  ( G `  ( K `  y
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
k  +  1 ) ) ) ) ) ) ) ) ) )
199198a2d 23 . . . 4  |-  ( 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 ) ) ) ) ) ) ) ) ) )
20065, 76, 87, 76, 91, 199nnind 9809 . . 3  |-  ( 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
) ) ) ) ) ) ) )
20147, 49, 54, 200syl3c 57 . 2  |-  ( (
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
) ) ) ) ) )
2024, 8, 12, 15, 45, 201eqord1 9346 1  |-  ( (
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
) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1633    e. wcel 1701    =/= wne 2479   A.wral 2577   {crab 2581    i^i cin 3185    C_ wss 3186   (/)c0 3489   ifcif 3599   ~Pcpw 3659   {csn 3674   U.cuni 3864   class class class wbr 4060    X. cxp 4724   ran crn 4727    o. ccom 4730   -->wf 5288   ` cfv 5292  (class class class)co 5900   1stc1st 6162   2ndc2nd 6163   Fincfn 6906   RRcr 8781   1c1 8783    + caddc 8785    < clt 8912    <_ cle 8913    - cmin 9082   NNcn 9791   ZZcz 10071   (,)cioo 10703   [,]cicc 10706    seq cseq 11093   abscabs 11766
This theorem is referenced by:  ovolicc2lem4  18932
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-n0 10013  df-z 10072  df-uz 10278  df-ioo 10707  df-icc 10710  df-fz 10830  df-seq 11094
  Copyright terms: Public domain W3C validator