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	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → 𝐹 ∈ dom ∫1 )
2		0ss	⊢ ∅ ⊆ ℝ
3	2	a1i	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ∅ ⊆ ℝ )
4		ovol0	⊢ ( vol* ‘ ∅ ) = 0
5	4	a1i	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( vol* ‘ ∅ ) = 0 )
6		simp2	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → 𝐺 ∈ dom ∫1 )
7		simpl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 ∈ dom ∫1 )
8		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
9		ffn	⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
10	7 8 9	3syl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 Fn ℝ )
11		simpr	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 ∈ dom ∫1 )
12		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
13		ffn	⊢ ( 𝐺 : ℝ ⟶ ℝ → 𝐺 Fn ℝ )
14	11 12 13	3syl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 Fn ℝ )
15		reex	⊢ ℝ ∈ V
16	15	a1i	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ℝ ∈ V )
17		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
18		eqidd	⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19		eqidd	⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
20	10 14 16 16 17 18 19	ofrval	⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝐹 ∘r ≤ 𝐺 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
21	20	3exp	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘r ≤ 𝐺 → ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) )
22	21	3impia	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
23		eldifi	⊢ ( 𝑥 ∈ ( ℝ ∖ ∅ ) → 𝑥 ∈ ℝ )
24	22 23	impel	⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) ∧ 𝑥 ∈ ( ℝ ∖ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
25	1 3 5 6 24	itg1lea	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )