Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2addnc Unicode version

Theorem itg2addnc 25319
Description: Alternate proof of itg2add 19167 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19116, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8106, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.)
Hypotheses
Ref Expression
itg2addnc.f1  |-  ( ph  ->  F  e. MblFn )
itg2addnc.f2  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
itg2addnc.f3  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
itg2addnc.g2  |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )
itg2addnc.g3  |-  ( ph  ->  ( S.2 `  G
)  e.  RR )
Assertion
Ref Expression
itg2addnc  |-  ( ph  ->  ( S.2 `  ( F  o F  +  G
) )  =  ( ( S.2 `  F
)  +  ( S.2 `  G ) ) )

Proof of Theorem itg2addnc
Dummy variables  t 
s  u  v  x  y  z  w  f  g  h  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ge0addcl 10795 . . . . . . . 8  |-  ( ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo ) )  ->  (
x  +  y )  e.  ( 0 [,) 
+oo ) )
21adantl 452 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 0 [,)  +oo )  /\  y  e.  ( 0 [,)  +oo )
) )  ->  (
x  +  y )  e.  ( 0 [,) 
+oo ) )
3 itg2addnc.f2 . . . . . . 7  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
4 itg2addnc.g2 . . . . . . 7  |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )
5 reex 8873 . . . . . . . 8  |-  RR  e.  _V
65a1i 10 . . . . . . 7  |-  ( ph  ->  RR  e.  _V )
7 inidm 3412 . . . . . . 7  |-  ( RR 
i^i  RR )  =  RR
82, 3, 4, 6, 6, 7off 6135 . . . . . 6  |-  ( ph  ->  ( F  o F  +  G ) : RR --> ( 0 [,) 
+oo ) )
9 df-ico 10709 . . . . . . 7  |-  [,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) } )
10 df-icc 10710 . . . . . . 7  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
11 idd 21 . . . . . . 7  |-  ( ( 0  e.  RR*  /\  w  e.  RR* )  ->  (
0  <_  w  ->  0  <_  w ) )
12 xrltle 10530 . . . . . . 7  |-  ( ( w  e.  RR*  /\  +oo  e.  RR* )  ->  (
w  <  +oo  ->  w  <_  +oo ) )
139, 10, 11, 12ixxssixx 10717 . . . . . 6  |-  ( 0 [,)  +oo )  C_  (
0 [,]  +oo )
14 fss 5435 . . . . . 6  |-  ( ( ( F  o F  +  G ) : RR --> ( 0 [,) 
+oo )  /\  (
0 [,)  +oo )  C_  ( 0 [,]  +oo ) )  ->  ( F  o F  +  G
) : RR --> ( 0 [,]  +oo ) )
158, 13, 14sylancl 643 . . . . 5  |-  ( ph  ->  ( F  o F  +  G ) : RR --> ( 0 [,] 
+oo ) )
16 eqid 2316 . . . . . 6  |-  { s  |  E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  ( F  o F  +  G
)  /\  s  =  ( S.1 `  h ) ) }  =  {
s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
y } ) )  o R  <_  ( F  o F  +  G
)  /\  s  =  ( S.1 `  h ) ) }
1716itg2addnclem 25317 . . . . 5  |-  ( ( F  o F  +  G ) : RR --> ( 0 [,]  +oo )  ->  ( S.2 `  ( F  o F  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_ 
( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  )
)
1815, 17syl 15 . . . 4  |-  ( ph  ->  ( S.2 `  ( F  o F  +  G
) )  =  sup ( { s  |  E. h  e.  dom  S.1 ( E. y  e.  RR+  (
h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { y } ) )  o R  <_ 
( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) } ,  RR* ,  <  )
)
19 r19.41v 2727 . . . . . . . . . . . 12  |-  ( E. v  e.  RR+  (
( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { v } ) )  o R  <_  ( F  o F  +  G )  /\  s  =  ( S.1 `  h ) )  <-> 
( E. v  e.  RR+  ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR 
X.  { v } ) )  o R  <_  ( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) )
20 itg2addnc.f1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  e. MblFn )
2120, 3itg2addnclem2 25318 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  e. 
dom  S.1 )
22213adant3 975 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+  /\  ( ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { v } ) )  o R  <_ 
( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) )  ->  ( a  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 a )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  a )  /\  (
h `  a )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  a ) ) )  e.  dom  S.1 )
23 simplr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h  e.  dom  S.1 )
2420, 3itg2addnclem2 25318 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
b  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  b
)  /\  ( h `  b )  =/=  0
) ,  ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  b
) ) )  e. 
dom  S.1 )
25 i1fsub 19116 . . . . . . . . . . . . . . . . 17  |-  ( ( h  e.  dom  S.1  /\  ( b  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  b
)  /\  ( h `  b )  =/=  0
) ,  ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  b
) ) )  e. 
dom  S.1 )  ->  (
h  o F  -  ( b  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  b
)  /\  ( h `  b )  =/=  0
) ,  ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  b
) ) ) )  e.  dom  S.1 )
2623, 24, 25syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
h  o F  -  ( b  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  b
)  /\  ( h `  b )  =/=  0
) ,  ( ( ( |_ `  (
( F `  b
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  b
) ) ) )  e.  dom  S.1 )
27263adant3 975 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+  /\  ( ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  { v } ) )  o R  <_ 
( F  o F  +  G )  /\  s  =  ( S.1 `  h ) ) )  ->  ( h  o F  -  ( b  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  b )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  b )  /\  ( h `  b
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  b )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  b ) ) ) )  e. 
dom  S.1 )
28 3nn 9925 . . . . . . . . . . . . . . . . . . . . . . 23  |-  3  e.  NN
29 nnrp 10410 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 3  e.  NN  ->  3  e.  RR+ )
3028, 29ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  3  e.  RR+
31 rpdivcl 10423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v  e.  RR+  /\  3  e.  RR+ )  ->  (
v  /  3 )  e.  RR+ )
3230, 31mpan2 652 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR+ )
33323ad2ant2 977 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+  /\  ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
v } ) )  o R  <_  ( F  o F  +  G
) )  ->  (
v  /  3 )  e.  RR+ )
34 breq1 4063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  -> 
( 0  <_  ( F `  x )  <->  if ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  <_ 
( F `  x
) ) )
35 breq1 4063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  =  if ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  -> 
( ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  +  ( v  /  3 ) )  <_  ( F `  x )  <->  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  <_ 
( F `  x
) ) )
363ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> ( 0 [,) 
+oo ) )
3736ffvelrnda 5703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
38 elrege0 10793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
3937, 38sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
4039simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  ( F `  x )
)
4140adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 )  ->  0  <_  ( F `  x
) )
42 df-ne 2481 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =/=  0  <->  -.  if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 )
43 0re 8883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  e.  RR
44 pnfxr 10502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  +oo  e.  RR*
45 icossre 10777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
4643, 44, 45mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 0 [,)  +oo )  C_  RR
47 fss 5435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
483, 46, 47sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  F : RR --> RR )
4948ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> RR )
5049ffvelrnda 5703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
51 rpre 10407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( v  e.  RR+  ->  v  e.  RR )
52 3re 9862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  3  e.  RR
53 3ne0 9876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  3  =/=  0
54 redivcl 9524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( v  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
v  /  3 )  e.  RR )
5552, 53, 54mp3an23 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( v  e.  RR  ->  (
v  /  3 )  e.  RR )
5651, 55syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR )
5756ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR )
58 rpcn 10409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( v  e.  RR+  ->  v  e.  CC )
59 rpne0 10416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( v  e.  RR+  ->  v  =/=  0 )
60 3cn 9863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  3  e.  CC
61 divne0 9481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( v  e.  CC  /\  v  =/=  0 )  /\  ( 3  e.  CC  /\  3  =/=  0 ) )  -> 
( v  /  3
)  =/=  0 )
6260, 53, 61mpanr12 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( v  e.  CC  /\  v  =/=  0 )  -> 
( v  /  3
)  =/=  0 )
6358, 59, 62syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( v  e.  RR+  ->  ( v  /  3 )  =/=  0 )
6463ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  =/=  0
)
6550, 57, 64redivcld 9633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  / 
( v  /  3
) )  e.  RR )
66 reflcl 10975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F `  x
)  /  ( v  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  e.  RR )
67 peano2rem 9158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  e.  RR  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  e.  RR )
6865, 66, 673syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  e.  RR )
6968, 57remulcld 8908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  e.  RR )
70 peano2rem 9158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F `  x
)  /  ( v  /  3 ) )  e.  RR  ->  (
( ( F `  x )  /  (
v  /  3 ) )  -  1 )  e.  RR )
7165, 70syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( F `  x )  /  ( v  / 
3 ) )  - 
1 )  e.  RR )
7271, 57remulcld 8908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( F `  x
)  /  ( v  /  3 ) )  -  1 )  x.  ( v  /  3
) )  e.  RR )
7365, 66syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  RR )
74 1re 8882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  RR
7574a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  1  e.  RR )
76 flle 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( F `  x
)  /  ( v  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  <_ 
( ( F `  x )  /  (
v  /  3 ) ) )
7765, 76syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  (
( F `  x
)  /  ( v  /  3 ) ) )
7873, 65, 75, 77lesub1dd 9433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  <_  (
( ( F `  x )  /  (
v  /  3 ) )  -  1 ) )
7932ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR+ )
8068, 71, 79lemul1d 10476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  <_ 
( ( ( F `
 x )  / 
( v  /  3
) )  -  1 )  <->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
( ( ( F `
 x )  / 
( v  /  3
) )  -  1 )  x.  ( v  /  3 ) ) ) )
8178, 80mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
( ( ( F `
 x )  / 
( v  /  3
) )  -  1 )  x.  ( v  /  3 ) ) )
8269, 72, 57, 81leadd1dd 9431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  <_  (
( ( ( ( F `  x )  /  ( v  / 
3 ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) ) )
8365recnd 8906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  / 
( v  /  3
) )  e.  CC )
84 ax-1cn 8840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  1  e.  CC
8584a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  1  e.  CC )
8657recnd 8906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  CC )
8783, 85, 86subdird 9281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( F `  x
)  /  ( v  /  3 ) )  -  1 )  x.  ( v  /  3
) )  =  ( ( ( ( F `
 x )  / 
( v  /  3
) )  x.  (
v  /  3 ) )  -  ( 1  x.  ( v  / 
3 ) ) ) )
8850recnd 8906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  CC )
8988, 86, 64divcan1d 9582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( F `  x )  /  ( v  / 
3 ) )  x.  ( v  /  3
) )  =  ( F `  x ) )
9032rpcnd 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  CC )
9190mulid2d 8898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( v  e.  RR+  ->  ( 1  x.  ( v  / 
3 ) )  =  ( v  /  3
) )
9291ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( 1  x.  ( v  /  3
) )  =  ( v  /  3 ) )
9389, 92oveq12d 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( F `  x
)  /  ( v  /  3 ) )  x.  ( v  / 
3 ) )  -  ( 1  x.  (
v  /  3 ) ) )  =  ( ( F `  x
)  -  ( v  /  3 ) ) )
9487, 93eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( F `  x
)  /  ( v  /  3 ) )  -  1 )  x.  ( v  /  3
) )  =  ( ( F `  x
)  -  ( v  /  3 ) ) )
9594oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( F `  x )  /  (
v  /  3 ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  =  ( ( ( F `  x )  -  (
v  /  3 ) )  +  ( v  /  3 ) ) )
96 divcl 9475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( v  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
v  /  3 )  e.  CC )
9760, 53, 96mp3an23 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  e.  CC  ->  (
v  /  3 )  e.  CC )
9858, 97syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  CC )
9998ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  CC )
10088, 99npcand 9206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( F `  x )  -  ( v  / 
3 ) )  +  ( v  /  3
) )  =  ( F `  x ) )
10195, 100eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( F `  x )  /  (
v  /  3 ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  =  ( F `  x ) )
10282, 101breqtrd 4084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  <_  ( F `  x )
)
103102adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) )  <_  ( F `  x ) )
104 iftrue 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )
105104oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) )  =  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  +  ( v  / 
3 ) ) )
106105breq1d 4070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  (
( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )  <->  ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
107106adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  (
( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )  <->  ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
108103, 107mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) )  <_  ( F `  x ) )
109108a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =/=  0  ->  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )
) )
110 ianor 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  <-> 
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  -.  (
h `  x )  =/=  0 ) )
111 oranabs 829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  -.  (
h `  x )  =/=  0 )  /\  (
h `  x )  =/=  0 )  <->  ( -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) )
112 i1ff 19084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( h  e.  dom  S.1  ->  h : RR --> RR )
113112ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h : RR --> RR )
114113ffvelrnda 5703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  RR )
115114, 69, 57ltadd1d 9410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( h `
 x )  < 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <->  ( ( h `
 x )  +  ( v  /  3
) )  <  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) ) ) )
116114, 69ltnled 9011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( h `
 x )  < 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <->  -.  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) ) )
