Metamath Proof Explorer

Theorem itg2le

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

Ref Expression
Assertion itg2le ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→∫2⁡F≤∫2⁡G

Proof

Step Hyp Ref Expression
1 reex ⊢ℝ∈V
2 1 a1i ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→ℝ∈V
3 i1ff ⊢h∈dom⁡∫1→h:ℝ⟶ℝ
4 3 adantl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→h:ℝ⟶ℝ
5 ressxr ⊢ℝ⊆ℝ*
6 fss ⊢h:ℝ⟶ℝ∧ℝ⊆ℝ*→h:ℝ⟶ℝ*
7 4 5 6 sylancl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→h:ℝ⟶ℝ*
8 simpll ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→F:ℝ⟶0+∞
9 iccssxr ⊢0+∞⊆ℝ*
10 fss ⊢F:ℝ⟶0+∞∧0+∞⊆ℝ*→F:ℝ⟶ℝ*
11 8 9 10 sylancl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→F:ℝ⟶ℝ*
12 simplr ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→G:ℝ⟶0+∞
13 fss ⊢G:ℝ⟶0+∞∧0+∞⊆ℝ*→G:ℝ⟶ℝ*
14 12 9 13 sylancl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→G:ℝ⟶ℝ*
15 xrletr ⊢x∈ℝ*∧y∈ℝ*∧z∈ℝ*→x≤y∧y≤z→x≤z
16 15 adantl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1∧x∈ℝ*∧y∈ℝ*∧z∈ℝ*→x≤y∧y≤z→x≤z
17 2 7 11 14 16 caoftrn ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→h≤fF∧F≤fG→h≤fG
18 simplr ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1∧h≤fG→G:ℝ⟶0+∞
19 simprl ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1∧h≤fG→h∈dom⁡∫1
20 simprr ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1∧h≤fG→h≤fG
21 itg2ub ⊢G:ℝ⟶0+∞∧h∈dom⁡∫1∧h≤fG→∫1⁡h≤∫2⁡G
22 18 19 20 21 syl3anc ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1∧h≤fG→∫1⁡h≤∫2⁡G
23 22 expr ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→h≤fG→∫1⁡h≤∫2⁡G
24 17 23 syld ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→h≤fF∧F≤fG→∫1⁡h≤∫2⁡G
25 24 ancomsd ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧h∈dom⁡∫1→F≤fG∧h≤fF→∫1⁡h≤∫2⁡G
26 25 exp4b ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞→h∈dom⁡∫1→F≤fG→h≤fF→∫1⁡h≤∫2⁡G
27 26 com23 ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞→F≤fG→h∈dom⁡∫1→h≤fF→∫1⁡h≤∫2⁡G
28 27 3impia ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→h∈dom⁡∫1→h≤fF→∫1⁡h≤∫2⁡G
29 28 ralrimiv ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→∀h∈dom⁡∫1h≤fF→∫1⁡h≤∫2⁡G
30 simp1 ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→F:ℝ⟶0+∞
31 itg2cl ⊢G:ℝ⟶0+∞→∫2⁡G∈ℝ*
32 31 3ad2ant2 ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→∫2⁡G∈ℝ*
33 itg2leub ⊢F:ℝ⟶0+∞∧∫2⁡G∈ℝ*→∫2⁡F≤∫2⁡G↔∀h∈dom⁡∫1h≤fF→∫1⁡h≤∫2⁡G
34 30 32 33 syl2anc ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→∫2⁡F≤∫2⁡G↔∀h∈dom⁡∫1h≤fF→∫1⁡h≤∫2⁡G
35 29 34 mpbird ⊢F:ℝ⟶0+∞∧G:ℝ⟶0+∞∧F≤fG→∫2⁡F≤∫2⁡G