Metamath Proof Explorer

Theorem ovolicopnf

Description: The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolicopnf 
|- ( A e. RR -> ( vol* ` ( A [,) +oo ) ) = +oo )

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 icossre 
 |-  ( ( A e. RR /\ +oo e. RR* ) -> ( A [,) +oo ) C_ RR )
3 1 2 mpan2 
 |-  ( A e. RR -> ( A [,) +oo ) C_ RR )
4 3 adantr 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( A [,) +oo ) C_ RR )
5 ovolge0 
 |-  ( ( A [,) +oo ) C_ RR -> 0 <_ ( vol* ` ( A [,) +oo ) ) )
6 4 5 syl 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 <_ ( vol* ` ( A [,) +oo ) ) )
7 mnflt0 
 |-  -oo < 0
8 mnfxr 
 |-  -oo e. RR*
9 0xr 
 |-  0 e. RR*
10 ovolcl 
 |-  ( ( A [,) +oo ) C_ RR -> ( vol* ` ( A [,) +oo ) ) e. RR* )
11 3 10 syl 
 |-  ( A e. RR -> ( vol* ` ( A [,) +oo ) ) e. RR* )
12 11 adantr 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) e. RR* )
13 xrltletr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ ( vol* ` ( A [,) +oo ) ) e. RR* ) -> ( ( -oo < 0 /\ 0 <_ ( vol* ` ( A [,) +oo ) ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) )
14 8 9 12 13 mp3an12i 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( -oo < 0 /\ 0 <_ ( vol* ` ( A [,) +oo ) ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) )
15 7 14 mpani 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( 0 <_ ( vol* ` ( A [,) +oo ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) )
16 6 15 mpd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> -oo < ( vol* ` ( A [,) +oo ) ) )
17 simpr 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) < +oo )
18 xrrebnd 
 |-  ( ( vol* ` ( A [,) +oo ) ) e. RR* -> ( ( vol* ` ( A [,) +oo ) ) e. RR <-> ( -oo < ( vol* ` ( A [,) +oo ) ) /\ ( vol* ` ( A [,) +oo ) ) < +oo ) ) )
19 12 18 syl 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) e. RR <-> ( -oo < ( vol* ` ( A [,) +oo ) ) /\ ( vol* ` ( A [,) +oo ) ) < +oo ) ) )
20 16 17 19 mpbir2and 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) e. RR )
21 20 ltp1d 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) < ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
22 peano2re 
 |-  ( ( vol* ` ( A [,) +oo ) ) e. RR -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. RR )
23 20 22 syl 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. RR )
24 simpl 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A e. RR )
25 23 24 readdcld 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR )
26 0red 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 e. RR )
27 20 lep1d 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
28 26 20 23 6 27 letrd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
29 24 23 addge02d 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( 0 <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) <-> A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) )
30 28 29 mpbid 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) )
31 ovolicc 
 |-  ( ( A e. RR /\ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR /\ A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) )
32 24 25 30 31 syl3anc 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) )
33 23 recnd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. CC )
34 24 recnd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A e. CC )
35 33 34 pncand 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) = ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
36 32 35 eqtrd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
37 elicc2 
 |-  ( ( A e. RR /\ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) <-> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) )
38 24 25 37 syl2anc 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) <-> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) )
39 38 biimpa 
 |-  ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) )
40 39 simp1d 
 |-  ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> x e. RR )
41 39 simp2d 
 |-  ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> A <_ x )
42 elicopnf 
 |-  ( A e. RR -> ( x e. ( A [,) +oo ) <-> ( x e. RR /\ A <_ x ) ) )
43 42 ad2antrr 
 |-  ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> ( x e. ( A [,) +oo ) <-> ( x e. RR /\ A <_ x ) ) )
44 40 41 43 mpbir2and 
 |-  ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> x e. ( A [,) +oo ) )
45 44 ex 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) -> x e. ( A [,) +oo ) ) )
46 45 ssrdv 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) C_ ( A [,) +oo ) )
47 ovolss 
 |-  ( ( ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) C_ ( A [,) +oo ) /\ ( A [,) +oo ) C_ RR ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) <_ ( vol* ` ( A [,) +oo ) ) )
48 46 4 47 syl2anc 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) <_ ( vol* ` ( A [,) +oo ) ) )
49 36 48 eqbrtrrd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) <_ ( vol* ` ( A [,) +oo ) ) )
50 23 20 49 lensymd 
 |-  ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> -. ( vol* ` ( A [,) +oo ) ) < ( ( vol* ` ( A [,) +oo ) ) + 1 ) )
51 21 50 pm2.65da 
 |-  ( A e. RR -> -. ( vol* ` ( A [,) +oo ) ) < +oo )
52 nltpnft 
 |-  ( ( vol* ` ( A [,) +oo ) ) e. RR* -> ( ( vol* ` ( A [,) +oo ) ) = +oo <-> -. ( vol* ` ( A [,) +oo ) ) < +oo ) )
53 11 52 syl 
 |-  ( A e. RR -> ( ( vol* ` ( A [,) +oo ) ) = +oo <-> -. ( vol* ` ( A [,) +oo ) ) < +oo ) )
54 51 53 mpbird 
 |-  ( A e. RR -> ( vol* ` ( A [,) +oo ) ) = +oo )