Metamath Proof Explorer


Theorem ovolgelb

Description: The outer volume is the greatest lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovolgelb.1 S = seq 1 + abs g
Assertion ovolgelb A vol * A B + g 2 A ran . g sup ran S * < vol * A + B

Proof

Step Hyp Ref Expression
1 ovolgelb.1 S = seq 1 + abs g
2 simp2 A vol * A B + vol * A
3 simp3 A vol * A B + B +
4 2 3 ltaddrpd A vol * A B + vol * A < vol * A + B
5 3 rpred A vol * A B + B
6 2 5 readdcld A vol * A B + vol * A + B
7 2 6 ltnled A vol * A B + vol * A < vol * A + B ¬ vol * A + B vol * A
8 4 7 mpbid A vol * A B + ¬ vol * A + B vol * A
9 eqid y * | g 2 A ran . g y = sup ran seq 1 + abs g * < = y * | g 2 A ran . g y = sup ran seq 1 + abs g * <
10 9 ovolval A vol * A = sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * <
11 10 3ad2ant1 A vol * A B + vol * A = sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * <
12 11 breq2d A vol * A B + vol * A + B vol * A vol * A + B sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * <
13 ssrab2 y * | g 2 A ran . g y = sup ran seq 1 + abs g * < *
14 6 rexrd A vol * A B + vol * A + B *
15 infxrgelb y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * vol * A + B * vol * A + B sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * < x y * | g 2 A ran . g y = sup ran seq 1 + abs g * < vol * A + B x
16 13 14 15 sylancr A vol * A B + vol * A + B sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * < x y * | g 2 A ran . g y = sup ran seq 1 + abs g * < vol * A + B x
17 eqeq1 y = x y = sup ran seq 1 + abs g * < x = sup ran seq 1 + abs g * <
18 1 rneqi ran S = ran seq 1 + abs g
19 18 supeq1i sup ran S * < = sup ran seq 1 + abs g * <
20 19 eqeq2i x = sup ran S * < x = sup ran seq 1 + abs g * <
21 17 20 bitr4di y = x y = sup ran seq 1 + abs g * < x = sup ran S * <
22 21 anbi2d y = x A ran . g y = sup ran seq 1 + abs g * < A ran . g x = sup ran S * <
23 22 rexbidv y = x g 2 A ran . g y = sup ran seq 1 + abs g * < g 2 A ran . g x = sup ran S * <
24 23 ralrab x y * | g 2 A ran . g y = sup ran seq 1 + abs g * < vol * A + B x x * g 2 A ran . g x = sup ran S * < vol * A + B x
25 ralcom x * g 2 A ran . g x = sup ran S * < vol * A + B x g 2 x * A ran . g x = sup ran S * < vol * A + B x
26 r19.23v g 2 A ran . g x = sup ran S * < vol * A + B x g 2 A ran . g x = sup ran S * < vol * A + B x
27 26 ralbii x * g 2 A ran . g x = sup ran S * < vol * A + B x x * g 2 A ran . g x = sup ran S * < vol * A + B x
28 ancomst A ran . g x = sup ran S * < vol * A + B x x = sup ran S * < A ran . g vol * A + B x
29 impexp x = sup ran S * < A ran . g vol * A + B x x = sup ran S * < A ran . g vol * A + B x
30 28 29 bitri A ran . g x = sup ran S * < vol * A + B x x = sup ran S * < A ran . g vol * A + B x
31 30 ralbii x * A ran . g x = sup ran S * < vol * A + B x x * x = sup ran S * < A ran . g vol * A + B x
32 elovolmlem g 2 g : 2
33 eqid abs g = abs g
34 33 1 ovolsf g : 2 S : 0 +∞
35 32 34 sylbi g 2 S : 0 +∞
36 35 frnd g 2 ran S 0 +∞
37 icossxr 0 +∞ *
38 36 37 sstrdi g 2 ran S *
39 supxrcl ran S * sup ran S * < *
40 38 39 syl g 2 sup ran S * < *
41 breq2 x = sup ran S * < vol * A + B x vol * A + B sup ran S * <
42 41 imbi2d x = sup ran S * < A ran . g vol * A + B x A ran . g vol * A + B sup ran S * <
43 42 ceqsralv sup ran S * < * x * x = sup ran S * < A ran . g vol * A + B x A ran . g vol * A + B sup ran S * <
44 40 43 syl g 2 x * x = sup ran S * < A ran . g vol * A + B x A ran . g vol * A + B sup ran S * <
45 31 44 syl5bb g 2 x * A ran . g x = sup ran S * < vol * A + B x A ran . g vol * A + B sup ran S * <
46 45 ralbiia g 2 x * A ran . g x = sup ran S * < vol * A + B x g 2 A ran . g vol * A + B sup ran S * <
47 25 27 46 3bitr3i x * g 2 A ran . g x = sup ran S * < vol * A + B x g 2 A ran . g vol * A + B sup ran S * <
48 24 47 bitri x y * | g 2 A ran . g y = sup ran seq 1 + abs g * < vol * A + B x g 2 A ran . g vol * A + B sup ran S * <
49 16 48 bitr2di A vol * A B + g 2 A ran . g vol * A + B sup ran S * < vol * A + B sup y * | g 2 A ran . g y = sup ran seq 1 + abs g * < * <
50 12 49 bitr4d A vol * A B + vol * A + B vol * A g 2 A ran . g vol * A + B sup ran S * <
51 8 50 mtbid A vol * A B + ¬ g 2 A ran . g vol * A + B sup ran S * <
52 rexanali g 2 A ran . g ¬ vol * A + B sup ran S * < ¬ g 2 A ran . g vol * A + B sup ran S * <
53 51 52 sylibr A vol * A B + g 2 A ran . g ¬ vol * A + B sup ran S * <
54 xrltnle sup ran S * < * vol * A + B * sup ran S * < < vol * A + B ¬ vol * A + B sup ran S * <
55 xrltle sup ran S * < * vol * A + B * sup ran S * < < vol * A + B sup ran S * < vol * A + B
56 54 55 sylbird sup ran S * < * vol * A + B * ¬ vol * A + B sup ran S * < sup ran S * < vol * A + B
57 40 14 56 syl2anr A vol * A B + g 2 ¬ vol * A + B sup ran S * < sup ran S * < vol * A + B
58 57 anim2d A vol * A B + g 2 A ran . g ¬ vol * A + B sup ran S * < A ran . g sup ran S * < vol * A + B
59 58 reximdva A vol * A B + g 2 A ran . g ¬ vol * A + B sup ran S * < g 2 A ran . g sup ran S * < vol * A + B
60 53 59 mpd A vol * A B + g 2 A ran . g sup ran S * < vol * A + B