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

Theorem itg2addnclem3 26157
Description: Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 26158. (Contributed by Brendan Leahy, 11-Mar-2018.)
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
itg2addnclem3  |-  ( ph  ->  ( E. h  e. 
dom  S.1 ( E. y  e.  RR+  ( z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `
 z )  +  y ) ) )  o R  <_  ( F  o F  +  G
)  /\  s  =  ( S.1 `  h ) )  ->  E. t E. u ( E. f  e.  dom  S.1 E. g  e. 
dom  S.1 ( ( E. c  e.  RR+  (
z  e.  RR  |->  if ( ( f `  z )  =  0 ,  0 ,  ( ( f `  z
)  +  c ) ) )  o R  <_  F  /\  t  =  ( S.1 `  f
) )  /\  ( E. d  e.  RR+  (
z  e.  RR  |->  if ( ( g `  z )  =  0 ,  0 ,  ( ( g `  z
)  +  d ) ) )  o R  <_  G  /\  u  =  ( S.1 `  g
) ) )  /\  s  =  ( t  +  u ) ) ) )
Distinct variable groups:    t, s, u, y, z, f, g, h, c, d, F    G, s, t, u, y, z, f, g, h, c, d    ph, s,
t, u, y, z, f, g, h, c, d

Proof of Theorem itg2addnclem3
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 itg2addnc.f1 . . . . . . . . 9  |-  ( ph  ->  F  e. MblFn )
2 itg2addnc.f2 . . . . . . . . 9  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
31, 2itg2addnclem2 26156 . . . . . . . 8  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) )  e. 
dom  S.1 )
43adantrr 698 . . . . . . 7  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  (
y  e.  RR+  /\  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )
) )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) )  e. 
dom  S.1 )
5 simplr 732 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  h  e.  dom  S.1 )
6 i1fsub 19553 . . . . . . . . 9  |-  ( ( h  e.  dom  S.1  /\  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) )  e. 
dom  S.1 )  ->  (
h  o F  -  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) )  e.  dom  S.1 )
75, 3, 6syl2anc 643 . . . . . . . 8  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
h  o F  -  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) )  e.  dom  S.1 )
87adantrr 698 . . . . . . 7  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  (
y  e.  RR+  /\  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )
) )  ->  (
h  o F  -  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) )  e.  dom  S.1 )
9 3nn 10090 . . . . . . . . . . . . 13  |-  3  e.  NN
10 nnrp 10577 . . . . . . . . . . . . 13  |-  ( 3  e.  NN  ->  3  e.  RR+ )
119, 10ax-mp 8 . . . . . . . . . . . 12  |-  3  e.  RR+
12 rpdivcl 10590 . . . . . . . . . . . 12  |-  ( ( y  e.  RR+  /\  3  e.  RR+ )  ->  (
y  /  3 )  e.  RR+ )
1311, 12mpan2 653 . . . . . . . . . . 11  |-  ( y  e.  RR+  ->  ( y  /  3 )  e.  RR+ )
1413adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
y  /  3 )  e.  RR+ )
15 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  ( F `  x )  =  ( F `  z ) )
1615oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  (
( F `  x
)  /  ( y  /  3 ) )  =  ( ( F `
 z )  / 
( y  /  3
) ) )
1716fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  ( |_ `  ( ( F `
 x )  / 
