Metamath Proof Explorer


Theorem itg2leub

Description: Any upper bound on the integrals of all simple functions G dominated by F is greater than ( S.2F ) , the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2leub F : 0 +∞ A * 2 F A g dom 1 g f F 1 g A

Proof

Step Hyp Ref Expression
1 eqid x | g dom 1 g f F x = 1 g = x | g dom 1 g f F x = 1 g
2 1 itg2val F : 0 +∞ 2 F = sup x | g dom 1 g f F x = 1 g * <
3 2 adantr F : 0 +∞ A * 2 F = sup x | g dom 1 g f F x = 1 g * <
4 3 breq1d F : 0 +∞ A * 2 F A sup x | g dom 1 g f F x = 1 g * < A
5 1 itg2lcl x | g dom 1 g f F x = 1 g *
6 supxrleub x | g dom 1 g f F x = 1 g * A * sup x | g dom 1 g f F x = 1 g * < A z x | g dom 1 g f F x = 1 g z A
7 5 6 mpan A * sup x | g dom 1 g f F x = 1 g * < A z x | g dom 1 g f F x = 1 g z A
8 7 adantl F : 0 +∞ A * sup x | g dom 1 g f F x = 1 g * < A z x | g dom 1 g f F x = 1 g z A
9 eqeq1 x = z x = 1 g z = 1 g
10 9 anbi2d x = z g f F x = 1 g g f F z = 1 g
11 10 rexbidv x = z g dom 1 g f F x = 1 g g dom 1 g f F z = 1 g
12 11 ralab z x | g dom 1 g f F x = 1 g z A z g dom 1 g f F z = 1 g z A
13 r19.23v g dom 1 g f F z = 1 g z A g dom 1 g f F z = 1 g z A
14 ancomst g f F z = 1 g z A z = 1 g g f F z A
15 impexp z = 1 g g f F z A z = 1 g g f F z A
16 14 15 bitri g f F z = 1 g z A z = 1 g g f F z A
17 16 ralbii g dom 1 g f F z = 1 g z A g dom 1 z = 1 g g f F z A
18 13 17 bitr3i g dom 1 g f F z = 1 g z A g dom 1 z = 1 g g f F z A
19 18 albii z g dom 1 g f F z = 1 g z A z g dom 1 z = 1 g g f F z A
20 ralcom4 g dom 1 z z = 1 g g f F z A z g dom 1 z = 1 g g f F z A
21 fvex 1 g V
22 breq1 z = 1 g z A 1 g A
23 22 imbi2d z = 1 g g f F z A g f F 1 g A
24 21 23 ceqsalv z z = 1 g g f F z A g f F 1 g A
25 24 ralbii g dom 1 z z = 1 g g f F z A g dom 1 g f F 1 g A
26 20 25 bitr3i z g dom 1 z = 1 g g f F z A g dom 1 g f F 1 g A
27 19 26 bitri z g dom 1 g f F z = 1 g z A g dom 1 g f F 1 g A
28 12 27 bitri z x | g dom 1 g f F x = 1 g z A g dom 1 g f F 1 g A
29 8 28 bitrdi F : 0 +∞ A * sup x | g dom 1 g f F x = 1 g * < A g dom 1 g f F 1 g A
30 4 29 bitrd F : 0 +∞ A * 2 F A g dom 1 g f F 1 g A