Theorem itg2ub

Description: The integral of a nonnegative real function F is an upper bound on the integrals of all simple functions G dominated by F . (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	itg2ub	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ≤ ( ∫2 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2	1	itg2lcl	⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ*
3	1	itg2lr	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } )
4	3	3adant1	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } )
5		supxrub	⊢ ( ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ* ∧ ( ∫1 ‘ 𝐺 ) ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ) → ( ∫1 ‘ 𝐺 ) ≤ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
6	2 4 5	sylancr	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ≤ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
7	1	itg2val	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) = sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
8	7	3ad2ant1	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫2 ‘ 𝐹 ) = sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
9	6 8	breqtrrd	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ≤ ( ∫2 ‘ 𝐹 ) )