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

Theorem ioombl 20890
Description: An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
Assertion
Ref Expression
ioombl  |-  ( A (,) B )  e. 
dom  vol

Proof of Theorem ioombl
Dummy variables  x  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snunioo 11400 . . . . . . . . 9  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  ( { A }  u.  ( A (,) B ) )  =  ( A [,) B ) )
213expa 1182 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( { A }  u.  ( A (,) B ) )  =  ( A [,) B
) )
32adantrr 711 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( { A }  u.  ( A (,) B ) )  =  ( A [,) B ) )
4 lbico1 11340 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  A  e.  ( A [,) B
) )
543expa 1182 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  A  e.  ( A [,) B ) )
65adantrr 711 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  A  e.  ( A [,) B ) )
76snssd 4008 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  { A }  C_  ( A [,) B ) )
8 iccid 11335 . . . . . . . . . . 11  |-  ( A  e.  RR*  ->  ( A [,] A )  =  { A } )
98ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( A [,] A )  =  { A } )
109ineq1d 3541 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( ( A [,] A )  i^i  ( A (,) B
) )  =  ( { A }  i^i  ( A (,) B ) ) )
11 simpll 748 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  A  e.  RR* )
12 simplr 749 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  B  e.  RR* )
13 df-icc 11297 . . . . . . . . . . 11  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
14 df-ioo 11294 . . . . . . . . . . 11  |-  (,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <  z  /\  z  <  y ) } )
15 xrltnle 9433 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  w  e.  RR* )  ->  ( A  <  w  <->  -.  w  <_  A ) )
1613, 14, 15ixxdisj 11305 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  A  e.  RR*  /\  B  e. 
RR* )  ->  (
( A [,] A
)  i^i  ( A (,) B ) )  =  (/) )
1711, 11, 12, 16syl3anc 1213 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( ( A [,] A )  i^i  ( A (,) B
) )  =  (/) )
1810, 17eqtr3d 2469 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( { A }  i^i  ( A (,) B ) )  =  (/) )
19 uneqdifeq 3757 . . . . . . . 8  |-  ( ( { A }  C_  ( A [,) B )  /\  ( { A }  i^i  ( A (,) B ) )  =  (/) )  ->  ( ( { A }  u.  ( A (,) B ) )  =  ( A [,) B )  <->  ( ( A [,) B )  \  { A } )  =  ( A (,) B
) ) )
207, 18, 19syl2anc 656 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( ( { A }  u.  ( A (,) B ) )  =  ( A [,) B )  <->  ( ( A [,) B )  \  { A } )  =  ( A (,) B
) ) )
213, 20mpbid 210 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( ( A [,) B )  \  { A } )  =  ( A (,) B
) )
22 mnfxr 11084 . . . . . . . . . 10  |- -oo  e.  RR*
2322a1i 11 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  -> -oo  e.  RR* )
24 simprr 751 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  -> -oo  <  A
)
25 simprl 750 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  A  <  B )
26 xrre2 11132 . . . . . . . . 9  |-  ( ( ( -oo  e.  RR*  /\  A  e.  RR*  /\  B  e.  RR* )  /\  ( -oo  <  A  /\  A  <  B ) )  ->  A  e.  RR )
2723, 11, 12, 24, 25, 26syl32anc 1221 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  A  e.  RR )
28 icombl 20889 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR* )  -> 
( A [,) B
)  e.  dom  vol )
2927, 12, 28syl2anc 656 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( A [,) B )  e.  dom  vol )
3027snssd 4008 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  { A }  C_  RR )
31 ovolsn 20822 . . . . . . . . 9  |-  ( A  e.  RR  ->  ( vol* `  { A } )  =  0 )
3227, 31syl 16 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( vol* `  { A }
)  =  0 )
33 nulmbl 20861 . . . . . . . 8  |-  ( ( { A }  C_  RR  /\  ( vol* `  { A } )  =  0 )  ->  { A }  e.  dom  vol )
3430, 32, 33syl2anc 656 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  { A }  e.  dom  vol )
35 difmbl 20868 . . . . . . 7  |-  ( ( ( A [,) B
)  e.  dom  vol  /\ 
{ A }  e.  dom  vol )  ->  (
( A [,) B
)  \  { A } )  e.  dom  vol )
3629, 34, 35syl2anc 656 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( ( A [,) B )  \  { A } )  e. 
dom  vol )
3721, 36eqeltrrd 2510 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\ -oo  <  A )
)  ->  ( A (,) B )  e.  dom  vol )
3837expr 612 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( -oo  <  A  ->  ( A (,) B )  e.  dom  vol ) )
39 uncom 3490 . . . . . . . . 9  |-  ( ( B [,) +oo )  u.  ( -oo (,) B
) )  =  ( ( -oo (,) B
)  u.  ( B [,) +oo ) )
4022a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  -> -oo  e.  RR* )
41 simplr 749 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  B  e.  RR* )
42 pnfxr 11082 . . . . . . . . . . 11  |- +oo  e.  RR*
4342a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  -> +oo  e.  RR* )
44 simpll 748 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  A  e.  RR* )
45 mnfle 11103 . . . . . . . . . . . 12  |-  ( A  e.  RR*  -> -oo  <_  A )
4645ad2antrr 720 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  -> -oo  <_  A )
47 simpr 458 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  A  <  B
)
4840, 44, 41, 46, 47xrlelttrd 11124 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  -> -oo  <  B )
49 pnfge 11100 . . . . . . . . . . 11  |-  ( B  e.  RR*  ->  B  <_ +oo )
5041, 49syl 16 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  B  <_ +oo )
51 df-ico 11296 . . . . . . . . . . 11  |-  [,)  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  y ) } )
52 xrlenlt 9432 . . . . . . . . . . 11  |-  ( ( B  e.  RR*  /\  w  e.  RR* )  ->  ( B  <_  w  <->  -.  w  <  B ) )
53 xrltletr 11121 . . . . . . . . . . 11  |-  ( ( w  e.  RR*  /\  B  e.  RR*  /\ +oo  e.  RR* )  ->  ( (
w  <  B  /\  B  <_ +oo )  ->  w  < +oo ) )
54 xrltletr 11121 . . . . . . . . . . 11  |-  ( ( -oo  e.  RR*  /\  B  e.  RR*  /\  w  e. 
RR* )  ->  (
( -oo  <  B  /\  B  <_  w )  -> -oo  <  w ) )
5514, 51, 52, 14, 53, 54ixxun 11306 . . . . . . . . . 10  |-  ( ( ( -oo  e.  RR*  /\  B  e.  RR*  /\ +oo  e.  RR* )  /\  ( -oo  <  B  /\  B  <_ +oo ) )  -> 
( ( -oo (,) B )  u.  ( B [,) +oo ) )  =  ( -oo (,) +oo ) )
5640, 41, 43, 48, 50, 55syl32anc 1221 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( -oo (,) B )  u.  ( B [,) +oo ) )  =  ( -oo (,) +oo ) )
5739, 56syl5eq 2479 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( B [,) +oo )  u.  ( -oo (,) B
) )  =  ( -oo (,) +oo )
)
58 ioomax 11360 . . . . . . . 8  |-  ( -oo (,) +oo )  =  RR
5957, 58syl6eq 2483 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( B [,) +oo )  u.  ( -oo (,) B
) )  =  RR )
60 ssun1 3509 . . . . . . . . 9  |-  ( B [,) +oo )  C_  ( ( B [,) +oo )  u.  ( -oo (,) B ) )
6160, 59syl5sseq 3394 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B [,) +oo )  C_  RR )
62 incom 3533 . . . . . . . . 9  |-  ( ( B [,) +oo )  i^i  ( -oo (,) B
) )  =  ( ( -oo (,) B
)  i^i  ( B [,) +oo ) )
6314, 51, 52ixxdisj 11305 . . . . . . . . . 10  |-  ( ( -oo  e.  RR*  /\  B  e.  RR*  /\ +oo  e.  RR* )  ->  ( ( -oo (,) B )  i^i  ( B [,) +oo ) )  =  (/) )
6440, 41, 43, 63syl3anc 1213 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( -oo (,) B )  i^i  ( B [,) +oo ) )  =  (/) )
6562, 64syl5eq 2479 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( B [,) +oo )  i^i  ( -oo (,) B
) )  =  (/) )
66 uneqdifeq 3757 . . . . . . . 8  |-  ( ( ( B [,) +oo )  C_  RR  /\  (
( B [,) +oo )  i^i  ( -oo (,) B ) )  =  (/) )  ->  ( ( ( B [,) +oo )  u.  ( -oo (,) B ) )  =  RR  <->  ( RR  \ 
( B [,) +oo ) )  =  ( -oo (,) B ) ) )
6761, 65, 66syl2anc 656 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( ( B [,) +oo )  u.  ( -oo (,) B
) )  =  RR  <->  ( RR  \  ( B [,) +oo ) )  =  ( -oo (,) B ) ) )
6859, 67mpbid 210 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( RR  \ 
( B [,) +oo ) )  =  ( -oo (,) B ) )
69 rembl 20866 . . . . . . 7  |-  RR  e.  dom  vol
70 xrleloe 11111 . . . . . . . . . . 11  |-  ( ( B  e.  RR*  /\ +oo  e.  RR* )  ->  ( B  <_ +oo  <->  ( B  < +oo  \/  B  = +oo ) ) )
7141, 42, 70sylancl 657 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B  <_ +oo 
<->  ( B  < +oo  \/  B  = +oo ) ) )
7250, 71mpbid 210 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B  < +oo  \/  B  = +oo ) )
73 xrre2 11132 . . . . . . . . . . . 12  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\ +oo  e.  RR* )  /\  ( A  <  B  /\  B  < +oo ) )  ->  B  e.  RR )
7473expr 612 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\ +oo  e.  RR* )  /\  A  <  B )  ->  ( B  < +oo  ->  B  e.  RR ) )
7542, 74mp3anl3 1305 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B  < +oo  ->  B  e.  RR ) )
7675orim1d 830 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( ( B  < +oo  \/  B  = +oo )  ->  ( B  e.  RR  \/  B  = +oo )
) )
7772, 76mpd 15 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B  e.  RR  \/  B  = +oo ) )
78 icombl1 20888 . . . . . . . . 9  |-  ( B  e.  RR  ->  ( B [,) +oo )  e. 
dom  vol )
79 oveq1 6089 . . . . . . . . . . 11  |-  ( B  = +oo  ->  ( B [,) +oo )  =  ( +oo [,) +oo ) )
80 pnfge 11100 . . . . . . . . . . . . 13  |-  ( +oo  e.  RR*  -> +oo  <_ +oo )
8142, 80ax-mp 5 . . . . . . . . . . . 12  |- +oo  <_ +oo
82 ico0 11336 . . . . . . . . . . . . 13  |-  ( ( +oo  e.  RR*  /\ +oo  e.  RR* )  ->  (
( +oo [,) +oo )  =  (/)  <-> +oo  <_ +oo )
)
8342, 42, 82mp2an 667 . . . . . . . . . . . 12  |-  ( ( +oo [,) +oo )  =  (/)  <-> +oo  <_ +oo )
8481, 83mpbir 209 . . . . . . . . . . 11  |-  ( +oo [,) +oo )  =  (/)
8579, 84syl6eq 2483 . . . . . . . . . 10  |-  ( B  = +oo  ->  ( B [,) +oo )  =  (/) )
86 0mbl 20865 . . . . . . . . . 10  |-  (/)  e.  dom  vol
8785, 86syl6eqel 2523 . . . . . . . . 9  |-  ( B  = +oo  ->  ( B [,) +oo )  e. 
dom  vol )
8878, 87jaoi 379 . . . . . . . 8  |-  ( ( B  e.  RR  \/  B  = +oo )  ->  ( B [,) +oo )  e.  dom  vol )
8977, 88syl 16 . . . . . . 7  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( B [,) +oo )  e.  dom  vol )
90 difmbl 20868 . . . . . . 7  |-  ( ( RR  e.  dom  vol  /\  ( B [,) +oo )  e.  dom  vol )  ->  ( RR  \  ( B [,) +oo ) )  e.  dom  vol )
9169, 89, 90sylancr 658 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( RR  \ 
( B [,) +oo ) )  e.  dom  vol )
9268, 91eqeltrrd 2510 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( -oo (,) B )  e.  dom  vol )
93 oveq1 6089 . . . . . 6  |-  ( -oo  =  A  ->  ( -oo (,) B )  =  ( A (,) B ) )
9493eleq1d 2501 . . . . 5  |-  ( -oo  =  A  ->  ( ( -oo (,) B )  e.  dom  vol  <->  ( A (,) B )  e.  dom  vol ) )
9592, 94syl5ibcom 220 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( -oo  =  A  ->  ( A (,) B )  e.  dom  vol ) )
96 xrleloe 11111 . . . . . 6  |-  ( ( -oo  e.  RR*  /\  A  e.  RR* )  ->  ( -oo  <_  A  <->  ( -oo  <  A  \/ -oo  =  A ) ) )
9722, 44, 96sylancr 658 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( -oo  <_  A  <-> 
( -oo  <  A  \/ -oo  =  A ) ) )
9846, 97mpbid 210 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( -oo  <  A  \/ -oo  =  A ) )
9938, 95, 98mpjaod 381 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  A  <  B )  ->  ( A (,) B )  e.  dom  vol )
100 ioo0 11315 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A (,) B
)  =  (/)  <->  B  <_  A ) )
101 xrlenlt 9432 . . . . . . 7  |-  ( ( B  e.  RR*  /\  A  e.  RR* )  ->  ( B  <_  A  <->  -.  A  <  B ) )
102101ancoms 450 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( B  <_  A  <->  -.  A  <  B ) )
103100, 102bitrd 253 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A (,) B
)  =  (/)  <->  -.  A  <  B ) )
104103biimpar 482 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  -.  A  <  B
)  ->  ( A (,) B )  =  (/) )
105104, 86syl6eqel 2523 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  -.  A  <  B
)  ->  ( A (,) B )  e.  dom  vol )
10699, 105pm2.61dan 784 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A (,) B )  e. 
dom  vol )
107 ndmioo 11317 . . 3  |-  ( -.  ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A (,) B
)  =  (/) )
108107, 86syl6eqel 2523 . 2  |-  ( -.  ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A (,) B
)  e.  dom  vol )
109106, 108pm2.61i 164 1  |-  ( A (,) B )  e. 
dom  vol
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757    \ cdif 3315    u. cun 3316    i^i cin 3317    C_ wss 3318   (/)c0 3627   {csn 3867   class class class wbr 4282   dom cdm 4829   ` cfv 5408  (class class class)co 6082   RRcr 9271   0cc0 9272   +oocpnf 9405   -oocmnf 9406   RR*cxr 9407    < clt 9408    <_ cle 9409   (,)cioo 11290   [,)cico 11292   [,]cicc 11293   vol*covol 20790   volcvol 20791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-se 4669  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6311  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-er 7091  df-map 7206  df-pm 7207  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-sup 7681  df-oi 7714  df-card 8099  df-cda 8327  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-3 10371  df-n0 10570  df-z 10637  df-uz 10852  df-q 10944  df-rp 10982  df-xadd 11080  df-ioo 11294  df-ico 11296  df-icc 11297  df-fz 11427  df-fzo 11535  df-fl 11628  df-seq 11793  df-exp 11852  df-hash 12090  df-cj 12574  df-re 12575  df-im 12576  df-sqr 12710  df-abs 12711  df-clim 12952  df-rlim 12953  df-sum 13150  df-xmet 17656  df-met 17657  df-ovol 20792  df-vol 20793
This theorem is referenced by:  iccmbl  20891  ovolioo  20893  ioovolcl  20894  uniioovol  20903  uniioombllem4  20910  uniioombllem5  20911  opnmblALT  20927  mbfid  20958  ditgcl  21177  ditgswap  21178  ditgsplitlem  21179  ftc1lem1  21351  ftc1lem2  21352  ftc1a  21353  ftc1lem4  21355  ftc2  21360  ftc2ditglem  21361  itgsubstlem  21364  itg2gt0cn  28293  ftc1cnnclem  28311  ftc1anclem7  28319  ftc1anclem8  28320  ftc1anc  28321  ftc2nc  28322  areacirc  28335  iocmbl  29435  cnioobibld  29436  itgpowd  29437  lhe4.4ex1a  29450  volioo  29637  itgsin0pilem1  29638  iblioosinexp  29641  itgsinexplem1  29642  itgsinexp  29643  wallispilem2  29709
  Copyright terms: Public domain W3C validator