Description: The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ovolicopnf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfxr | |
|
2 | icossre | |
|
3 | 1 2 | mpan2 | |
4 | 3 | adantr | |
5 | ovolge0 | |
|
6 | 4 5 | syl | |
7 | mnflt0 | |
|
8 | mnfxr | |
|
9 | 0xr | |
|
10 | ovolcl | |
|
11 | 3 10 | syl | |
12 | 11 | adantr | |
13 | xrltletr | |
|
14 | 8 9 12 13 | mp3an12i | |
15 | 7 14 | mpani | |
16 | 6 15 | mpd | |
17 | simpr | |
|
18 | xrrebnd | |
|
19 | 12 18 | syl | |
20 | 16 17 19 | mpbir2and | |
21 | 20 | ltp1d | |
22 | peano2re | |
|
23 | 20 22 | syl | |
24 | simpl | |
|
25 | 23 24 | readdcld | |
26 | 0red | |
|
27 | 20 | lep1d | |
28 | 26 20 23 6 27 | letrd | |
29 | 24 23 | addge02d | |
30 | 28 29 | mpbid | |
31 | ovolicc | |
|
32 | 24 25 30 31 | syl3anc | |
33 | 23 | recnd | |
34 | 24 | recnd | |
35 | 33 34 | pncand | |
36 | 32 35 | eqtrd | |
37 | elicc2 | |
|
38 | 24 25 37 | syl2anc | |
39 | 38 | biimpa | |
40 | 39 | simp1d | |
41 | 39 | simp2d | |
42 | elicopnf | |
|
43 | 42 | ad2antrr | |
44 | 40 41 43 | mpbir2and | |
45 | 44 | ex | |
46 | 45 | ssrdv | |
47 | ovolss | |
|
48 | 46 4 47 | syl2anc | |
49 | 36 48 | eqbrtrrd | |
50 | 23 20 49 | lensymd | |
51 | 21 50 | pm2.65da | |
52 | nltpnft | |
|
53 | 11 52 | syl | |
54 | 51 53 | mpbird | |