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	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to \int^{1} (F) \leq \int^{1} (G)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to F \in dom \int^{1}$
2		0ss	$⊢ \emptyset \subseteq ℝ$
3	2	a1i	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to \emptyset \subseteq ℝ$
4		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
5	4	a1i	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to {vol}^{*} (\emptyset) = 0$
6		simp2	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to G \in dom \int^{1}$
7		simpl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F \in dom \int^{1}$
8		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
9		ffn	$⊢ F : ℝ ⟶ ℝ \to F Fn ℝ$
10	7 8 9	3syl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F Fn ℝ$
11		simpr	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to G \in dom \int^{1}$
12		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
13		ffn	$⊢ G : ℝ ⟶ ℝ \to G Fn ℝ$
14	11 12 13	3syl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to G Fn ℝ$
15		reex	$⊢ ℝ \in V$
16	15	a1i	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to ℝ \in V$
17		inidm	$⊢ ℝ \cap ℝ = ℝ$
18		eqidd	$⊢ ((F \in dom \int^{1} \land G \in dom \int^{1}) \land x \in ℝ) \to F (x) = F (x)$
19		eqidd	$⊢ ((F \in dom \int^{1} \land G \in dom \int^{1}) \land x \in ℝ) \to G (x) = G (x)$
20	10 14 16 16 17 18 19	ofrval	$⊢ ((F \in dom \int^{1} \land G \in dom \int^{1}) \land F \leq_{f} G \land x \in ℝ) \to F (x) \leq G (x)$
21	20	3exp	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to (F \leq_{f} G \to (x \in ℝ \to F (x) \leq G (x)))$
22	21	3impia	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to (x \in ℝ \to F (x) \leq G (x))$
23		eldifi	$⊢ x \in (ℝ ∖ \emptyset) \to x \in ℝ$
24	22 23	impel	$⊢ ((F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \land x \in (ℝ ∖ \emptyset)) \to F (x) \leq G (x)$
25	1 3 5 6 24	itg1lea	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1} \land F \leq_{f} G) \to \int^{1} (F) \leq \int^{1} (G)$

Metamath Proof Explorer

Theorem itg1le

Proof