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	$⊢ φ \to F \in dom \int^{1}$
	itg10a.2	$⊢ φ \to A \subseteq ℝ$
	itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
	itg1lea.4	$⊢ φ \to G \in dom \int^{1}$
	itg1lea.5	$⊢ (φ \land x \in (ℝ ∖ A)) \to F (x) \leq G (x)$
Assertion	itg1lea	$⊢ φ \to \int^{1} (F) \leq \int^{1} (G)$

Proof

Step	Hyp	Ref	Expression
1		itg10a.1	$⊢ φ \to F \in dom \int^{1}$
2		itg10a.2	$⊢ φ \to A \subseteq ℝ$
3		itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
4		itg1lea.4	$⊢ φ \to G \in dom \int^{1}$
5		itg1lea.5	$⊢ (φ \land x \in (ℝ ∖ A)) \to F (x) \leq G (x)$
6		i1fsub	$⊢ (G \in dom \int^{1} \land F \in dom \int^{1}) \to G -_{f} F \in dom \int^{1}$
7	4 1 6	syl2anc	$⊢ φ \to G -_{f} F \in dom \int^{1}$
8		eldifi	$⊢ x \in (ℝ ∖ A) \to x \in ℝ$
9		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
10	4 9	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
11	10	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to G (x) \in ℝ$
12		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
13	1 12	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
14	13	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to F (x) \in ℝ$
15	11 14	subge0d	$⊢ (φ \land x \in ℝ) \to (0 \leq G (x) - F (x) \leftrightarrow F (x) \leq G (x))$
16	8 15	sylan2	$⊢ (φ \land x \in (ℝ ∖ A)) \to (0 \leq G (x) - F (x) \leftrightarrow F (x) \leq G (x))$
17	5 16	mpbird	$⊢ (φ \land x \in (ℝ ∖ A)) \to 0 \leq G (x) - F (x)$
18	10	ffnd	$⊢ φ \to G Fn ℝ$
19	13	ffnd	$⊢ φ \to F Fn ℝ$
20		reex	$⊢ ℝ \in V$
21	20	a1i	$⊢ φ \to ℝ \in V$
22		inidm	$⊢ ℝ \cap ℝ = ℝ$
23		eqidd	$⊢ (φ \land x \in ℝ) \to G (x) = G (x)$
24		eqidd	$⊢ (φ \land x \in ℝ) \to F (x) = F (x)$
25	18 19 21 21 22 23 24	ofval	$⊢ (φ \land x \in ℝ) \to (G -_{f} F) (x) = G (x) - F (x)$
26	8 25	sylan2	$⊢ (φ \land x \in (ℝ ∖ A)) \to (G -_{f} F) (x) = G (x) - F (x)$
27	17 26	breqtrrd	$⊢ (φ \land x \in (ℝ ∖ A)) \to 0 \leq (G -_{f} F) (x)$
28	7 2 3 27	itg1ge0a	$⊢ φ \to 0 \leq \int^{1} (G -_{f} F)$
29		itg1sub	$⊢ (G \in dom \int^{1} \land F \in dom \int^{1}) \to \int^{1} (G -_{f} F) = \int^{1} (G) - \int^{1} (F)$
30	4 1 29	syl2anc	$⊢ φ \to \int^{1} (G -_{f} F) = \int^{1} (G) - \int^{1} (F)$
31	28 30	breqtrd	$⊢ φ \to 0 \leq \int^{1} (G) - \int^{1} (F)$
32		itg1cl	$⊢ G \in dom \int^{1} \to \int^{1} (G) \in ℝ$
33	4 32	syl	$⊢ φ \to \int^{1} (G) \in ℝ$
34		itg1cl	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$
35	1 34	syl	$⊢ φ \to \int^{1} (F) \in ℝ$
36	33 35	subge0d	$⊢ φ \to (0 \leq \int^{1} (G) - \int^{1} (F) \leftrightarrow \int^{1} (F) \leq \int^{1} (G))$
37	31 36	mpbid	$⊢ φ \to \int^{1} (F) \leq \int^{1} (G)$

Metamath Proof Explorer

Theorem itg1lea

Proof