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 ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 1 a1i ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ℝ ∈ V )
3 i1ff ⊢ ( ℎ ∈ dom ∫1 → ℎ : ℝ ⟶ ℝ )
4 3 adantl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ℎ : ℝ ⟶ ℝ )
5 ressxr ⊢ ℝ ⊆ ℝ*
6 fss ⊢ ( ( ℎ : ℝ ⟶ ℝ ∧ ℝ ⊆ ℝ* ) → ℎ : ℝ ⟶ ℝ* )
7 4 5 6 sylancl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ℎ : ℝ ⟶ ℝ* )
8 simpll ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
9 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
10 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐹 : ℝ ⟶ ℝ* )
11 8 9 10 sylancl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → 𝐹 : ℝ ⟶ ℝ* )
12 simplr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
13 fss ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐺 : ℝ ⟶ ℝ* )
14 12 9 13 sylancl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → 𝐺 : ℝ ⟶ ℝ* )
15 xrletr ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
16 15 adantl ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
17 2 7 11 14 16 caoftrn ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ( ( ℎ ∘r ≤ 𝐹 ∧ 𝐹 ∘r ≤ 𝐺 ) → ℎ ∘r ≤ 𝐺 ) )
18 simplr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ( ℎ ∈ dom ∫1 ∧ ℎ ∘r ≤ 𝐺 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
19 simprl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ( ℎ ∈ dom ∫1 ∧ ℎ ∘r ≤ 𝐺 ) ) → ℎ ∈ dom ∫1 )
20 simprr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ( ℎ ∈ dom ∫1 ∧ ℎ ∘r ≤ 𝐺 ) ) → ℎ ∘r ≤ 𝐺 )
21 itg2ub ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ℎ ∈ dom ∫1 ∧ ℎ ∘r ≤ 𝐺 ) → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) )
22 18 19 20 21 syl3anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ( ℎ ∈ dom ∫1 ∧ ℎ ∘r ≤ 𝐺 ) ) → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) )
23 22 expr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ( ℎ ∘r ≤ 𝐺 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) )
24 17 23 syld ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ( ( ℎ ∘r ≤ 𝐹 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) )
25 24 ancomsd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) ∧ ℎ ∈ dom ∫1 ) → ( ( 𝐹 ∘r ≤ 𝐺 ∧ ℎ ∘r ≤ 𝐹 ) → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) )
26 25 exp4b ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) → ( ℎ ∈ dom ∫1 → ( 𝐹 ∘r ≤ 𝐺 → ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) ) ) )
27 26 com23 ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ) → ( 𝐹 ∘r ≤ 𝐺 → ( ℎ ∈ dom ∫1 → ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) ) ) )
28 27 3impia ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ℎ ∈ dom ∫1 → ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
29 28 ralrimiv ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ∀ ℎ ∈ dom ∫1 ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) )
30 simp1 ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
31 itg2cl ⊢ ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
32 31 3ad2ant2 ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
33 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ ℎ ∈ dom ∫1 ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
34 30 32 33 syl2anc ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ ℎ ∈ dom ∫1 ( ℎ ∘r ≤ 𝐹 → ( ∫1 ‘ ℎ ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
35 29 34 mpbird ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )