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

Theorem itg2addnclem2 25318
Description: Lemma for itg2addnc 25319. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
Hypotheses
Ref Expression
itg2addnc.f1  |-  ( ph  ->  F  e. MblFn )
itg2addnc.f2  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
Assertion
Ref Expression
itg2addnclem2  |-  ( ( ( 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. 
dom  S.1 )
Distinct variable groups:    x, v, h, F    ph, v, x, h

Proof of Theorem itg2addnclem2
Dummy variables  t 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2addnc.f2 . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
2 0re 8883 . . . . . . . . . . . 12  |-  0  e.  RR
3 pnfxr 10502 . . . . . . . . . . . 12  |-  +oo  e.  RR*
4 icossre 10777 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
52, 3, 4mp2an 653 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  RR
6 fss 5435 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
71, 5, 6sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
87ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> RR )
98ffvelrnda 5703 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
10 rpre 10407 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  v  e.  RR )
11 3re 9862 . . . . . . . . . . 11  |-  3  e.  RR
12 3ne0 9876 . . . . . . . . . . 11  |-  3  =/=  0
1311, 12pm3.2i 441 . . . . . . . . . 10  |-  ( 3  e.  RR  /\  3  =/=  0 )
14 redivcl 9524 . . . . . . . . . . 11  |-  ( ( v  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
v  /  3 )  e.  RR )
15143expb 1152 . . . . . . . . . 10  |-  ( ( v  e.  RR  /\  ( 3  e.  RR  /\  3  =/=  0 ) )  ->  ( v  /  3 )  e.  RR )
1610, 13, 15sylancl 643 . . . . . . . . 9  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR )
1716ad2antlr 707 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR )
18 rpcnne0 10418 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  ( v  e.  CC  /\  v  =/=  0 ) )
19 3cn 9863 . . . . . . . . . . 11  |-  3  e.  CC
2019, 12pm3.2i 441 . . . . . . . . . 10  |-  ( 3  e.  CC  /\  3  =/=  0 )
21 divne0 9481 . . . . . . . . . 10  |-  ( ( ( v  e.  CC  /\  v  =/=  0 )  /\  ( 3  e.  CC  /\  3  =/=  0 ) )  -> 
( v  /  3
)  =/=  0 )
2218, 20, 21sylancl 643 . . . . . . . . 9  |-  ( v  e.  RR+  ->  ( v  /  3 )  =/=  0 )
2322ad2antlr 707 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  =/=  0
)
249, 17, 23redivcld 9633 . . . . . . 7  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  / 
( v  /  3
) )  e.  RR )
25 reflcl 10975 . . . . . . 7  |-  ( ( ( F `  x
)  /  ( v  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  e.  RR )
2624, 25syl 15 . . . . . 6  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  RR )
27 peano2rem 9158 . . . . . 6  |-  ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  e.  RR  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  e.  RR )
2826, 27syl 15 . . . . 5  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  e.  RR )
2928, 17remulcld 8908 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  e.  RR )
30 i1ff 19084 . . . . . 6  |-  ( h  e.  dom  S.1  ->  h : RR --> RR )
3130ad2antlr 707 . . . . 5  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h : RR --> RR )
3231ffvelrnda 5703 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  RR )
33 ifcl 3635 . . . 4  |-  ( ( ( ( ( |_
`  ( ( 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 )
3429, 32, 33syl2anc 642 . . 3  |-  ( ( ( ( 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 )
35 eqid 2316 . . 3  |-  ( 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 ) ) )  =  ( 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
) ) )
3634, 35fmptd 5722 . 2  |-  ( ( ( 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
) ) ) : RR --> RR )
37 fzfi 11081 . . . . 5  |-  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  e.  Fin
38 ovex 5925 . . . . . . 7  |-  ( ( t  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
39 eqid 2316 . . . . . . 7  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  =  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )
4038, 39fnmpti 5409 . . . . . 6  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  Fn  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
41 dffn4 5495 . . . . . 6  |-  ( ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  Fn  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )  <-> 
( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) )
4240, 41mpbi 199 . . . . 5  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )
43 fofi 7187 . . . . 5  |-  ( ( ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )  e.  Fin  /\  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) )  ->  ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  e.  Fin )
4437, 42, 43mp2an 653 . . . 4  |-  ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  e. 
Fin
45 i1frn 19085 . . . . 5  |-  ( h  e.  dom  S.1  ->  ran  h  e.  Fin )
4645ad2antlr 707 . . . 4  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  h  e.  Fin )
47 unfi 7169 . . . 4  |-  ( ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  e.  Fin  /\ 
ran  h  e.  Fin )  ->  ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  e. 
Fin )
4844, 46, 47sylancr 644 . . 3  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h )  e.  Fin )
49 3nn 9925 . . . . . . . . . . . . . . . . 17  |-  3  e.  NN
50 nnrp 10410 . . . . . . . . . . . . . . . . 17  |-  ( 3  e.  NN  ->  3  e.  RR+ )
5149, 50ax-mp 8 . . . . . . . . . . . . . . . 16  |-  3  e.  RR+
52 rpdivcl 10423 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  RR+  /\  3  e.  RR+ )  ->  (
v  /  3 )  e.  RR+ )
5351, 52mpan2 652 . . . . . . . . . . . . . . 15  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR+ )
5453ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR+ )
551ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> ( 0 [,) 
+oo ) )
5655ffvelrnda 5703 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
57 elrege0 10793 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
5856, 57sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
5958simprd 449 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  ( F `  x )
)
609, 54, 59divge0d 10473 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  (
( F `  x
)  /  ( v  /  3 ) ) )
61 flge0nn0 10995 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  x )  /  (
v  /  3 ) )  e.  RR  /\  0  <_  ( ( F `
 x )  / 
( v  /  3
) ) )  -> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  NN0 )
6224, 60, 61syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  NN0 )
6362nn0ge0d 10068 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) ) )
6463adantr 451 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) )  ->  0  <_  ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) ) )
65 frn 5433 . . . . . . . . . . . . . . . . 17  |-  ( h : RR --> RR  ->  ran  h  C_  RR )
6630, 65syl 15 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  C_  RR )
67 i1f0rn 19090 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  0  e.  ran  h )
68 elex2 2834 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ran  h  ->  E. x  x  e.  ran  h )
6967, 68syl 15 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  E. x  x  e.  ran  h )
70 n0 3498 . . . . . . . . . . . . . . . . 17  |-  ( ran  h  =/=  (/)  <->  E. x  x  e.  ran  h )
7169, 70sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  =/=  (/) )
72 fimaxre2 9747 . . . . . . . . . . . . . . . . 17  |-  ( ( ran  h  C_  RR  /\ 
ran  h  e.  Fin )  ->  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )
7366, 45, 72syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )
7466, 71, 733jca 1132 . . . . . . . . . . . . . . 15  |-  ( h  e.  dom  S.1  ->  ( ran  h  C_  RR  /\ 
ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ran  h  y  <_  x ) )
7574ad3antlr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ran  h  C_  RR  /\  ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  h  y  <_  x ) )
76 ffn 5427 . . . . . . . . . . . . . . . . . 18  |-  ( h : RR --> RR  ->  h  Fn  RR )
7730, 76syl 15 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  h  Fn  RR )
78 dffn3 5434 . . . . . . . . . . . . . . . . 17  |-  ( h  Fn  RR  <->  h : RR
--> ran  h )
7977, 78sylib 188 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  h : RR --> ran  h
)
8079ad2antlr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h : RR --> ran  h )
8180ffvelrnda 5703 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  ran  h )
82 suprub 9760 . . . . . . . . . . . . . 14  |-  ( ( ( ran  h  C_  RR  /\  ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  h  y  <_  x )  /\  (
h `  x )  e.  ran  h )  -> 
( h `  x
)  <_  sup ( ran  h ,  RR ,  <  ) )
8375, 81, 82syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  <_  sup ( ran  h ,  RR ,  <  ) )
84 suprcl 9759 . . . . . . . . . . . . . . . . 17  |-  ( ( ran  h  C_  RR  /\ 
ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
8566, 71, 73, 84syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
8685ad3antlr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
87 letr 8959 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  RR  /\  ( h `  x
)  e.  RR  /\  sup ( ran  h ,  RR ,  <  )  e.  RR )  ->  (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  <_  sup ( ran  h ,  RR ,  <  ) )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  sup ( ran  h ,  RR ,  <  )
) )
8829, 32, 86, 87syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  <_  sup ( ran  h ,  RR ,  <  )
)  ->  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )
) )
8928, 86, 54lemuldivd 10482 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  <->  ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  <_  ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) ) ) )
90 1re 8882 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
9190a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  1  e.  RR )
9286, 17, 23redivcld 9633 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  e.  RR )
9326, 91, 92lesubaddd 9414 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  <_ 
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  <-> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
9489, 93bitrd 244 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  <->  ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
95 peano2re 9030 . . . . . . . . . . . . . . . . . 18  |-  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  e.  RR  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  e.  RR )
9692, 95syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  e.  RR )
97 ceige 11003 . . . . . . . . . . . . . . . . 17  |-  ( ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
9896, 97syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
99 ceicl 11002 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  ->  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )
10096, 99syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) )  e.  ZZ )
101100zred 10164 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) )  e.  RR )
102 letr 8959 . . . . . . . . . . . . . . . . 17  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  RR  /\  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  /\  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  RR )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  /\  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10326, 96, 101, 102syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  /\  (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10498, 103mpan2d 655 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_ 
( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  -> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10594, 104sylbid 206 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  ->  ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10688, 105syld 40 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  <_  sup ( ran  h ,  RR ,  <  )
)  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10783, 106mpan2d 655 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
108107adantrd 454 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) )
109108imp 418 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )
11024flcld 10977 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  ZZ )
111110adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( 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
) ) )  e.  ZZ )
112 0z 10082 . . . . . . . . . . . 12  |-  0  e.  ZZ
113112a1i 10 . . . . . . . . . . 11  |-  ( ( ( ( ( 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
) )  ->  0  e.  ZZ )
114100adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( 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
) )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )
115 elfz 10835 . . . . . . . . . . 11  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ZZ  /\  0  e.  ZZ  /\  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  <->  ( 0  <_ 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  /\  ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) ) )
116111, 113, 114, 115syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  <->  ( 0  <_ 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  /\  ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) ) )
11764, 109, 116mpbir2and 888 . . . . . . . . 9  |-  ( ( ( ( ( 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
) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
118 eqid 2316 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )
119 oveq1 5907 . . . . . . . . . . . 12  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
t  -  1 )  =  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 ) )
120119oveq1d 5915 . . . . . . . . . . 11  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
( t  -  1 )  x.  ( v  /  3 ) )  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )
121120eqeq2d 2327 . . . . . . . . . 10  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) )  <->  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) )
122121rspcev 2918 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  /\  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  ->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
123117, 118, 122sylancl 643 . . . . . . . 8  |-  ( ( ( ( ( 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
) )  ->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
124 ovex 5925 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
12539elrnmpt 4963 . . . . . . . . 9  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  _V  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  <->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) ) )
126124, 125ax-mp 8 . . . . . . . 8  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  <->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
127123, 126sylibr 203 . . . . . . 7  |-  ( ( ( ( ( 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 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) )
128 elun1 3376 . . . . . . 7  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  -> 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
129127, 128syl 15 . . . . . 6  |-  ( ( ( ( ( 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 ) )  e.  ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
130 elun2 3377 . . . . . . . 8  |-  ( ( h `  x )  e.  ran  h  -> 
( h `  x
)  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
13181, 130syl 15 . . . . . . 7  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
132131adantr 451 . . . . . 6  |-  ( ( ( ( ( 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
)  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
133129, 132ifclda 3626 . . . . 5  |-  ( ( ( ( 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.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
134133, 35fmptd 5722 . . . 4  |-  ( ( ( 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
) ) ) : RR --> ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
135 frn 5433 . . . 4  |-  ( ( 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
) ) ) : RR --> ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  ->  ran  ( 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
) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
136134, 135syl 15 . . 3  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( 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
) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
137 ssfi 7126 . . 3  |-  ( ( ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  e. 
Fin  /\  ran  ( 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 ) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )  ->  ran  ( 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. 
Fin )
13848, 136, 137syl2anc 642 . 2  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( 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. 
Fin )
13935mptpreima 5203 . . . 4  |-  ( `' ( 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
) ) ) " { t } )  =  { 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.  { t } }
140 unrab 3473 . . . . 5  |-  ( { x  e.  RR  | 
( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) }  u.  { x  e.  RR  | 
( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) } )  =  { x  e.  RR  |  ( ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) }
141 inrab 3474 . . . . . . . 8  |-  ( { x  e.  RR  | 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x ) }  i^i  { x  e.  RR  | 
( h `  x
)  =/=  0 } )  =  { x  e.  RR  |  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) }
142141ineq1i 3400 . . . . . . 7  |-  ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  =  ( { x  e.  RR  |  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) }  i^i  {
x  e.  RR  | 
t  =  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) } )
143 inrab 3474 . . . . . . 7  |-  ( { x  e.  RR  | 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) }  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  =  { x  e.  RR  |  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ) }
144142, 143eqtri 2336 . . . . . 6  |-  ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  =  {
x  e.  RR  | 
( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) }
145 unrab 3473 . . . . . . . 8  |-  ( { x  e.  RR  |  -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  =  { x  e.  RR  |  ( -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 ) }
146145ineq1i 3400 . . . . . . 7  |-  ( ( { x  e.  RR  |  -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  u.  { x  e.  RR  |  ( h `
 x )  =  0 } )  i^i 
{ x  e.  RR  |  t  =  (
h `  x ) } )  =  ( { x  e.  RR  |  ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 ) }  i^i  { x  e.  RR  |  t  =  ( h `  x
) } )
147 inrab 3474 . . . . . . 7  |-  ( { x  e.  RR  | 
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 ) }  i^i  { x  e.  RR  | 
t  =  ( h `
 x ) } )  =  { x  e.  RR  |  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) }
148146, 147eqtri 2336 . . . . . 6  |-  ( ( { x  e.  RR  |  -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  u.  { x  e.  RR  |  ( h `
 x )  =  0 } )  i^i 
{ x  e.  RR  |  t  =  (
h `  x ) } )  =  {
x  e.  RR  | 
( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) }
149144, 148uneq12i 3361 . . . . 5  |-  ( ( ( { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) }  i^i  {
x  e.  RR  | 
( h `  x
)  =/=  0 } )  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  u.  ( ( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )  =  ( { x  e.  RR  |  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ) }  u.  { x  e.  RR  |  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) } )
150 eqcom 2318 . . . . . . . 8  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  t  <-> 
t  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )
151 fvex 5577 . . . . . . . . . 10  |-  ( h `
 x )  e. 
_V
152124, 151ifex 3657 . . . . . . . . 9  |-  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
153152elsnc 3697 . . . . . . . 8  |-  ( 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.  {
t }  <->  if (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =  t )
154 ianor 474 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( |_ `  ( ( 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 ) )
155 nne 2483 . . . . . . . . . . . . 13  |-  ( -.  ( h `  x
)  =/=  0  <->  (
h `  x )  =  0 )
156155orbi2i 505 . . . . . . . . . . . 12  |-  ( ( -.  ( ( ( |_ `  ( ( 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 ) )
157154, 156bitr2i 241 . . . . . . . . . . 11  |-  ( ( -.  ( ( ( |_ `  ( ( 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 ) )
158157anbi1i 676 . . . . . . . . . 10  |-  ( ( ( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) )  <->  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( h `  x ) ) )
159158orbi2i 505 . . . . . . . . 9  |-  ( ( ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  \/  (
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) ) )  <-> 
( ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )  \/  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( h `  x ) ) ) )
160 eqif 3632 . . . . . . . . 9  |-  ( t  =  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
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( h `  x ) ) ) )
161159, 160bitr4i 243 . . . . . . . 8  |-  ( ( ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  \/  (
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) ) )  <-> 
t  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )
162150, 153, 1613bitr4i 268 . . . . . . 7  |-  ( 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.  {
t }  <->  ( (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) )
163162a1i 10 . . . . . 6  |-  ( 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.  {
t }  <->  ( (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) ) )
164163rabbiia 2812 . . . . 5  |-  { 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.  { t } }  =  {
x  e.  RR  | 
( ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )  \/  ( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) ) }
165140, 149, 1643eqtr4ri 2347 . . . 4  |-  { 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.  { t } }  =  ( ( ( { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) }  i^i  {
x  e.  RR  | 
( h `  x
)  =/=  0 } )  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  u.  ( ( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )
166139, 165eqtri 2336 . . 3  |-  ( `' ( 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
) ) ) " { t } )  =  ( ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  u.  (
( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )
167 eldifi 3332 . . . . . 6  |-  ( t  e.  ( ran  (
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 } )  ->  t  e.  ran  ( 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
) ) ) )
168 frn 5433 . . . . . . . 8  |-  ( ( 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
) ) ) : RR --> RR  ->  ran  ( 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
) ) )  C_  RR )
16936, 168syl 15 . . . . . . 7  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( 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
) ) )  C_  RR )
170169sseld 3213 . . . . . 6  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
t  e.  ran  (
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
) ) )  -> 
t  e.  RR ) )
171167, 170syl5 28 . . . . 5  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
t  e.  ( ran  ( 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 } )  ->  t  e.  RR ) )
172171imdistani 671 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  ( ran  ( 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 } ) )  ->  ( (
( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  RR ) )
173 rabiun2 25311 . . . . . . . . . 10  |-  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  U_ t  e. 
ran  h { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }
174 cnvimarndm 5071 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  dom  h
175 iunid 3994 . . . . . . . . . . . . . . . 16  |-  U_ t  e.  ran  h { t }  =  ran  h
176175imaeq2i 5047 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  ( `' h " ran  h
)
177 imaiun 5813 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  U_ t  e.  ran  h ( `' h " { t } )
178176, 177eqtr3i 2338 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  U_ t  e.  ran  h ( `' h " { t } )
179174, 178eqtr3i 2338 . . . . . . . . . . . . 13  |-  dom  h  =  U_ t  e.  ran  h ( `' h " { t } )
180 fdm 5431 . . . . . . . . . . . . . 14  |-  ( h : RR --> RR  ->  dom  h  =  RR )
18130, 180syl 15 . . . . . . . . . . . . 13  |-  ( h  e.  dom  S.1  ->  dom  h  =  RR )
182179, 181syl5eqr 2362 . . . . . . . . . . . 12  |-  ( h  e.  dom  S.1  ->  U_ t  e.  ran  h
( `' h " { t } )  =  RR )
183182ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  U_ t  e.  ran  h ( `' h " { t } )  =  RR )
184 rabeq 2816 . . . . . . . . . . 11  |-  ( U_ t  e.  ran  h ( `' h " { t } )  =  RR 
->  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) } )
185183, 184syl 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) } )
186173, 185syl5eqr 2362 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  U_ t  e.  ran  h { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) } )
187 fniniseg 5684 . . . . . . . . . . . . . . . . . 18  |-  ( h  Fn  RR  ->  (
x  e.  ( `' h " { t } )  <->  ( x  e.  RR  /\  ( h `
 x )  =  t ) ) )
18830, 76, 1873syl 18 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  ( x  e.  ( `' h " { t } )  <->  ( x  e.  RR  /\  ( h `
 x )  =  t ) ) )
189188simplbda 607 . . . . . . . . . . . . . . . 16  |-  ( ( h  e.  dom  S.1  /\  x  e.  ( `' h " { t } ) )  -> 
( h `  x
)  =  t )
190189breq2d 4072 . . . . . . . . . . . . . . 15  |-  ( ( h  e.  dom  S.1  /\  x  e.  ( `' h " { t } ) )  -> 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  <->  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t ) )
191190rabbidva 2813 . . . . . . . . . . . . . 14  |-  ( h  e.  dom  S.1  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
192 inrab2 3475 . . . . . . . . . . . . . . 15  |-  ( { x  e.  RR  | 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }  i^i  ( `' h " { t } ) )  =  { x  e.  ( RR  i^i  ( `' h " { t } ) )  |  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }
193 imassrn 5062 . . . . . . . . . . . . . . . . . 18  |-  ( `' h " { t } )  C_  ran  `' h
194 dfdm4 4909 . . . . . . . . . . . . . . . . . . 19  |-  dom  h  =  ran  `' h
195194, 181syl5eqr 2362 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  ran  `' h  =  RR )
196193, 195syl5sseq 3260 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  ( `' h " { t } )  C_  RR )
197 dfss1 3407 . . . . . . . . . . . . . . . . 17  |-  ( ( `' h " { t } )  C_  RR  <->  ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } ) )
198196, 197sylib 188 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } ) )
199 rabeq 2816 . . . . . . . . . . . . . . . 16  |-  ( ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } )  ->  { x  e.  ( RR  i^i  ( `' h " { t } ) )  |  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
200198, 199syl 15 . . . . . . . . . . . . . . 15  |-  ( h  e.  dom  S.1  ->  { x  e.  ( RR 
i^i  ( `' h " { t } ) )  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
t }  =  {
x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
201192, 200syl5eq 2360 . . . . . . . . . . . . . 14  |-  ( h  e.  dom  S.1  ->  ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t }  i^i  ( `' h " { t } ) )  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t } )
202191, 201eqtr4d 2351 . . . . . . . . . . . . 13  |-  ( h  e.  dom  S.1  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t }  i^i  ( `' h " { t } ) ) )
203202ad3antlr 711 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  ran  h )  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }