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 )