itg2le

Description: If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2le	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to \int^{2} (F) \leq \int^{2} (G)$

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2	1	a1i	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to ℝ \in V$
3		i1ff	$⊢ h \in dom \int^{1} \to h : ℝ ⟶ ℝ$
4	3	adantl	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to h : ℝ ⟶ ℝ$
5		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
6		fss	$⊢ (h : ℝ ⟶ ℝ \land ℝ \subseteq ℝ^{}) \to h : ℝ ⟶ ℝ^{}$
7	4 5 6	sylancl	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to h : ℝ ⟶ ℝ^{*}$
8		simpll	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to F : ℝ ⟶ [0, +∞]$
9		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
10		fss	$⊢ (F : ℝ ⟶ [0, +∞] \land [0, +∞] \subseteq ℝ^{}) \to F : ℝ ⟶ ℝ^{}$
11	8 9 10	sylancl	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to F : ℝ ⟶ ℝ^{*}$
12		simplr	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to G : ℝ ⟶ [0, +∞]$
13		fss	$⊢ (G : ℝ ⟶ [0, +∞] \land [0, +∞] \subseteq ℝ^{}) \to G : ℝ ⟶ ℝ^{}$
14	12 9 13	sylancl	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to G : ℝ ⟶ ℝ^{*}$
15		xrletr	$⊢ (x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to ((x \leq y \land y \leq z) \to x \leq z)$
16	15	adantl	$⊢ (((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \land (x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*})) \to ((x \leq y \land y \leq z) \to x \leq z)$
17	2 7 11 14 16	caoftrn	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to ((h \leq_{f} F \land F \leq_{f} G) \to h \leq_{f} G)$
18		simplr	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land (h \in dom \int^{1} \land h \leq_{f} G)) \to G : ℝ ⟶ [0, +∞]$
19		simprl	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land (h \in dom \int^{1} \land h \leq_{f} G)) \to h \in dom \int^{1}$
20		simprr	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land (h \in dom \int^{1} \land h \leq_{f} G)) \to h \leq_{f} G$
21		itg2ub	$⊢ (G : ℝ ⟶ [0, +∞] \land h \in dom \int^{1} \land h \leq_{f} G) \to \int^{1} (h) \leq \int^{2} (G)$
22	18 19 20 21	syl3anc	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land (h \in dom \int^{1} \land h \leq_{f} G)) \to \int^{1} (h) \leq \int^{2} (G)$
23	22	expr	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to (h \leq_{f} G \to \int^{1} (h) \leq \int^{2} (G))$
24	17 23	syld	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to ((h \leq_{f} F \land F \leq_{f} G) \to \int^{1} (h) \leq \int^{2} (G))$
25	24	ancomsd	$⊢ ((F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \land h \in dom \int^{1}) \to ((F \leq_{f} G \land h \leq_{f} F) \to \int^{1} (h) \leq \int^{2} (G))$
26	25	exp4b	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \to (h \in dom \int^{1} \to (F \leq_{f} G \to (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G))))$
27	26	com23	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞]) \to (F \leq_{f} G \to (h \in dom \int^{1} \to (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G))))$
28	27	3impia	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to (h \in dom \int^{1} \to (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G)))$
29	28	ralrimiv	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to \forall h \in dom \int^{1} (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G))$
30		simp1	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to F : ℝ ⟶ [0, +∞]$
31		itg2cl	$⊢ G : ℝ ⟶ [0, +∞] \to \int^{2} (G) \in ℝ^{*}$
32	31	3ad2ant2	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to \int^{2} (G) \in ℝ^{*}$
33		itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land \int^{2} (G) \in ℝ^{*}) \to (\int^{2} (F) \leq \int^{2} (G) \leftrightarrow \forall h \in dom \int^{1} (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G)))$
34	30 32 33	syl2anc	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to (\int^{2} (F) \leq \int^{2} (G) \leftrightarrow \forall h \in dom \int^{1} (h \leq_{f} F \to \int^{1} (h) \leq \int^{2} (G)))$
35	29 34	mpbird	$⊢ (F : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F \leq_{f} G) \to \int^{2} (F) \leq \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2le

Proof