Metamath Proof Explorer

Theorem itg2ub

Description: The integral of a nonnegative real function F is an upper bound on the integrals of all simple functions G dominated by F . (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2ub ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{1}\left({G}\right)\le {\int }^{2}\left({F}\right)$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}=\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}$
2 1 itg2lcl ${⊢}\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\subseteq {ℝ}^{*}$
3 1 itg2lr ${⊢}\left({G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{1}\left({G}\right)\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}$
4 3 3adant1 ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{1}\left({G}\right)\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}$
5 supxrub ${⊢}\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {\int }^{1}\left({G}\right)\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\right)\to {\int }^{1}\left({G}\right)\le sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
6 2 4 5 sylancr ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{1}\left({G}\right)\le sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
7 1 itg2val ${⊢}{F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\to {\int }^{2}\left({F}\right)=sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
8 7 3ad2ant1 ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{2}\left({F}\right)=sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
9 6 8 breqtrrd ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {G}{\le }_{f}{F}\right)\to {\int }^{1}\left({G}\right)\le {\int }^{2}\left({F}\right)$