Metamath Proof Explorer


Theorem ovolicopnf

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

Ref Expression
Assertion ovolicopnf Avol*A+∞=+∞

Proof

Step Hyp Ref Expression
1 pnfxr +∞*
2 icossre A+∞*A+∞
3 1 2 mpan2 AA+∞
4 3 adantr Avol*A+∞<+∞A+∞
5 ovolge0 A+∞0vol*A+∞
6 4 5 syl Avol*A+∞<+∞0vol*A+∞
7 mnflt0 −∞<0
8 mnfxr −∞*
9 0xr 0*
10 ovolcl A+∞vol*A+∞*
11 3 10 syl Avol*A+∞*
12 11 adantr Avol*A+∞<+∞vol*A+∞*
13 xrltletr −∞*0*vol*A+∞*−∞<00vol*A+∞−∞<vol*A+∞
14 8 9 12 13 mp3an12i Avol*A+∞<+∞−∞<00vol*A+∞−∞<vol*A+∞
15 7 14 mpani Avol*A+∞<+∞0vol*A+∞−∞<vol*A+∞
16 6 15 mpd Avol*A+∞<+∞−∞<vol*A+∞
17 simpr Avol*A+∞<+∞vol*A+∞<+∞
18 xrrebnd vol*A+∞*vol*A+∞−∞<vol*A+∞vol*A+∞<+∞
19 12 18 syl Avol*A+∞<+∞vol*A+∞−∞<vol*A+∞vol*A+∞<+∞
20 16 17 19 mpbir2and Avol*A+∞<+∞vol*A+∞
21 20 ltp1d Avol*A+∞<+∞vol*A+∞<vol*A+∞+1
22 peano2re vol*A+∞vol*A+∞+1
23 20 22 syl Avol*A+∞<+∞vol*A+∞+1
24 simpl Avol*A+∞<+∞A
25 23 24 readdcld Avol*A+∞<+∞vol*A+∞+1+A
26 0red Avol*A+∞<+∞0
27 20 lep1d Avol*A+∞<+∞vol*A+∞vol*A+∞+1
28 26 20 23 6 27 letrd Avol*A+∞<+∞0vol*A+∞+1
29 24 23 addge02d Avol*A+∞<+∞0vol*A+∞+1Avol*A+∞+1+A
30 28 29 mpbid Avol*A+∞<+∞Avol*A+∞+1+A
31 ovolicc Avol*A+∞+1+AAvol*A+∞+1+Avol*Avol*A+∞+1+A=vol*A+∞+1+A-A
32 24 25 30 31 syl3anc Avol*A+∞<+∞vol*Avol*A+∞+1+A=vol*A+∞+1+A-A
33 23 recnd Avol*A+∞<+∞vol*A+∞+1
34 24 recnd Avol*A+∞<+∞A
35 33 34 pncand Avol*A+∞<+∞vol*A+∞+1+A-A=vol*A+∞+1
36 32 35 eqtrd Avol*A+∞<+∞vol*Avol*A+∞+1+A=vol*A+∞+1
37 elicc2 Avol*A+∞+1+AxAvol*A+∞+1+AxAxxvol*A+∞+1+A
38 24 25 37 syl2anc Avol*A+∞<+∞xAvol*A+∞+1+AxAxxvol*A+∞+1+A
39 38 biimpa Avol*A+∞<+∞xAvol*A+∞+1+AxAxxvol*A+∞+1+A
40 39 simp1d Avol*A+∞<+∞xAvol*A+∞+1+Ax
41 39 simp2d Avol*A+∞<+∞xAvol*A+∞+1+AAx
42 elicopnf AxA+∞xAx
43 42 ad2antrr Avol*A+∞<+∞xAvol*A+∞+1+AxA+∞xAx
44 40 41 43 mpbir2and Avol*A+∞<+∞xAvol*A+∞+1+AxA+∞
45 44 ex Avol*A+∞<+∞xAvol*A+∞+1+AxA+∞
46 45 ssrdv Avol*A+∞<+∞Avol*A+∞+1+AA+∞
47 ovolss Avol*A+∞+1+AA+∞A+∞vol*Avol*A+∞+1+Avol*A+∞
48 46 4 47 syl2anc Avol*A+∞<+∞vol*Avol*A+∞+1+Avol*A+∞
49 36 48 eqbrtrrd Avol*A+∞<+∞vol*A+∞+1vol*A+∞
50 23 20 49 lensymd Avol*A+∞<+∞¬vol*A+∞<vol*A+∞+1
51 21 50 pm2.65da A¬vol*A+∞<+∞
52 nltpnft vol*A+∞*vol*A+∞=+∞¬vol*A+∞<+∞
53 11 52 syl Avol*A+∞=+∞¬vol*A+∞<+∞
54 51 53 mpbird Avol*A+∞=+∞