117115, 116bitr3d 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( h `  x )  +  ( v  / 
3 ) )  < 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  +  ( v  /  3 ) )  <->  -.  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) ) )
118114, 57readdcld 8907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( h `
 x )  +  ( v  /  3
) )  e.  RR )
11969, 57readdcld 8907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  e.  RR )
120 ltletr 8958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( h `  x )  +  ( v  /  3 ) )  e.  RR  /\  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  +  ( v  /  3 ) )  e.  RR  /\  ( F `  x )  e.  RR )  -> 
( ( ( ( h `  x )  +  ( v  / 
3 ) )  < 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  +  ( v  /  3 ) )  /\  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  +  ( v  / 
3 ) )  <_ 
( F `  x
) )  ->  (
( h `  x
)  +  ( v  /  3 ) )  <  ( F `  x ) ) )
121118, 119, 50, 120syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( h `  x
)  +  ( v  /  3 ) )  <  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  +  ( v  /  3
) )  /\  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  +  ( v  /  3 ) )  <_  ( F `  x ) )  -> 
( ( h `  x )  +  ( v  /  3 ) )  <  ( F `
 x ) ) )
122102, 121mpan2d 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( h `  x )  +  ( v  / 
3 ) )  < 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  +  ( v  /  3 ) )  ->  ( (
h `  x )  +  ( v  / 
3 ) )  < 
( F `  x
) ) )
123 ltle 8955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( h `  x )  +  ( v  /  3 ) )  e.  RR  /\  ( F `  x )  e.  RR )  -> 
( ( ( h `
 x )  +  ( v  /  3
) )  <  ( F `  x )  ->  ( ( h `  x )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
124118, 50, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( h `  x )  +  ( v  / 
3 ) )  < 
( F `  x
)  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) )
125122, 124syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( h `  x )  +  ( v  / 
3 ) )  < 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  +  ( v  /  3 ) )  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) )
126117, 125sylbird 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  ->  (
( h `  x
)  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
127126adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  (
( h `  x
)  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
128111, 127syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  -.  ( h `  x )  =/=  0
)  /\  ( h `  x )  =/=  0
)  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) )
129128exp3a 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  \/  -.  ( h `  x
)  =/=  0 )  ->  ( ( h `
 x )  =/=  0  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) ) )
130110, 129syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( -.  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  (
( h `  x
)  =/=  0  -> 
( ( h `  x )  +  ( v  /  3 ) )  <_  ( F `  x ) ) ) )
131130imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) )  -> 
( ( h `  x )  =/=  0  ->  ( ( h `  x )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
132 iffalse 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  ( h `  x
) )
133132neeq1d 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =/=  0  <->  (
h `  x )  =/=  0 ) )
134132oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  +  ( v  /  3 ) )  =  ( ( h `
 x )  +  ( v  /  3
) ) )
135134breq1d 4070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  ->  ( ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) )  <_  ( F `  x )  <->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) )
136133, 135imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  ->  ( ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =/=  0  ->  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )
)  <->  ( ( h `
 x )  =/=  0  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) ) )
137136adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) )  -> 
( ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =/=  0  -> 
( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )
)  <->  ( ( h `
 x )  =/=  0  ->  ( (
h `  x )  +  ( v  / 
3 ) )  <_ 
( F `  x
) ) ) )
138131, 137mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) )  -> 
( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =/=  0  ->  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
139109, 138pm2.61dan 766 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =/=  0  -> 
( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) )  <_  ( F `  x )
) )
14042, 139syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( -.  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  +  ( v  /  3 ) )  <_  ( F `  x ) ) )
141140imp 418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  -.  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =  0 )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  +  ( v  /  3 ) )  <_  ( F `  x ) )
14234, 35, 41, 141ifbothda 3629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  <_ 
( F `  x
) )
143142ralrimiva 2660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  A. x  e.  RR  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  <_ 
( F `  x
) )
144 ovex 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
145 fvex 5577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h `
 a )  e. 
