# Metamath Proof Explorer

## Theorem itg1ge0a

Description: The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg10a.1 ${⊢}{\phi }\to {F}\in \mathrm{dom}{\int }^{1}$
itg10a.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
itg10a.3 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
itg1ge0a.4 ${⊢}\left({\phi }\wedge {x}\in \left(ℝ\setminus {A}\right)\right)\to 0\le {F}\left({x}\right)$
Assertion itg1ge0a ${⊢}{\phi }\to 0\le {\int }^{1}\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 itg10a.1 ${⊢}{\phi }\to {F}\in \mathrm{dom}{\int }^{1}$
2 itg10a.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
3 itg10a.3 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
4 itg1ge0a.4 ${⊢}\left({\phi }\wedge {x}\in \left(ℝ\setminus {A}\right)\right)\to 0\le {F}\left({x}\right)$
5 i1frn ${⊢}{F}\in \mathrm{dom}{\int }^{1}\to \mathrm{ran}{F}\in \mathrm{Fin}$
6 1 5 syl ${⊢}{\phi }\to \mathrm{ran}{F}\in \mathrm{Fin}$
7 difss ${⊢}\mathrm{ran}{F}\setminus \left\{0\right\}\subseteq \mathrm{ran}{F}$
8 ssfi ${⊢}\left(\mathrm{ran}{F}\in \mathrm{Fin}\wedge \mathrm{ran}{F}\setminus \left\{0\right\}\subseteq \mathrm{ran}{F}\right)\to \mathrm{ran}{F}\setminus \left\{0\right\}\in \mathrm{Fin}$
9 6 7 8 sylancl ${⊢}{\phi }\to \mathrm{ran}{F}\setminus \left\{0\right\}\in \mathrm{Fin}$
10 i1ff ${⊢}{F}\in \mathrm{dom}{\int }^{1}\to {F}:ℝ⟶ℝ$
11 1 10 syl ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
12 11 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq ℝ$
13 12 ssdifssd ${⊢}{\phi }\to \mathrm{ran}{F}\setminus \left\{0\right\}\subseteq ℝ$
14 13 sselda ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to {k}\in ℝ$
15 i1fima2sn ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)\in ℝ$
16 1 15 sylan ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)\in ℝ$
17 14 16 remulcld ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)\in ℝ$
18 0le0 ${⊢}0\le 0$
19 i1fima ${⊢}{F}\in \mathrm{dom}{\int }^{1}\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\in \mathrm{dom}vol$
20 1 19 syl ${⊢}{\phi }\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\in \mathrm{dom}vol$
21 mblvol ${⊢}{{F}}^{-1}\left[\left\{{k}\right\}\right]\in \mathrm{dom}vol\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)={vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
22 20 21 syl ${⊢}{\phi }\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)={vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
23 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)={vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
24 11 ffnd ${⊢}{\phi }\to {F}Fnℝ$
25 fniniseg ${⊢}{F}Fnℝ\to \left({x}\in {{F}}^{-1}\left[\left\{{k}\right\}\right]↔\left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)$
26 24 25 syl ${⊢}{\phi }\to \left({x}\in {{F}}^{-1}\left[\left\{{k}\right\}\right]↔\left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)$
27 26 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to \left({x}\in {{F}}^{-1}\left[\left\{{k}\right\}\right]↔\left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)$
28 simprl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to {x}\in ℝ$
29 eldif ${⊢}{x}\in \left(ℝ\setminus {A}\right)↔\left({x}\in ℝ\wedge ¬{x}\in {A}\right)$
30 4 ex ${⊢}{\phi }\to \left({x}\in \left(ℝ\setminus {A}\right)\to 0\le {F}\left({x}\right)\right)$
31 30 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left({x}\in \left(ℝ\setminus {A}\right)\to 0\le {F}\left({x}\right)\right)$
32 simprr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to {F}\left({x}\right)={k}$
33 32 breq2d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left(0\le {F}\left({x}\right)↔0\le {k}\right)$
34 0red ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to 0\in ℝ$
35 14 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to {k}\in ℝ$
36 34 35 lenltd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left(0\le {k}↔¬{k}<0\right)$
37 33 36 bitrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left(0\le {F}\left({x}\right)↔¬{k}<0\right)$
38 31 37 sylibd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left({x}\in \left(ℝ\setminus {A}\right)\to ¬{k}<0\right)$
39 29 38 syl5bir ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left(\left({x}\in ℝ\wedge ¬{x}\in {A}\right)\to ¬{k}<0\right)$
40 28 39 mpand ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left(¬{x}\in {A}\to ¬{k}<0\right)$
41 40 con4d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge \left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\right)\to \left({k}<0\to {x}\in {A}\right)$
42 41 impancom ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to \left(\left({x}\in ℝ\wedge {F}\left({x}\right)={k}\right)\to {x}\in {A}\right)$
43 27 42 sylbid ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to \left({x}\in {{F}}^{-1}\left[\left\{{k}\right\}\right]\to {x}\in {A}\right)$
44 43 ssrdv ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\subseteq {A}$
45 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {A}\subseteq ℝ$
46 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {vol}^{*}\left({A}\right)=0$
47 ovolssnul ${⊢}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\subseteq {A}\wedge {A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)=0\right)\to {vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)=0$
48 44 45 46 47 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)=0$
49 23 48 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)=0$
50 49 oveq2d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)={k}\cdot 0$
51 14 recnd ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to {k}\in ℂ$
52 51 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {k}\in ℂ$
53 52 mul01d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {k}\cdot 0=0$
54 50 53 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)=0$
55 18 54 breqtrrid ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge {k}<0\right)\to 0\le {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
56 14 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to {k}\in ℝ$
57 16 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)\in ℝ$
58 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to 0\le {k}$
59 20 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\in \mathrm{dom}vol$
60 mblss ${⊢}{{F}}^{-1}\left[\left\{{k}\right\}\right]\in \mathrm{dom}vol\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\subseteq ℝ$
61 59 60 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to {{F}}^{-1}\left[\left\{{k}\right\}\right]\subseteq ℝ$
62 ovolge0 ${⊢}{{F}}^{-1}\left[\left\{{k}\right\}\right]\subseteq ℝ\to 0\le {vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
63 61 62 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to 0\le {vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
64 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)={vol}^{*}\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
65 63 64 breqtrrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to 0\le vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
66 56 57 58 65 mulge0d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\wedge 0\le {k}\right)\to 0\le {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
67 0red ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to 0\in ℝ$
68 55 66 14 67 ltlecasei ${⊢}\left({\phi }\wedge {k}\in \left(\mathrm{ran}{F}\setminus \left\{0\right\}\right)\right)\to 0\le {k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
69 9 17 68 fsumge0 ${⊢}{\phi }\to 0\le \sum _{{k}\in \mathrm{ran}{F}\setminus \left\{0\right\}}{k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
70 itg1val ${⊢}{F}\in \mathrm{dom}{\int }^{1}\to {\int }^{1}\left({F}\right)=\sum _{{k}\in \mathrm{ran}{F}\setminus \left\{0\right\}}{k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
71 1 70 syl ${⊢}{\phi }\to {\int }^{1}\left({F}\right)=\sum _{{k}\in \mathrm{ran}{F}\setminus \left\{0\right\}}{k}vol\left({{F}}^{-1}\left[\left\{{k}\right\}\right]\right)$
72 69 71 breqtrrd ${⊢}{\phi }\to 0\le {\int }^{1}\left({F}\right)$