Metamath Proof Explorer

Theorem ioorcl2

Description: An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion ioorcl2 
|- ( ( ( A (,) B ) =/= (/) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A e. RR /\ B e. RR ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( ( A (,) B ) =/= (/) <-> E. z z e. ( A (,) B ) )
2 elioore 
 |-  ( z e. ( A (,) B ) -> z e. RR )
3 2 adantr 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z e. RR )
4 peano2re 
 |-  ( ( vol* ` ( A (,) B ) ) e. RR -> ( ( vol* ` ( A (,) B ) ) + 1 ) e. RR )
5 4 adantl 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( vol* ` ( A (,) B ) ) + 1 ) e. RR )
6 3 5 resubcld 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR )
7 6 rexrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR* )
8 eliooxr 
 |-  ( z e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* ) )
9 8 adantr 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A e. RR* /\ B e. RR* ) )
10 9 simpld 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> A e. RR* )
11 3 rexrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z e. RR* )
12 ltp1 
 |-  ( ( vol* ` ( A (,) B ) ) e. RR -> ( vol* ` ( A (,) B ) ) < ( ( vol* ` ( A (,) B ) ) + 1 ) )
13 12 adantl 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( A (,) B ) ) < ( ( vol* ` ( A (,) B ) ) + 1 ) )
14 0red 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> 0 e. RR )
15 simpr 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( A (,) B ) ) e. RR )
16 ioossre 
 |-  ( A (,) B ) C_ RR
17 ovolge0 
 |-  ( ( A (,) B ) C_ RR -> 0 <_ ( vol* ` ( A (,) B ) ) )
18 16 17 mp1i 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> 0 <_ ( vol* ` ( A (,) B ) ) )
19 lep1 
 |-  ( ( vol* ` ( A (,) B ) ) e. RR -> ( vol* ` ( A (,) B ) ) <_ ( ( vol* ` ( A (,) B ) ) + 1 ) )
20 19 adantl 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( A (,) B ) ) <_ ( ( vol* ` ( A (,) B ) ) + 1 ) )
21 14 15 5 18 20 letrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> 0 <_ ( ( vol* ` ( A (,) B ) ) + 1 ) )
22 3 5 subge02d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( 0 <_ ( ( vol* ` ( A (,) B ) ) + 1 ) <-> ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ z ) )
23 21 22 mpbid 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ z )
24 ovolioo 
 |-  ( ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR /\ z e. RR /\ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ z ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) = ( z - ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) )
25 6 3 23 24 syl3anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) = ( z - ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) )
26 3 recnd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z e. CC )
27 5 recnd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( vol* ` ( A (,) B ) ) + 1 ) e. CC )
28 26 27 nncand 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z - ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
29 25 28 eqtrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
30 29 adantr 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
31 iooss1 
 |-  ( ( A e. RR* /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) C_ ( A (,) z ) )
32 10 31 sylan 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) C_ ( A (,) z ) )
33 9 simprd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> B e. RR* )
34 eliooord 
 |-  ( z e. ( A (,) B ) -> ( A < z /\ z < B ) )
35 34 adantr 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A < z /\ z < B ) )
36 35 simprd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z < B )
37 11 33 36 xrltled 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z <_ B )
38 iooss2 
 |-  ( ( B e. RR* /\ z <_ B ) -> ( A (,) z ) C_ ( A (,) B ) )
39 33 37 38 syl2anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A (,) z ) C_ ( A (,) B ) )
40 39 adantr 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( A (,) z ) C_ ( A (,) B ) )
41 32 40 sstrd 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) C_ ( A (,) B ) )
42 ovolss 
 |-  ( ( ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) C_ ( A (,) B ) /\ ( A (,) B ) C_ RR ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) <_ ( vol* ` ( A (,) B ) ) )
43 41 16 42 sylancl 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( vol* ` ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) (,) z ) ) <_ ( vol* ` ( A (,) B ) ) )
44 30 43 eqbrtrrd 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( ( vol* ` ( A (,) B ) ) + 1 ) <_ ( vol* ` ( A (,) B ) ) )
45 44 ex 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) -> ( ( vol* ` ( A (,) B ) ) + 1 ) <_ ( vol* ` ( A (,) B ) ) ) )
46 10 7 xrlenltd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A <_ ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) <-> -. ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) < A ) )
47 5 15 lenltd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( ( vol* ` ( A (,) B ) ) + 1 ) <_ ( vol* ` ( A (,) B ) ) <-> -. ( vol* ` ( A (,) B ) ) < ( ( vol* ` ( A (,) B ) ) + 1 ) ) )
48 45 46 47 3imtr3d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( -. ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) < A -> -. ( vol* ` ( A (,) B ) ) < ( ( vol* ` ( A (,) B ) ) + 1 ) ) )
49 13 48 mt4d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) < A )
50 35 simpld 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> A < z )
51 xrre2 
 |-  ( ( ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( ( z - ( ( vol* ` ( A (,) B ) ) + 1 ) ) < A /\ A < z ) ) -> A e. RR )
52 7 10 11 49 50 51 syl32anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> A e. RR )
53 3 5 readdcld 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR )
54 53 rexrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR* )
55 3 5 addge01d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( 0 <_ ( ( vol* ` ( A (,) B ) ) + 1 ) <-> z <_ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) )
56 21 55 mpbid 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> z <_ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) )
57 ovolioo 
 |-  ( ( z e. RR /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR /\ z <_ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) = ( ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) - z ) )
58 3 53 56 57 syl3anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) = ( ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) - z ) )
59 26 27 pncan2d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) - z ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
60 58 59 eqtrd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
61 60 adantr 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) = ( ( vol* ` ( A (,) B ) ) + 1 ) )
62 iooss2 
 |-  ( ( B e. RR* /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) C_ ( z (,) B ) )
63 33 62 sylan 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) C_ ( z (,) B ) )
64 10 11 50 xrltled 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> A <_ z )
65 iooss1 
 |-  ( ( A e. RR* /\ A <_ z ) -> ( z (,) B ) C_ ( A (,) B ) )
66 10 64 65 syl2anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( z (,) B ) C_ ( A (,) B ) )
67 66 adantr 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( z (,) B ) C_ ( A (,) B ) )
68 63 67 sstrd 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) C_ ( A (,) B ) )
69 ovolss 
 |-  ( ( ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) C_ ( A (,) B ) /\ ( A (,) B ) C_ RR ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) <_ ( vol* ` ( A (,) B ) ) )
70 68 16 69 sylancl 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( vol* ` ( z (,) ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) <_ ( vol* ` ( A (,) B ) ) )
71 61 70 eqbrtrrd 
 |-  ( ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B ) -> ( ( vol* ` ( A (,) B ) ) + 1 ) <_ ( vol* ` ( A (,) B ) ) )
72 71 ex 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B -> ( ( vol* ` ( A (,) B ) ) + 1 ) <_ ( vol* ` ( A (,) B ) ) ) )
73 54 33 xrlenltd 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) <_ B <-> -. B < ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) )
74 72 73 47 3imtr3d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( -. B < ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) -> -. ( vol* ` ( A (,) B ) ) < ( ( vol* ` ( A (,) B ) ) + 1 ) ) )
75 13 74 mt4d 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> B < ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) )
76 xrre2 
 |-  ( ( ( z e. RR* /\ B e. RR* /\ ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) e. RR* ) /\ ( z < B /\ B < ( z + ( ( vol* ` ( A (,) B ) ) + 1 ) ) ) ) -> B e. RR )
77 11 33 54 36 75 76 syl32anc 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> B e. RR )
78 52 77 jca 
 |-  ( ( z e. ( A (,) B ) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A e. RR /\ B e. RR ) )
79 78 ex 
 |-  ( z e. ( A (,) B ) -> ( ( vol* ` ( A (,) B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) )
80 79 exlimiv 
 |-  ( E. z z e. ( A (,) B ) -> ( ( vol* ` ( A (,) B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) )
81 1 80 sylbi 
 |-  ( ( A (,) B ) =/= (/) -> ( ( vol* ` ( A (,) B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) )
82 81 imp 
 |-  ( ( ( A (,) B ) =/= (/) /\ ( vol* ` ( A (,) B ) ) e. RR ) -> ( A e. RR /\ B e. RR ) )