( y  /  3
) ) )  =  ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) ) )
1817oveq1d 6055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  =  ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 ) )
1918oveq1d 6055 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  =  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) )
20 fveq2 5687 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
h `  x )  =  ( h `  z ) )
2119, 20breq12d 4185 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  <->  ( (
( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) ) )
2220neeq1d 2580 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  (
( h `  x
)  =/=  0  <->  (
h `  z )  =/=  0 ) )
2321, 22anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  <-> 
( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ) )
2423, 19, 20ifbieq12d 3721 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) )  =  if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) ) )
25 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) )  =  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) )
26 ovex 6065 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  e. 
_V
27 fvex 5701 . . . . . . . . . . . . . . . . . 18  |-  ( h `
 z )  e. 
_V
2826, 27ifex 3757 . . . . . . . . . . . . . . . . 17  |-  if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  e.  _V
2924, 25, 28fvmpt 5765 . . . . . . . . . . . . . . . 16  |-  ( z  e.  RR  ->  (
( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) ) )
3029eqeq1d 2412 . . . . . . . . . . . . . . 15  |-  ( z  e.  RR  ->  (
( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  =  0  <->  if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 ) )
3129oveq1d 6055 . . . . . . . . . . . . . . 15  |-  ( z  e.  RR  ->  (
( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) )  =  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )
3230, 31ifbieq2d 3719 . . . . . . . . . . . . . 14  |-  ( z  e.  RR  ->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) )  =  if ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) ) )
3332adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )  =  if ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  +  ( y  /  3 ) ) ) )
34 breq1 4175 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )  -> 
( 0  <_  ( F `  z )  <->  if ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )  <_ 
( F `  z
) ) )
35 breq1 4175 . . . . . . . . . . . . . 14  |-  ( ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  =  if ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )  -> 
( ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  +  ( y  /  3 ) )  <_  ( F `  z )  <->  if ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )  <_ 
( F `  z
) ) )
362ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F : RR --> ( 0 [,) 
+oo ) )
3736ffvelrnda 5829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  ( 0 [,)  +oo )
)
38 elrege0 10963 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  z )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  z )  e.  RR  /\  0  <_ 
( F `  z
) ) )
3937, 38sylib 189 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( F `
 z )  e.  RR  /\  0  <_ 
( F `  z
) ) )
4039simprd 450 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  0  <_  ( F `  z )
)
4140adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 )  ->  0  <_  ( F `  z
) )
42 df-ne 2569 . . . . . . . . . . . . . . . 16  |-  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =/=  0  <->  -.  if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  =  0 )
43 neeq1 2575 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  =/=  0  <->  if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =/=  0
) )
44 oveq1 6047 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  +  ( y  /  3 ) )  =  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  +  ( y  /  3 ) ) )
4544breq1d 4182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  <_  ( F `  z )  <->  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  <_  ( F `  z )
) )
4643, 45imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  =/=  0  ->  ( (
( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  +  ( y  / 
3 ) )  <_ 
( F `  z
) )  <->  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =/=  0  ->  ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  <_  ( F `  z )
) ) )
47 neeq1 2575 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  z )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( h `  z )  =/=  0  <->  if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =/=  0
) )
48 oveq1 6047 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  z )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( h `  z )  +  ( y  /  3 ) )  =  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  +  ( y  /  3 ) ) )
4948breq1d 4182 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  z )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( h `
 z )  +  ( y  /  3
) )  <_  ( F `  z )  <->  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  <_  ( F `  z )
) )
5047, 49imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  z )  =  if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  -> 
( ( ( h `
 z )  =/=  0  ->  ( (
h `  z )  +  ( y  / 
3 ) )  <_ 
( F `  z
) )  <->  ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =/=  0  ->  ( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  <_  ( F `  z )
) ) )
51 0re 9047 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  RR
52 pnfxr 10669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  +oo  e.  RR*
53 icossre 10947 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
5451, 52, 53mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 [,)  +oo )  C_  RR
5554, 37sseldi 3306 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  RR )
5613ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( y  / 
3 )  e.  RR+ )
5755, 56rerpdivcld 10631 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( F `
 z )  / 
( y  /  3
) )  e.  RR )
58 reflcl 11160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  z
)  /  ( y  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 z )  / 
( y  /  3
) ) )  e.  RR )
59 peano2rem 9323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  e.  RR  ->  (
( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  e.  RR )
6057, 58, 593syl 19 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  e.  RR )
6113rpred 10604 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  RR+  ->  ( y  /  3 )  e.  RR )
6261ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( y  / 
3 )  e.  RR )
6360, 62remulcld 9072 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  e.  RR )
64 peano2rem 9323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  z
)  /  ( y  /  3 ) )  e.  RR  ->  (
( ( F `  z )  /  (
y  /  3 ) )  -  1 )  e.  RR )
6557, 64syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  e.  RR )
6665, 62remulcld 9072 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( F `  z
)  /  ( y  /  3 ) )  -  1 )  x.  ( y  /  3
) )  e.  RR )
6757, 58syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  e.  RR )
68 1re 9046 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  RR
6968a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  1  e.  RR )
70 flle 11163 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  z
)  /  ( y  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 z )  / 
( y  /  3
) ) )  <_ 
( ( F `  z )  /  (
y  /  3 ) ) )
7157, 70syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  <_  (
( F `  z
)  /  ( y  /  3 ) ) )
7267, 57, 69, 71lesub1dd 9598 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  <_  (
( ( F `  z )  /  (
y  /  3 ) )  -  1 ) )
7360, 65, 56lemul1d 10643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  <_ 
( ( ( F `
 z )  / 
( y  /  3
) )  -  1 )  <->  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
( ( ( F `
 z )  / 
( y  /  3
) )  -  1 )  x.  ( y  /  3 ) ) ) )
7472, 73mpbid 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
( ( ( F `
 z )  / 
( y  /  3
) )  -  1 )  x.  ( y  /  3 ) ) )
7563, 66, 62, 74leadd1dd 9596 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  <_  (
( ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( y  /  3 ) ) )
7657recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( F `
 z )  / 
( y  /  3
) )  e.  CC )
77 ax-1cn 9004 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  CC
78 subcl 9261 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F `  z )  /  (
y  /  3 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( F `
 z )  / 
( y  /  3
) )  -  1 )  e.  CC )
7976, 77, 78sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  e.  CC )
8077a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  1  e.  CC )
8156rpcnd 10606 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( y  / 
3 )  e.  CC )
8279, 80, 81adddird 9069 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( ( F `  z )  /  (
y  /  3 ) )  -  1 )  +  1 )  x.  ( y  /  3
) )  =  ( ( ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( 1  x.  ( y  / 
3 ) ) ) )
83 npcan 9270 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F `  z )  /  (
y  /  3 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  +  1 )  =  ( ( F `  z )  /  ( y  / 
3 ) ) )
8476, 77, 83sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( F `  z
)  /  ( y  /  3 ) )  -  1 )  +  1 )  =  ( ( F `  z
)  /  ( y  /  3 ) ) )
8584oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( ( F `  z )  /  (
y  /  3 ) )  -  1 )  +  1 )  x.  ( y  /  3
) )  =  ( ( ( F `  z )  /  (
y  /  3 ) )  x.  ( y  /  3 ) ) )
8681mulid2d 9062 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( 1  x.  ( y  /  3
) )  =  ( y  /  3 ) )
8786oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( ( F `  z )  /  (
y  /  3 ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( 1  x.  (
y  /  3 ) ) )  =  ( ( ( ( ( F `  z )  /  ( y  / 
3 ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( y  /  3 ) ) )
8882, 85, 873eqtr3rd 2445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( ( F `  z )  /  (
y  /  3 ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  =  ( ( ( F `  z )  /  (
y  /  3 ) )  x.  ( y  /  3 ) ) )
8955recnd 9070 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( F `  z )  e.  CC )
9056rpne0d 10609 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( y  / 
3 )  =/=  0
)
9189, 81, 90divcan1d 9747 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( F `  z )  /  ( y  / 
3 ) )  x.  ( y  /  3
) )  =  ( F `  z ) )
9288, 91eqtrd 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( ( F `  z )  /  (
y  /  3 ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  =  ( F `  z ) )
9375, 92breqtrd 4196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  <_  ( F `  z )
)
9493adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) )  ->  (
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( y  /  3 ) )  <_  ( F `  z ) )
9594a1d 23 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) )  ->  (
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  =/=  0  -> 
( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  +  ( y  /  3 ) )  <_  ( F `  z ) ) )
96 ianor 475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 )  <-> 
( -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  \/  -.  (
h `  z )  =/=  0 ) )
9796anbi1i 677 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
)  /\  ( h `  z )  =/=  0
)  <->  ( ( -.  ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  \/  -.  ( h `  z
)  =/=  0 )  /\  ( h `  z )  =/=  0
) )
98 oranabs 830 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  \/  -.  (
h `  z )  =/=  0 )  /\  (
h `  z )  =/=  0 )  <->  ( -.  ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) )
9997, 98bitri 241 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
)  /\  ( h `  z )  =/=  0
)  <->  ( -.  (
( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) )
100 i1ff 19521 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h  e.  dom  S.1  ->  h : RR --> RR )
101100ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  h : RR --> RR )
102101ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( h `  z )  e.  RR )
103102, 62readdcld 9071 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( h `
 z )  +  ( y  /  3
) )  e.  RR )
104103adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( h `  z
)  +  ( y  /  3 ) )  e.  RR )
10555adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  ( F `  z )  e.  RR )
10663, 62readdcld 9071 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) )  e.  RR )
107106adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( y  /  3 ) )  e.  RR )
108102adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
h `  z )  e.  RR )
10963adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  e.  RR )
11061ad3antlr 712 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
y  /  3 )  e.  RR )
111102, 63ltnled 9176 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( h `
 z )  < 
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <->  -.  ( (
( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) ) )
112111biimpar 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
h `  z )  <  ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) ) )
113108, 109, 110, 112ltadd1dd 9593 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( h `  z
)  +  ( y  /  3 ) )  <  ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  +  ( y  /  3
) ) )
11493adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  +  ( y  /  3 ) )  <_  ( F `  z ) )
115104, 107, 105, 113, 114ltletrd 9186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( h `  z
)  +  ( y  /  3 ) )  <  ( F `  z ) )
116104, 105, 115ltled 9177 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
) )  ->  (
( h `  z
)  +  ( y  /  3 ) )  <_  ( F `  z ) )
117116adantrr 698 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  ( -.  (
( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) )  -> 
( ( h `  z )  +  ( y  /  3 ) )  <_  ( F `  z ) )
11899, 117sylan2b 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  ( -.  (
( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 )  /\  (
h `  z )  =/=  0 ) )  -> 
( ( h `  z )  +  ( y  /  3 ) )  <_  ( F `  z ) )
119118expr 599 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) )  -> 
( ( h `  z )  =/=  0  ->  ( ( h `  z )  +  ( y  /  3 ) )  <_  ( F `  z ) ) )
12046, 50, 95, 119ifbothda 3729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  =/=  0  -> 
( if ( ( ( ( ( |_
`  ( ( F `
 z )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) )  <_  ( F `  z )
) )
12142, 120syl5bir 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( -.  if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =  0  ->  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  +  ( y  /  3 ) )  <_  ( F `  z ) ) )
122121imp 419 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  /\  -.  if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  =  0 )  ->  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  z ) )  +  ( y  /  3 ) )  <_  ( F `  z ) )
12334, 35, 41, 122ifbothda 3729 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( if ( ( ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  z
)  /\  ( h `  z )  =/=  0
) ,  ( ( ( |_ `  (
( F `  z
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  z
) )  =  0 ,  0 ,  ( if ( ( ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) )  <_  ( h `  z )  /\  (
h `  z )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  z ) )  +  ( y  /  3
) ) )  <_ 
( F `  z
) )
12433, 123eqbrtrd 4192 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )  <_ 
( F `  z
) )
125124ralrimiva 2749 . . . . . . . . . . 11  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  A. z  e.  RR  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )  <_ 
( F `  z
) )
126 reex 9037 . . . . . . . . . . . . 13  |-  RR  e.  _V
127126a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  RR  e.  _V )
128 c0ex 9041 . . . . . . . . . . . . . 14  |-  0  e.  _V
129 ovex 6065 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) )  e.  _V
130128, 129ifex 3757 . . . . . . . . . . . . 13  |-  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  +  ( y  /  3 ) ) )  e.  _V
131130a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )  e. 
_V )
132 eqidd 2405 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) )  =  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) ) )
1332feqmptd 5738 . . . . . . . . . . . . 13  |-  ( ph  ->  F  =  ( z  e.  RR  |->  ( F `
 z ) ) )
134133ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  F  =  ( z  e.  RR  |->  ( F `  z ) ) )
135127, 131, 37, 132, 134ofrfval2 6282 . . . . . . . . . . 11  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) )  o R  <_  F  <->  A. z  e.  RR  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )  <_ 
( F `  z
) ) )
136125, 135mpbird 224 . . . . . . . . . 10  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) )  o R  <_  F )
137 oveq2 6048 . . . . . . . . . . . . . 14  |-  ( c  =  ( y  / 
3 )  ->  (
( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  c )  =  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) )
138137ifeq2d 3714 . . . . . . . . . . . . 13  |-  ( c  =  ( y  / 
3 )  ->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  c ) )  =  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) )
139138mpteq2dv 4256 . . . . . . . . . . . 12  |-  ( c  =  ( y  / 
3 )  ->  (
z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  c ) ) )  =  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) ) )
140139breq1d 4182 . . . . . . . . . . 11  |-  ( c  =  ( y  / 
3 )  ->  (
( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  c ) ) )  o R  <_  F  <->  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  ( y  /  3
) ) ) )  o R  <_  F
) )
141140rspcev 3012 . . . . . . . . . 10  |-  ( ( ( y  /  3
)  e.  RR+  /\  (
z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  ( y  /  3 ) ) ) )  o R  <_  F )  ->  E. c  e.  RR+  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  +  c ) ) )  o R  <_  F )
14214, 136, 141syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  E. c  e.  RR+  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  c ) ) )  o R  <_  F
)
143142adantrr 698 . . . . . . . 8  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  (
y  e.  RR+  /\  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )
) )  ->  E. c  e.  RR+  ( z  e.  RR  |->  if ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) ) `  z )  =  0 ,  0 ,  ( ( ( x  e.  RR  |->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( y  /  3
) ) )  - 
1 )  x.  (
y  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
y  /  3 ) ) )  -  1 )  x.  ( y  /  3 ) ) ,  ( h `  x ) ) ) `
 z )  +  c ) ) )  o R  <_  F
)
14413ad2antrl 709 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  (
y  e.  RR+  /\  (
z  e.  RR  |->  if ( ( h `  z )  =  0 ,  0 ,  ( ( h `  z
)  +  y ) ) )  o R  <_  ( F  o F  +  G )
) )  ->  (
y  /  3 )  e.  RR+ )
145 ffn 5550 . . . . . . . . . . . . . . . . . . . 20  |-  ( h : RR --> RR  ->  h  Fn  RR )
146100, 145syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( h  e.  dom  S.1  ->  h  Fn  RR )
147146ad2antlr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  h  Fn  RR )
148 ovex 6065 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  e. 
_V
149 fvex 5701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h `
 x )  e. 
_V
150148, 149ifex 3757 . . . . . . . . . . . . . . . . . . . 20  |-  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) )  e.  _V
151150, 25fnmpti 5532 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) )  Fn  RR
152151a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( y  /  3 ) ) )  -  1 )  x.  ( y  / 
3 ) ) ,  ( h `  x
) ) )  Fn  RR )
153 inidm 3510 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
i^i  RR )  =  RR
154 eqidd 2405 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( h `  z )  =  ( h `  z ) )
15529adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  y  e.  RR+ )  /\  z  e.  RR )  ->  ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) ) ,  ( h `  x ) ) ) `  z
)  =  if ( ( ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) ) )  -  1 )  x.  ( y  /  3
) )  <_  (
h `  z )  /\  ( h `  z
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  z )  /  ( y  / 
3 ) )