# Metamath Proof Explorer

## Theorem itg1le

Description: If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion itg1le ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to {\int }^{1}\left({F}\right)\le {\int }^{1}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to {F}\in \mathrm{dom}{\int }^{1}$
2 0ss ${⊢}\varnothing \subseteq ℝ$
3 2 a1i ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to \varnothing \subseteq ℝ$
4 ovol0 ${⊢}{vol}^{*}\left(\varnothing \right)=0$
5 4 a1i ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to {vol}^{*}\left(\varnothing \right)=0$
6 simp2 ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to {G}\in \mathrm{dom}{\int }^{1}$
7 simpl ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to {F}\in \mathrm{dom}{\int }^{1}$
8 i1ff ${⊢}{F}\in \mathrm{dom}{\int }^{1}\to {F}:ℝ⟶ℝ$
9 ffn ${⊢}{F}:ℝ⟶ℝ\to {F}Fnℝ$
10 7 8 9 3syl ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to {F}Fnℝ$
11 simpr ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to {G}\in \mathrm{dom}{\int }^{1}$
12 i1ff ${⊢}{G}\in \mathrm{dom}{\int }^{1}\to {G}:ℝ⟶ℝ$
13 ffn ${⊢}{G}:ℝ⟶ℝ\to {G}Fnℝ$
14 11 12 13 3syl ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to {G}Fnℝ$
15 reex ${⊢}ℝ\in \mathrm{V}$
16 15 a1i ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to ℝ\in \mathrm{V}$
17 inidm ${⊢}ℝ\cap ℝ=ℝ$
18 eqidd ${⊢}\left(\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\wedge {x}\in ℝ\right)\to {F}\left({x}\right)={F}\left({x}\right)$
19 eqidd ${⊢}\left(\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\wedge {x}\in ℝ\right)\to {G}\left({x}\right)={G}\left({x}\right)$
20 10 14 16 16 17 18 19 ofrval ${⊢}\left(\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\wedge {F}{\le }_{f}{G}\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\le {G}\left({x}\right)$
21 20 3exp ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\right)\to \left({F}{\le }_{f}{G}\to \left({x}\in ℝ\to {F}\left({x}\right)\le {G}\left({x}\right)\right)\right)$
22 21 3impia ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to \left({x}\in ℝ\to {F}\left({x}\right)\le {G}\left({x}\right)\right)$
23 eldifi ${⊢}{x}\in \left(ℝ\setminus \varnothing \right)\to {x}\in ℝ$
24 22 23 impel ${⊢}\left(\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\wedge {x}\in \left(ℝ\setminus \varnothing \right)\right)\to {F}\left({x}\right)\le {G}\left({x}\right)$
25 1 3 5 6 24 itg1lea ${⊢}\left({F}\in \mathrm{dom}{\int }^{1}\wedge {G}\in \mathrm{dom}{\int }^{1}\wedge {F}{\le }_{f}{G}\right)\to {\int }^{1}\left({F}\right)\le {\int }^{1}\left({G}\right)$