# Metamath Proof Explorer

## Theorem itg2cl

Description: The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2cl ${⊢}{F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\to {\int }^{2}\left({F}\right)\in {ℝ}^{*}$

### 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 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)$
3 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 {ℝ}^{*}$
4 supxrcl ${⊢}\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 {ℝ}^{*}\to 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)\in {ℝ}^{*}$
5 3 4 ax-mp ${⊢}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)\in {ℝ}^{*}$
6 2 5 eqeltrdi ${⊢}{F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\to {\int }^{2}\left({F}\right)\in {ℝ}^{*}$