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 φ A
ovolicc.2 φ B
ovolicc.3 φ A B
ovolicc1.4 G = n if n = 1 A B 0 0
Assertion ovolicc1 φ vol * A B B A

Proof

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