Metamath Proof Explorer

Theorem ovolicc1

Description: The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc1.4 
|- G = ( n e. NN |-> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) )
Assertion ovolicc1 
|- ( ph -> ( vol* ` ( A [,] B ) ) <_ ( B - A ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc1.4 
 |-  G = ( n e. NN |-> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) )
5 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
6 1 2 5 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
7 ovolcl 
 |-  ( ( A [,] B ) C_ RR -> ( vol* ` ( A [,] B ) ) e. RR* )
8 6 7 syl 
 |-  ( ph -> ( vol* ` ( A [,] B ) ) e. RR* )
9 df-br 
 |-  ( A <_ B <-> <. A , B >. e. <_ )
10 3 9 sylib 
 |-  ( ph -> <. A , B >. e. <_ )
11 1 2 opelxpd 
 |-  ( ph -> <. A , B >. e. ( RR X. RR ) )
12 10 11 elind 
 |-  ( ph -> <. A , B >. e. ( <_ i^i ( RR X. RR ) ) )
13 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> <. A , B >. e. ( <_ i^i ( RR X. RR ) ) )
14 0le0 
 |-  0 <_ 0
15 df-br 
 |-  ( 0 <_ 0 <-> <. 0 , 0 >. e. <_ )
16 14 15 mpbi 
 |-  <. 0 , 0 >. e. <_
17 0re 
 |-  0 e. RR
18 opelxpi 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> <. 0 , 0 >. e. ( RR X. RR ) )
19 17 17 18 mp2an 
 |-  <. 0 , 0 >. e. ( RR X. RR )
20 16 19 elini 
 |-  <. 0 , 0 >. e. ( <_ i^i ( RR X. RR ) )
21 ifcl 
 |-  ( ( <. A , B >. e. ( <_ i^i ( RR X. RR ) ) /\ <. 0 , 0 >. e. ( <_ i^i ( RR X. RR ) ) ) -> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) e. ( <_ i^i ( RR X. RR ) ) )
22 13 20 21 sylancl 
 |-  ( ( ph /\ n e. NN ) -> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) e. ( <_ i^i ( RR X. RR ) ) )
23 22 4 fmptd 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
24 eqid 
 |-  ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
25 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. G ) ) = seq 1 ( + , ( ( abs o. - ) o. G ) )
26 24 25 ovolsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. G ) ) : NN --> ( 0 [,) +oo ) )
27 23 26 syl 
 |-  ( ph -> seq 1 ( + , ( ( abs o. - ) o. G ) ) : NN --> ( 0 [,) +oo ) )
28 27 frnd 
 |-  ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. G ) ) C_ ( 0 [,) +oo ) )
29 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
30 28 29 sstrdi 
 |-  ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. G ) ) C_ RR* )
31 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) e. RR* )
32 30 31 syl 
 |-  ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) e. RR* )
33 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
34 33 rexrd 
 |-  ( ph -> ( B - A ) e. RR* )
35 1nn 
 |-  1 e. NN
36 35 a1i 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> 1 e. NN )
37 op1stg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 1st ` <. A , B >. ) = A )
38 1 2 37 syl2anc 
 |-  ( ph -> ( 1st ` <. A , B >. ) = A )
39 38 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( 1st ` <. A , B >. ) = A )
40 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
41 1 2 40 syl2anc 
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
42 41 biimpa 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
43 42 simp2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
44 39 43 eqbrtrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( 1st ` <. A , B >. ) <_ x )
45 42 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
46 op2ndg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2nd ` <. A , B >. ) = B )
47 1 2 46 syl2anc 
 |-  ( ph -> ( 2nd ` <. A , B >. ) = B )
48 47 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( 2nd ` <. A , B >. ) = B )
49 45 48 breqtrrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ ( 2nd ` <. A , B >. ) )
50 fveq2 
 |-  ( n = 1 -> ( G ` n ) = ( G ` 1 ) )
51 iftrue 
 |-  ( n = 1 -> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) = <. A , B >. )
52 opex 
 |-  <. A , B >. e. _V
53 51 4 52 fvmpt 
 |-  ( 1 e. NN -> ( G ` 1 ) = <. A , B >. )
54 35 53 ax-mp 
 |-  ( G ` 1 ) = <. A , B >.
55 50 54 eqtrdi 
 |-  ( n = 1 -> ( G ` n ) = <. A , B >. )
56 55 fveq2d 
 |-  ( n = 1 -> ( 1st ` ( G ` n ) ) = ( 1st ` <. A , B >. ) )
57 56 breq1d 
 |-  ( n = 1 -> ( ( 1st ` ( G ` n ) ) <_ x <-> ( 1st ` <. A , B >. ) <_ x ) )
58 55 fveq2d 
 |-  ( n = 1 -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. A , B >. ) )
