Theorem itg1lea

Description: Approximate version of itg1le . If F <_ G for almost all x , then S.1 F <_ S.1 G . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Hypotheses	itg10a.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
	itg10a.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	itg10a.3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	itg1lea.4	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
	itg1lea.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
Assertion	itg1lea	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		itg10a.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2		itg10a.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		itg10a.3	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
4		itg1lea.4	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
5		itg1lea.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
6		i1fsub	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 )
7	4 1 6	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 )
8		eldifi	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
9		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
10	4 9	syl	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
11	10	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
12		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
13	1 12	syl	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
14	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15	11 14	subge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
16	8 15	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
17	5 16	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
18	10	ffnd	⊢ ( 𝜑 → 𝐺 Fn ℝ )
19	13	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℝ )
20		reex	⊢ ℝ ∈ V
21	20	a1i	⊢ ( 𝜑 → ℝ ∈ V )
22		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
23		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25	18 19 21 21 22 23 24	ofval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
26	8 25	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
27	17 26	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) )
28	7 2 3 27	itg1ge0a	⊢ ( 𝜑 → 0 ≤ ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) )
29		itg1sub	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
30	4 1 29	syl2anc	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
31	28 30	breqtrd	⊢ ( 𝜑 → 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
32		itg1cl	⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
33	4 32	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
34		itg1cl	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
35	1 34	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
36	33 35	subge0d	⊢ ( 𝜑 → ( 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ↔ ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) ) )
37	31 36	mpbid	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )