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

Theorem ismbf3d 22602
Description: Simplified form of ismbfd 22588. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypotheses
Ref Expression
ismbf3d.1  |-  ( ph  ->  F : A --> RR )
ismbf3d.2  |-  ( (
ph  /\  x  e.  RR )  ->  ( `' F " ( x (,) +oo ) )  e.  dom  vol )
Assertion
Ref Expression
ismbf3d  |-  ( ph  ->  F  e. MblFn )
Distinct variable groups:    x, F    ph, x
Allowed substitution hint:    A( x)

Proof of Theorem ismbf3d
Dummy variables  v  u  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ismbf3d.1 . 2  |-  ( ph  ->  F : A --> RR )
2 fimacnv 6025 . . . 4  |-  ( F : A --> RR  ->  ( `' F " RR )  =  A )
31, 2syl 17 . . 3  |-  ( ph  ->  ( `' F " RR )  =  A
)
4 imaiun 6163 . . . . 5  |-  ( `' F " U_ y  e.  NN  ( -u y (,) +oo ) )  = 
U_ y  e.  NN  ( `' F " ( -u y (,) +oo ) )
5 ioossre 11698 . . . . . . . . 9  |-  ( -u y (,) +oo )  C_  RR
65rgenw 2787 . . . . . . . 8  |-  A. y  e.  NN  ( -u y (,) +oo )  C_  RR
7 iunss 4338 . . . . . . . 8  |-  ( U_ y  e.  NN  ( -u y (,) +oo )  C_  RR  <->  A. y  e.  NN  ( -u y (,) +oo )  C_  RR )
86, 7mpbir 213 . . . . . . 7  |-  U_ y  e.  NN  ( -u y (,) +oo )  C_  RR
9 renegcl 9939 . . . . . . . . . . 11  |-  ( z  e.  RR  ->  -u z  e.  RR )
10 arch 10868 . . . . . . . . . . 11  |-  ( -u z  e.  RR  ->  E. y  e.  NN  -u z  <  y )
119, 10syl 17 . . . . . . . . . 10  |-  ( z  e.  RR  ->  E. y  e.  NN  -u z  <  y
)
12 simpl 459 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  z  e.  RR )
1312biantrurd 511 . . . . . . . . . . . 12  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  ( -u y  < 
z  <->  ( z  e.  RR  /\  -u y  <  z ) ) )
14 nnre 10618 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  RR )
15 ltnegcon1 10117 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  y  e.  RR )  ->  ( -u z  < 
y  <->  -u y  <  z
) )
1614, 15sylan2 477 . . . . . . . . . . . 12  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  ( -u z  < 
y  <->  -u y  <  z
) )
1714adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  y  e.  RR )
1817renegcld 10048 . . . . . . . . . . . . . 14  |-  ( ( z  e.  RR  /\  y  e.  NN )  -> 
-u y  e.  RR )
1918rexrd 9692 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  y  e.  NN )  -> 
-u y  e.  RR* )
20 elioopnf 11730 . . . . . . . . . . . . 13  |-  ( -u y  e.  RR*  ->  (
z  e.  ( -u y (,) +oo )  <->  ( z  e.  RR  /\  -u y  <  z ) ) )
2119, 20syl 17 . . . . . . . . . . . 12  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  ( z  e.  (
-u y (,) +oo ) 
<->  ( z  e.  RR  /\  -u y  <  z ) ) )
2213, 16, 213bitr4d 289 . . . . . . . . . . 11  |-  ( ( z  e.  RR  /\  y  e.  NN )  ->  ( -u z  < 
y  <->  z  e.  (
-u y (,) +oo ) ) )
2322rexbidva 2937 . . . . . . . . . 10  |-  ( z  e.  RR  ->  ( E. y  e.  NN  -u z  <  y  <->  E. y  e.  NN  z  e.  (
-u y (,) +oo ) ) )
2411, 23mpbid 214 . . . . . . . . 9  |-  ( z  e.  RR  ->  E. y  e.  NN  z  e.  (
-u y (,) +oo ) )
25 eliun 4302 . . . . . . . . 9  |-  ( z  e.  U_ y  e.  NN  ( -u y (,) +oo )  <->  E. y  e.  NN  z  e.  (
-u y (,) +oo ) )
2624, 25sylibr 216 . . . . . . . 8  |-  ( z  e.  RR  ->  z  e.  U_ y  e.  NN  ( -u y (,) +oo ) )
2726ssriv 3469 . . . . . . 7  |-  RR  C_  U_ y  e.  NN  ( -u y (,) +oo )
288, 27eqssi 3481 . . . . . 6  |-  U_ y  e.  NN  ( -u y (,) +oo )  =  RR
2928imaeq2i 5183 . . . . 5  |-  ( `' F " U_ y  e.  NN  ( -u y (,) +oo ) )  =  ( `' F " RR )
304, 29eqtr3i 2454 . . . 4  |-  U_ y  e.  NN  ( `' F " ( -u y (,) +oo ) )  =  ( `' F " RR )
31 ismbf3d.2 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( `' F " ( x (,) +oo ) )  e.  dom  vol )
3231ralrimiva 2840 . . . . . . 7  |-  ( ph  ->  A. x  e.  RR  ( `' F " ( x (,) +oo ) )  e.  dom  vol )
3314renegcld 10048 . . . . . . 7  |-  ( y  e.  NN  ->  -u y  e.  RR )
34 oveq1 6310 . . . . . . . . . 10  |-  ( x  =  -u y  ->  (
x (,) +oo )  =  ( -u y (,) +oo ) )
3534imaeq2d 5185 . . . . . . . . 9  |-  ( x  =  -u y  ->  ( `' F " ( x (,) +oo ) )  =  ( `' F " ( -u y (,) +oo ) ) )
3635eleq1d 2492 . . . . . . . 8  |-  ( x  =  -u y  ->  (
( `' F "
( x (,) +oo ) )  e.  dom  vol  <->  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
)
3736rspccva 3182 . . . . . . 7  |-  ( ( A. x  e.  RR  ( `' F " ( x (,) +oo ) )  e.  dom  vol  /\  -u y  e.  RR )  ->  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
3832, 33, 37syl2an 480 . . . . . 6  |-  ( (
ph  /\  y  e.  NN )  ->  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
3938ralrimiva 2840 . . . . 5  |-  ( ph  ->  A. y  e.  NN  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
40 iunmbl 22498 . . . . 5  |-  ( A. y  e.  NN  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol  ->  U_ y  e.  NN  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
4139, 40syl 17 . . . 4  |-  ( ph  ->  U_ y  e.  NN  ( `' F " ( -u y (,) +oo ) )  e.  dom  vol )
4230, 41syl5eqelr 2516 . . 3  |-  ( ph  ->  ( `' F " RR )  e.  dom  vol )
433, 42eqeltrrd 2512 . 2  |-  ( ph  ->  A  e.  dom  vol )
44 imaiun 6163 . . . . . . 7  |-  ( `' F " U_ y  e.  NN  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  = 
U_ y  e.  NN  ( `' F " ( -oo (,] ( z  -  (
1  /  y ) ) ) )
45 eliun 4302 . . . . . . . . . 10  |-  ( x  e.  U_ y  e.  NN  ( -oo (,] ( z  -  (
1  /  y ) ) )  <->  E. y  e.  NN  x  e.  ( -oo (,] ( z  -  ( 1  / 
y ) ) ) )
46 3simpb 1004 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\ -oo 
<  x  /\  x  <_  ( z  -  (
1  /  y ) ) )  ->  (
x  e.  RR  /\  x  <_  ( z  -  ( 1  /  y
) ) ) )
47 simplr 761 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  z  e.  RR )
48 nnrp 11313 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  NN  ->  y  e.  RR+ )
4948ad2antrl 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  y  e.  RR+ )
5049rpreccld 11353 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  ( 1  /  y )  e.  RR+ )
5147, 50ltsubrpd 11372 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  ( z  -  ( 1  / 
y ) )  < 
z )
52 simprr 765 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  x  e.  RR )
53 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  RR )  ->  z  e.  RR )
54 nnrecre 10648 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  NN  ->  (
1  /  y )  e.  RR )
55 resubcl 9940 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  e.  RR  /\  ( 1  /  y
)  e.  RR )  ->  ( z  -  ( 1  /  y
) )  e.  RR )
5653, 54, 55syl2an 480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
z  -  ( 1  /  y ) )  e.  RR )
5756adantrr 722 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  ( z  -  ( 1  / 
y ) )  e.  RR )
58 lelttr 9726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  ( z  -  (
1  /  y ) )  e.  RR  /\  z  e.  RR )  ->  ( ( x  <_ 
( z  -  (
1  /  y ) )  /\  ( z  -  ( 1  / 
y ) )  < 
z )  ->  x  <  z ) )
5952, 57, 47, 58syl3anc 1265 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  ( (
x  <_  ( z  -  ( 1  / 
y ) )  /\  ( z  -  (
1  /  y ) )  <  z )  ->  x  <  z
) )
6051, 59mpan2d 679 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
y  e.  NN  /\  x  e.  RR )
)  ->  ( x  <_  ( z  -  (
1  /  y ) )  ->  x  <  z ) )
6160anassrs 653 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  /\  x  e.  RR )  ->  ( x  <_ 
( z  -  (
1  /  y ) )  ->  x  <  z ) )
6261imdistanda 698 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( x  e.  RR  /\  x  <_  ( z  -  ( 1  / 
y ) ) )  ->  ( x  e.  RR  /\  x  < 
z ) ) )
6346, 62syl5 34 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( x  e.  RR  /\ -oo  <  x  /\  x  <_  ( z  -  (
1  /  y ) ) )  ->  (
x  e.  RR  /\  x  <  z ) ) )
64 mnfxr 11416 . . . . . . . . . . . . . . . 16  |- -oo  e.  RR*
65 elioc2 11699 . . . . . . . . . . . . . . . 16  |-  ( ( -oo  e.  RR*  /\  (
z  -  ( 1  /  y ) )  e.  RR )  -> 
( x  e.  ( -oo (,] ( z  -  ( 1  / 
y ) ) )  <-> 
( x  e.  RR  /\ -oo  <  x  /\  x  <_  ( z  -  (
1  /  y ) ) ) ) )
6664, 56, 65sylancr 668 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
x  e.  ( -oo (,] ( z  -  (
1  /  y ) ) )  <->  ( x  e.  RR  /\ -oo  <  x  /\  x  <_  (
z  -  ( 1  /  y ) ) ) ) )
67 rexr 9688 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  RR  ->  z  e.  RR* )
6867adantl 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  RR )  ->  z  e. 
RR* )
69 elioomnf 11731 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  RR*  ->  ( x  e.  ( -oo (,) z )  <->  ( x  e.  RR  /\  x  < 
z ) ) )
7068, 69syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  RR )  ->  ( x  e.  ( -oo (,) z )  <->  ( x  e.  RR  /\  x  < 
z ) ) )
7170adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
x  e.  ( -oo (,) z )  <->  ( x  e.  RR  /\  x  < 
z ) ) )
7263, 66, 713imtr4d 272 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
x  e.  ( -oo (,] ( z  -  (
1  /  y ) ) )  ->  x  e.  ( -oo (,) z
) ) )
7372rexlimdva 2918 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  RR )  ->  ( E. y  e.  NN  x  e.  ( -oo (,] (
z  -  ( 1  /  y ) ) )  ->  x  e.  ( -oo (,) z ) ) )
7473, 70sylibd 218 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( E. y  e.  NN  x  e.  ( -oo (,] (
z  -  ( 1  /  y ) ) )  ->  ( x  e.  RR  /\  x  < 
z ) ) )
75 simprl 763 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  x  e.  RR )
7675adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  x  e.  RR )
77 mnflt 11427 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  -> -oo  <  x )
7876, 77syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  -> -oo  <  x )
7956ad2ant2r 752 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  ( z  -  ( 1  /  y
) )  e.  RR )
8054ad2antrl 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  ( 1  / 
y )  e.  RR )
81 simplr 761 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  z  e.  RR )
8281adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  z  e.  RR )
83 simprr 765 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  ( 1  / 
y )  <  (
z  -  x ) )
8480, 82, 76, 83ltsub13d 10221 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  x  <  (
z  -  ( 1  /  y ) ) )
8576, 79, 84ltled 9785 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  x  <_  (
z  -  ( 1  /  y ) ) )
8666ad2ant2r 752 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  ( x  e.  ( -oo (,] (
z  -  ( 1  /  y ) ) )  <->  ( x  e.  RR  /\ -oo  <  x  /\  x  <_  (
z  -  ( 1  /  y ) ) ) ) )
8776, 78, 85, 86mpbir3and 1189 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  RR )  /\  ( x  e.  RR  /\  x  <  z ) )  /\  ( y  e.  NN  /\  (
1  /  y )  <  ( z  -  x ) ) )  ->  x  e.  ( -oo (,] ( z  -  ( 1  / 
y ) ) ) )
8881, 75resubcld 10049 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  ( z  -  x )  e.  RR )
89 simprr 765 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  x  <  z
)
9075, 81posdifd 10202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  ( x  < 
z  <->  0  <  (
z  -  x ) ) )
9189, 90mpbid 214 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  0  <  (
z  -  x ) )
92 nnrecl 10869 . . . . . . . . . . . . . . 15  |-  ( ( ( z  -  x
)  e.  RR  /\  0  <  ( z  -  x ) )  ->  E. y  e.  NN  ( 1  /  y
)  <  ( z  -  x ) )
9388, 91, 92syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  E. y  e.  NN  ( 1  /  y
)  <  ( z  -  x ) )
9487, 93reximddv 2902 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  RR )  /\  (
x  e.  RR  /\  x  <  z ) )  ->  E. y  e.  NN  x  e.  ( -oo (,] ( z  -  (
1  /  y ) ) ) )
9594ex 436 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  RR )  ->  ( ( x  e.  RR  /\  x  <  z )  ->  E. y  e.  NN  x  e.  ( -oo (,] ( z  -  (
1  /  y ) ) ) ) )
9674, 95impbid 194 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  RR )  ->  ( E. y  e.  NN  x  e.  ( -oo (,] (
z  -  ( 1  /  y ) ) )  <->  ( x  e.  RR  /\  x  < 
z ) ) )
9796, 70bitr4d 260 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR )  ->  ( E. y  e.  NN  x  e.  ( -oo (,] (
z  -  ( 1  /  y ) ) )  <->  x  e.  ( -oo (,) z ) ) )
9845, 97syl5bb 261 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  RR )  ->  ( x  e.  U_ y  e.  NN  ( -oo (,] ( z  -  (
1  /  y ) ) )  <->  x  e.  ( -oo (,) z ) ) )
9998eqrdv 2420 . . . . . . . 8  |-  ( (
ph  /\  z  e.  RR )  ->  U_ y  e.  NN  ( -oo (,] ( z  -  (
1  /  y ) ) )  =  ( -oo (,) z ) )
10099imaeq2d 5185 . . . . . . 7  |-  ( (
ph  /\  z  e.  RR )  ->  ( `' F " U_ y  e.  NN  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  =  ( `' F "
( -oo (,) z ) ) )
10144, 100syl5eqr 2478 . . . . . 6  |-  ( (
ph  /\  z  e.  RR )  ->  U_ y  e.  NN  ( `' F " ( -oo (,] (
z  -  ( 1  /  y ) ) ) )  =  ( `' F " ( -oo (,) z ) ) )
1021ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  F : A --> RR )
103 ffun 5746 . . . . . . . . . . 11  |-  ( F : A --> RR  ->  Fun 
F )
104 funcnvcnv 5657 . . . . . . . . . . 11  |-  ( Fun 
F  ->  Fun  `' `' F )
105 imadif 5674 . . . . . . . . . . 11  |-  ( Fun  `' `' F  ->  ( `' F " ( RR 
\  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) ) )  =  ( ( `' F " RR )  \  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) ) ) )
106102, 103, 104, 1054syl 19 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( `' F " ( RR 
\  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) ) )  =  ( ( `' F " RR )  \  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) ) ) )
10764a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  -> -oo  e.  RR* )
10856rexrd 9692 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
z  -  ( 1  /  y ) )  e.  RR* )
109 pnfxr 11414 . . . . . . . . . . . . . . 15  |- +oo  e.  RR*
110109a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  -> +oo  e.  RR* )
111 mnflt 11427 . . . . . . . . . . . . . . 15  |-  ( ( z  -  ( 1  /  y ) )  e.  RR  -> -oo  <  ( z  -  ( 1  /  y ) ) )
11256, 111syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  -> -oo  <  ( z  -  ( 1  /  y ) ) )
113 ltpnf 11424 . . . . . . . . . . . . . . 15  |-  ( ( z  -  ( 1  /  y ) )  e.  RR  ->  (
z  -  ( 1  /  y ) )  < +oo )
11456, 113syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
z  -  ( 1  /  y ) )  < +oo )
115 df-ioc 11642 . . . . . . . . . . . . . . 15  |-  (,]  =  ( u  e.  RR* ,  v  e.  RR*  |->  { w  e.  RR*  |  ( u  <  w  /\  w  <_  v ) } )
116 df-ioo 11641 . . . . . . . . . . . . . . 15  |-  (,)  =  ( u  e.  RR* ,  v  e.  RR*  |->  { w  e.  RR*  |  ( u  <  w  /\  w  <  v ) } )
117 xrltnle 9703 . . . . . . . . . . . . . . 15  |-  ( ( ( z  -  (
1  /  y ) )  e.  RR*  /\  x  e.  RR* )  ->  (
( z  -  (
1  /  y ) )  <  x  <->  -.  x  <_  ( z  -  (
1  /  y ) ) ) )
118 xrlelttr 11455 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR*  /\  (
z  -  ( 1  /  y ) )  e.  RR*  /\ +oo  e.  RR* )  ->  ( (
x  <_  ( z  -  ( 1  / 
y ) )  /\  ( z  -  (
1  /  y ) )  < +oo )  ->  x  < +oo )
)
119 xrlttr 11441 . . . . . . . . . . . . . . 15  |-  ( ( -oo  e.  RR*  /\  (
z  -  ( 1  /  y ) )  e.  RR*  /\  x  e.  RR* )  ->  (
( -oo  <  ( z  -  ( 1  / 
y ) )  /\  ( z  -  (
1  /  y ) )  <  x )  -> -oo  <  x ) )
120115, 116, 117, 116, 118, 119ixxun 11653 . . . . . . . . . . . . . 14  |-  ( ( ( -oo  e.  RR*  /\  ( z  -  (
1  /  y ) )  e.  RR*  /\ +oo  e.  RR* )  /\  ( -oo  <  ( z  -  ( 1  /  y
) )  /\  (
z  -  ( 1  /  y ) )  < +oo ) )  -> 
( ( -oo (,] ( z  -  (
1  /  y ) ) )  u.  (
( z  -  (
1  /  y ) ) (,) +oo )
)  =  ( -oo (,) +oo ) )
121107, 108, 110, 112, 114, 120syl32anc 1273 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( -oo (,] ( z  -  ( 1  / 
y ) ) )  u.  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )  =  ( -oo (,) +oo )
)
122 uncom 3611 . . . . . . . . . . . . 13  |-  ( ( -oo (,] ( z  -  ( 1  / 
y ) ) )  u.  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )  =  ( ( ( z  -  ( 1  /  y
) ) (,) +oo )  u.  ( -oo (,] ( z  -  (
1  /  y ) ) ) )
123 ioomax 11711 . . . . . . . . . . . . 13  |-  ( -oo (,) +oo )  =  RR
124121, 122, 1233eqtr3g 2487 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( ( z  -  ( 1  /  y
) ) (,) +oo )  u.  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  =  RR )
125 ioossre 11698 . . . . . . . . . . . . 13  |-  ( ( z  -  ( 1  /  y ) ) (,) +oo )  C_  RR
126 incom 3656 . . . . . . . . . . . . . 14  |-  ( ( ( z  -  (
1  /  y ) ) (,) +oo )  i^i  ( -oo (,] (
z  -  ( 1  /  y ) ) ) )  =  ( ( -oo (,] (
z  -  ( 1  /  y ) ) )  i^i  ( ( z  -  ( 1  /  y ) ) (,) +oo ) )
127115, 116, 117ixxdisj 11652 . . . . . . . . . . . . . . . 16  |-  ( ( -oo  e.  RR*  /\  (
z  -  ( 1  /  y ) )  e.  RR*  /\ +oo  e.  RR* )  ->  ( ( -oo (,] ( z  -  ( 1  /  y
) ) )  i^i  ( ( z  -  ( 1  /  y
) ) (,) +oo ) )  =  (/) )
12864, 109, 127mp3an13 1352 . . . . . . . . . . . . . . 15  |-  ( ( z  -  ( 1  /  y ) )  e.  RR*  ->  ( ( -oo (,] ( z  -  ( 1  / 
y ) ) )  i^i  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )  =  (/) )
129108, 128syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( -oo (,] ( z  -  ( 1  / 
y ) ) )  i^i  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )  =  (/) )
130126, 129syl5eq 2476 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( ( z  -  ( 1  /  y
) ) (,) +oo )  i^i  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  =  (/) )
131 uneqdifeq 3885 . . . . . . . . . . . . 13  |-  ( ( ( ( z  -  ( 1  /  y
) ) (,) +oo )  C_  RR  /\  (
( ( z  -  ( 1  /  y
) ) (,) +oo )  i^i  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  =  (/) )  ->  ( ( ( ( z  -  ( 1  /  y
) ) (,) +oo )  u.  ( -oo (,] ( z  -  (
1  /  y ) ) ) )  =  RR  <->  ( RR  \ 
( ( z  -  ( 1  /  y
) ) (,) +oo ) )  =  ( -oo (,] ( z  -  ( 1  / 
y ) ) ) ) )
132125, 130, 131sylancr 668 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( ( ( z  -  ( 1  / 
y ) ) (,) +oo )  u.  ( -oo (,] ( z  -  ( 1  /  y
) ) ) )  =  RR  <->  ( RR  \  ( ( z  -  ( 1  /  y
) ) (,) +oo ) )  =  ( -oo (,] ( z  -  ( 1  / 
y ) ) ) ) )
133124, 132mpbid 214 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( RR  \  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )  =  ( -oo (,] ( z  -  ( 1  / 
y ) ) ) )
134133imaeq2d 5185 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( `' F " ( RR 
\  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) ) )  =  ( `' F "
( -oo (,] ( z  -  ( 1  / 
y ) ) ) ) )
135106, 134eqtr3d 2466 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( `' F " RR )  \  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) ) )  =  ( `' F " ( -oo (,] ( z  -  (
1  /  y ) ) ) ) )
13642ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( `' F " RR )  e.  dom  vol )
13732ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  A. x  e.  RR  ( `' F " ( x (,) +oo ) )  e.  dom  vol )
138 oveq1 6310 . . . . . . . . . . . . . 14  |-  ( x  =  ( z  -  ( 1  /  y
) )  ->  (
x (,) +oo )  =  ( ( z  -  ( 1  / 
y ) ) (,) +oo ) )
139138imaeq2d 5185 . . . . . . . . . . . . 13  |-  ( x  =  ( z  -  ( 1  /  y
) )  ->  ( `' F " ( x (,) +oo ) )  =  ( `' F " ( ( z  -  ( 1  /  y
) ) (,) +oo ) ) )
140139eleq1d 2492 . . . . . . . . . . . 12  |-  ( x  =  ( z  -  ( 1  /  y
) )  ->  (
( `' F "
( x (,) +oo ) )  e.  dom  vol  <->  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) )  e.  dom  vol )
)
141140rspcv 3179 . . . . . . . . . . 11  |-  ( ( z  -  ( 1  /  y ) )  e.  RR  ->  ( A. x  e.  RR  ( `' F " ( x (,) +oo ) )  e.  dom  vol  ->  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) )  e.  dom  vol )
)
14256, 137, 141sylc 63 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) )  e.  dom  vol )
143 difmbl 22488 . . . . . . . . . 10  |-  ( ( ( `' F " RR )  e.  dom  vol 
/\  ( `' F " ( ( z  -  ( 1  /  y
) ) (,) +oo ) )  e.  dom  vol )  ->  ( ( `' F " RR ) 
\  ( `' F " ( ( z  -  ( 1  /  y
) ) (,) +oo ) ) )  e. 
dom  vol )
144136, 142, 143syl2anc 666 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  (
( `' F " RR )  \  ( `' F " ( ( z  -  ( 1  /  y ) ) (,) +oo ) ) )  e.  dom  vol )
145135, 144eqeltrrd 2512 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  RR )  /\  y  e.  NN )  ->  ( `' F " ( -oo (,] ( z  -  (
1  /  y ) ) ) )  e. 
dom  vol )
146145ralrimiva 2840 . . . . . . 7  |-  ( (
ph  /\  z  e.  RR )  ->  A. y  e.  NN  ( `' F " ( -oo (,] (
z  -  ( 1  /  y ) ) ) )  e.  dom  vol )
147 iunmbl 22498 . . . . . . 7  |-  ( A. y  e.  NN  ( `' F " ( -oo (,] ( z  -  (
1  /  y ) ) ) )  e. 
dom  vol  ->  U_ y  e.  NN  ( `' F " ( -oo (,] (
z  -  ( 1  /  y ) ) ) )  e.  dom  vol )
148146, 147syl 17 . . . . . 6  |-  ( (
ph  /\  z  e.  RR )  ->  U_ y  e.  NN  ( `' F " ( -oo (,] (
z  -  ( 1  /  y ) ) ) )  e.  dom  vol )
149101, 148eqeltrrd 2512 . . . . 5  |-  ( (
ph  /\  z  e.  RR )  ->  ( `' F " ( -oo (,) z ) )  e. 
dom  vol )
150149ralrimiva 2840 . . . 4  |-  ( ph  ->  A. z  e.  RR  ( `' F " ( -oo (,) z ) )  e. 
dom  vol )
151 oveq2 6311 . . . . . . 7  |-  ( z  =  x  ->  ( -oo (,) z )  =  ( -oo (,) x
) )
152151imaeq2d 5185 . . . . . 6  |-  ( z  =  x  ->  ( `' F " ( -oo (,) z ) )  =  ( `' F "
( -oo (,) x ) ) )
153152eleq1d 2492 . . . . 5  |-  ( z  =  x  ->  (
( `' F "
( -oo (,) z ) )  e.  dom  vol  <->  ( `' F " ( -oo (,) x ) )  e. 
dom  vol ) )
154153cbvralv 3056 . . . 4  |-  ( A. z  e.  RR  ( `' F " ( -oo (,) z ) )  e. 
dom  vol  <->  A. x  e.  RR  ( `' F " ( -oo (,) x ) )  e. 
dom  vol )
155150, 154sylib 200 . . 3  |-  ( ph  ->  A. x  e.  RR  ( `' F " ( -oo (,) x ) )  e. 
dom  vol )
156155r19.21bi 2795 . 2  |-  ( (
ph  /\  x  e.  RR )  ->  ( `' F " ( -oo (,) x ) )  e. 
dom  vol )
1571, 43, 31, 156ismbf2d 22589 1  |-  ( ph  ->  F  e. MblFn )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 983    = wceq 1438    e. wcel 1869   A.wral 2776   E.wrex 2777    \ cdif 3434    u. cun 3435    i^i cin 3436    C_ wss 3437   (/)c0 3762   U_ciun 4297   class class class wbr 4421   `'ccnv 4850   dom cdm 4851   "cima 4854   Fun wfun 5593   -->wf 5595  (class class class)co 6303   RRcr 9540   0cc0 9541   1c1 9542   +oocpnf 9674   -oocmnf 9675   RR*cxr 9676    < clt 9677    <_ cle 9678    - cmin 9862   -ucneg 9863    / cdiv 10271   NNcn 10611   RR+crp 11304   (,)cioo 11637   (,]cioc 11638   volcvol 22407  MblFncmbf 22564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cc 8867  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-disj 4393  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-of 6543  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-q 11267  df-rp 11305  df-xadd 11412  df-ioo 11641  df-ioc 11642  df-ico 11643  df-icc 11644  df-fz 11787  df-fzo 11918  df-fl 12029  df-seq 12215  df-exp 12274  df-hash 12517  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-clim 13545  df-rlim 13546  df-sum 13746  df-xmet 18956  df-met 18957  df-ovol 22408  df-vol 22410  df-mbf 22569
This theorem is referenced by:  mbfaddlem  22608  mbfsup  22612
  Copyright terms: Public domain W3C validator