59 58 breq2d 
 |-  ( n = 1 -> ( x <_ ( 2nd ` ( G ` n ) ) <-> x <_ ( 2nd ` <. A , B >. ) ) )
60 57 59 anbi12d 
 |-  ( n = 1 -> ( ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) <-> ( ( 1st ` <. A , B >. ) <_ x /\ x <_ ( 2nd ` <. A , B >. ) ) ) )
61 60 rspcev 
 |-  ( ( 1 e. NN /\ ( ( 1st ` <. A , B >. ) <_ x /\ x <_ ( 2nd ` <. A , B >. ) ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) )
62 36 44 49 61 syl12anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) )
63 62 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) )
64 ovolficc 
 |-  ( ( ( A [,] B ) C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( A [,] B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( A [,] B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
65 6 23 64 syl2anc 
 |-  ( ph -> ( ( A [,] B ) C_ U. ran ( [,] o. G ) <-> A. x e. ( A [,] B ) E. n e. NN ( ( 1st ` ( G ` n ) ) <_ x /\ x <_ ( 2nd ` ( G ` n ) ) ) ) )
66 63 65 mpbird 
 |-  ( ph -> ( A [,] B ) C_ U. ran ( [,] o. G ) )
67 25 ovollb2 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( A [,] B ) C_ U. ran ( [,] o. G ) ) -> ( vol* ` ( A [,] B ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) )
68 23 66 67 syl2anc 
 |-  ( ph -> ( vol* ` ( A [,] B ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) )
69 addrid 
 |-  ( k e. CC -> ( k + 0 ) = k )
70 69 adantl 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. CC ) -> ( k + 0 ) = k )
71 nnuz 
 |-  NN = ( ZZ>= ` 1 )
72 35 71 eleqtri 
 |-  1 e. ( ZZ>= ` 1 )
73 72 a1i 
 |-  ( ( ph /\ x e. NN ) -> 1 e. ( ZZ>= ` 1 ) )
74 simpr 
 |-  ( ( ph /\ x e. NN ) -> x e. NN )
75 74 71 eleqtrdi 
 |-  ( ( ph /\ x e. NN ) -> x e. ( ZZ>= ` 1 ) )
76 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
77 27 adantr 
 |-  ( ( ph /\ x e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. G ) ) : NN --> ( 0 [,) +oo ) )
78 ffvelcdm 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) : NN --> ( 0 [,) +oo ) /\ 1 e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) e. ( 0 [,) +oo ) )
79 77 35 78 sylancl 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) e. ( 0 [,) +oo ) )
80 76 79 sselid 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) e. RR )
81 80 recnd 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) e. CC )
82 23 ad2antrr 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
83 elfzuz 
 |-  ( k e. ( ( 1 + 1 ) ... x ) -> k e. ( ZZ>= ` ( 1 + 1 ) ) )
84 83 adantl 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> k e. ( ZZ>= ` ( 1 + 1 ) ) )
85 df-2 
 |-  2 = ( 1 + 1 )
86 85 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
87 84 86 eleqtrrdi 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> k e. ( ZZ>= ` 2 ) )
88 eluz2nn 
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. NN )
89 87 88 syl 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> k e. NN )
90 24 ovolfsval 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` k ) = ( ( 2nd ` ( G ` k ) ) - ( 1st ` ( G ` k ) ) ) )
91 82 89 90 syl2anc 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( ( ( abs o. - ) o. G ) ` k ) = ( ( 2nd ` ( G ` k ) ) - ( 1st ` ( G ` k ) ) ) )
92 eqeq1 
 |-  ( n = k -> ( n = 1 <-> k = 1 ) )
93 92 ifbid 
 |-  ( n = k -> if ( n = 1 , <. A , B >. , <. 0 , 0 >. ) = if ( k = 1 , <. A , B >. , <. 0 , 0 >. ) )
94 opex 
 |-  <. 0 , 0 >. e. _V
95 52 94 ifex 
 |-  if ( k = 1 , <. A , B >. , <. 0 , 0 >. ) e. _V
96 93 4 95 fvmpt 
 |-  ( k e. NN -> ( G ` k ) = if ( k = 1 , <. A , B >. , <. 0 , 0 >. ) )
97 89 96 syl 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( G ` k ) = if ( k = 1 , <. A , B >. , <. 0 , 0 >. ) )
98 eluz2b3 
 |-  ( k e. ( ZZ>= ` 2 ) <-> ( k e. NN /\ k =/= 1 ) )
99 98 simprbi 
 |-  ( k e. ( ZZ>= ` 2 ) -> k =/= 1 )
100 87 99 syl 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> k =/= 1 )
101 100 neneqd 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> -. k = 1 )
102 101 iffalsed 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> if ( k = 1 , <. A , B >. , <. 0 , 0 >. ) = <. 0 , 0 >. )
103 97 102 eqtrd 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( G ` k ) = <. 0 , 0 >. )
104 103 fveq2d 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( 2nd ` ( G ` k ) ) = ( 2nd ` <. 0 , 0 >. ) )
105 c0ex 
 |-  0 e. _V
106 105 105 op2nd 
 |-  ( 2nd ` <. 0 , 0 >. ) = 0
107 104 106 eqtrdi 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( 2nd ` ( G ` k ) ) = 0 )
108 103 fveq2d 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( 1st ` ( G ` k ) ) = ( 1st ` <. 0 , 0 >. ) )
109 105 105 op1st 
 |-  ( 1st ` <. 0 , 0 >. ) = 0
110 108 109 eqtrdi 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( 1st ` ( G ` k ) ) = 0 )
111 107 110 oveq12d 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( ( 2nd ` ( G ` k ) ) - ( 1st ` ( G ` k ) ) ) = ( 0 - 0 ) )
112 0m0e0 
 |-  ( 0 - 0 ) = 0
113 111 112 eqtrdi 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( ( 2nd ` ( G ` k ) ) - ( 1st ` ( G ` k ) ) ) = 0 )
114 91 113 eqtrd 
 |-  ( ( ( ph /\ x e. NN ) /\ k e. ( ( 1 + 1 ) ... x ) ) -> ( ( ( abs o. - ) o. G ) ` k ) = 0 )
115 70 73 75 81 114 seqid2 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) )
116 1z 
 |-  1 e. ZZ
117 23 adantr 
 |-  ( ( ph /\ x e. NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
118 24 ovolfsval 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
119 117 35 118 sylancl 
 |-  ( ( ph /\ x e. NN ) -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
120 54 fveq2i 
 |-  ( 2nd ` ( G ` 1 ) ) = ( 2nd ` <. A , B >. )
121 47 adantr 
 |-  ( ( ph /\ x e. NN ) -> ( 2nd ` <. A , B >. ) = B )
122 120 121 eqtrid 
 |-  ( ( ph /\ x e. NN ) -> ( 2nd ` ( G ` 1 ) ) = B )
123 54 fveq2i 
 |-  ( 1st ` ( G ` 1 ) ) = ( 1st ` <. A , B >. )
124 38 adantr 
 |-  ( ( ph /\ x e. NN ) -> ( 1st ` <. A , B >. ) = A )
125 123 124 eqtrid 
 |-  ( ( ph /\ x e. NN ) -> ( 1st ` ( G ` 1 ) ) = A )
126 122 125 oveq12d 
 |-  ( ( ph /\ x e. NN ) -> ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) = ( B - A ) )
127 119 126 eqtrd 
 |-  ( ( ph /\ x e. NN ) -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( B - A ) )
128 116 127 seq1i 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) = ( B - A ) )
129 115 128 eqtr3d 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) = ( B - A ) )
130 33 leidd 
 |-  ( ph -> ( B - A ) <_ ( B - A ) )
131 130 adantr 
 |-  ( ( ph /\ x e. NN ) -> ( B - A ) <_ ( B - A ) )
132 129 131 eqbrtrd 
 |-  ( ( ph /\ x e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) <_ ( B - A ) )
133 132 ralrimiva 
 |-  ( ph -> A. x e. NN ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) <_ ( B - A ) )
134 27 ffnd 
 |-  ( ph -> seq 1 ( + , ( ( abs o. - ) o. G ) ) Fn NN )
135 breq1 
 |-  ( z = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) -> ( z <_ ( B - A ) <-> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) <_ ( B - A ) ) )
136 135 ralrn 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. G ) ) Fn NN -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. G ) ) z <_ ( B - A ) <-> A. x e. NN ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) <_ ( B - A ) ) )
137 134 136 syl 
 |-  ( ph -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. G ) ) z <_ ( B - A ) <-> A. x e. NN ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` x ) <_ ( B - A ) ) )
138 133 137 mpbird 
 |-  ( ph -> A. z e. ran seq 1 ( + , ( ( abs o. - ) o. G ) ) z <_ ( B - A ) )
139 supxrleub 
 |-  ( ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) C_ RR* /\ ( B - A ) e. RR* ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) <_ ( B - A ) <-> A. z e. ran seq 1 ( + , ( ( abs o. - ) o. G ) ) z <_ ( B - A ) ) )
140 30 34 139 syl2anc 
 |-  ( ph -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) <_ ( B - A ) <-> A. z e. ran seq 1 ( + , ( ( abs o. - ) o. G ) ) z <_ ( B - A ) ) )
141 138 140 mpbird 
 |-  ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) <_ ( B - A ) )
142 8 32 34 68 141 xrletrd 
 |-  ( ph -> ( vol* ` ( A [,] B ) ) <_ ( B - A ) )