_V
146144, 145ifex 3657 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( ( ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  a )  /\  ( h `  a
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  a ) )  e.  _V
147 eqid 2316 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  a )  /\  ( h `  a
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  a ) ) )  =  ( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )
148146, 147fnmpti 5409 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  a )  /\  ( h `  a
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  a ) ) )  Fn  RR
149148a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  Fn  RR )
150 ovex 5925 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  /  3 )  e. 
_V
151150fconst 5465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( RR 
X.  { ( v  /  3 ) } ) : RR --> { ( v  /  3 ) }
152 ffn 5427 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  X.  { ( v  /  3 ) } ) : RR --> { ( v  / 
3 ) }  ->  ( RR  X.  { ( v  /  3 ) } )  Fn  RR )
153151, 152mp1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ( RR  X.  { ( v  /  3 ) } )  Fn  RR )
1545a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  RR  e.  _V )
155149, 153, 154, 154, 7offn 6131 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) )  Fn  RR )
156 ffn 5427 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
1573, 156syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F  Fn  RR )
158157ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F  Fn  RR )
159 fveq2 5563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( a  =  x  ->  ( F `  a )  =  ( F `  x ) )
160159oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  x  ->  (
( F `  a
)  /  ( v  /  3 ) )  =  ( ( F `
 x )  / 
( v  /  3
) ) )
161160fveq2d 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  x  ->  ( |_ `  ( ( F `
 a )  / 
( v  /  3
) ) )  =  ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) ) )
162161oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  =  x  ->  (
( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  =  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 ) )
163162oveq1d 5915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  x  ->  (
( ( |_ `  ( ( F `  a )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )
164 fveq2 5563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  x  ->  (
h `  a )  =  ( h `  x ) )
165163, 164breq12d 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  x  ->  (
( ( ( |_
`  ( ( F `
 a )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  a )  <->  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) ) )
166164neeq1d 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  x  ->  (
( h `  a
)  =/=  0  <->  (
h `  x )  =/=  0 ) )
167165, 166anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  x  ->  (
( ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  a )  /\  ( h `  a
)  =/=  0 )  <-> 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ) )
168167, 163, 164ifbieq12d 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  x  ->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) )  =  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )
169 ovex 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
170 fvex 5577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h `
 x )  e. 
_V
171169, 170ifex 3657 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  e.  _V
172168, 147, 171fvmpt 5640 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  (
( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) ) `  x )  =  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )
173172adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( a  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  a )  /\  ( h `  a
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  a ) ) ) `  x
)  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )
174150fvconst2 5768 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  RR  ->  (
( RR  X.  {
( v  /  3
) } ) `  x )  =  ( v  /  3 ) )
175174adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( RR 
X.  { ( v  /  3 ) } ) `  x )  =  ( v  / 
3 ) )
176149, 153, 154, 154, 7, 173, 175ofval 6129 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) ) `
 x )  =  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) ) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( v  / 
3 ) ) )
177 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) )  =  ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) )
178 eqeq1 2322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  -> 
( z  =  0  <-> 
if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ) )
179178adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( z  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  /\  w  =  ( v  /  3
) )  ->  (
z  =  0  <->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ) )
180 oveq12 5909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( z  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  /\  w  =  ( v  /  3
) )  ->  (
z  +  w )  =  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  +  ( v  /  3 ) ) )
181179, 180ifbieq2d 3619 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( z  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  /\  w  =  ( v  /  3
) )  ->  if ( z  =  0 ,  0 ,  ( z  +  w ) )  =  if ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) ) )
182181adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( z  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  /\  w  =  ( v  /  3 ) ) )  ->  if (
z  =  0 ,  0 ,  ( z  +  w ) )  =  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) ) )
183 ifcl 3635 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  RR  /\  ( h `  x
)  e.  RR )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  e.  RR )
18469, 114, 183syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  e.  RR )
185 c0ex 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  _V
186 ovex 5925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) )  e.  _V
187185, 186ifex 3657 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  e. 
_V
188187a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  if ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  e. 
_V )
189177, 182, 184, 57, 188ovmpt2d 6017 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( v  /  3
) )  =  if ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) ) )
190176, 189eqtrd 2348 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) ) `
 x )  =  if ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  +  ( v  /  3 ) ) ) )
191 eqidd 2317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  =  ( F `  x ) )
192155, 158, 154, 154, 7, 190, 191ofrfval 6128 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
( ( a  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 a )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  a )  /\  (
h `  a )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  a )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  a ) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) )  o R  <_  F  <->  A. x  e.  RR  if ( if ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  +  ( v  /  3
) ) )  <_ 
( F `  x
) ) )
193143, 192mpbird 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) )  o R  <_  F
)
1941933adant3 975 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+  /\  ( h  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
v } ) )  o R  <_  ( F  o F  +  G
) )  ->  (
( a  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  a
)  /\  ( h `  a )  =/=  0
) ,  ( ( ( |_ `  (
( F `  a
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  a
) ) )  o F ( z  e.  RR ,  w  e.  RR  |->  if ( z  =  0 ,  0 ,  ( z  +  w ) ) ) ( RR  X.  {
( v  /  3
) } ) )  o R  <_  F
)
195 sneq 3685 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( v  / 
3 )  ->  { y }  =  { ( v  /  3 ) } )
196195xpeq2d 4750 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( v  / 
3 )  ->  ( RR  X.  { y } )  =  ( RR 
X.  { ( v