itg2ge0

Description: The integral of a nonnegative real function is greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		itg10	$⊢ \int^{1} (ℝ \times \{0\}) = 0$
2		ffvelcdm	$⊢ (F : ℝ ⟶ [0, +∞] \land y \in ℝ) \to F (y) \in [0, +∞]$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (F (y) \in [0, +∞] \leftrightarrow (F (y) \in ℝ^{*} \land 0 \leq F (y) \land F (y) \leq +∞))$
6	3 4 5	mp2an	$⊢ F (y) \in [0, +∞] \leftrightarrow (F (y) \in ℝ^{*} \land 0 \leq F (y) \land F (y) \leq +∞)$
7	6	simp2bi	$⊢ F (y) \in [0, +∞] \to 0 \leq F (y)$
8	2 7	syl	$⊢ (F : ℝ ⟶ [0, +∞] \land y \in ℝ) \to 0 \leq F (y)$
9	8	ralrimiva	$⊢ F : ℝ ⟶ [0, +∞] \to \forall y \in ℝ 0 \leq F (y)$
10		0re	$⊢ 0 \in ℝ$
11		fnconstg	$⊢ 0 \in ℝ \to (ℝ \times \{0\}) Fn ℝ$
12	10 11	mp1i	$⊢ F : ℝ ⟶ [0, +∞] \to (ℝ \times \{0\}) Fn ℝ$
13		ffn	$⊢ F : ℝ ⟶ [0, +∞] \to F Fn ℝ$
14		reex	$⊢ ℝ \in V$
15	14	a1i	$⊢ F : ℝ ⟶ [0, +∞] \to ℝ \in V$
16		inidm	$⊢ ℝ \cap ℝ = ℝ$
17		c0ex	$⊢ 0 \in V$
18	17	fvconst2	$⊢ y \in ℝ \to (ℝ \times \{0\}) (y) = 0$
19	18	adantl	$⊢ (F : ℝ ⟶ [0, +∞] \land y \in ℝ) \to (ℝ \times \{0\}) (y) = 0$
20		eqidd	$⊢ (F : ℝ ⟶ [0, +∞] \land y \in ℝ) \to F (y) = F (y)$
21	12 13 15 15 16 19 20	ofrfval	$⊢ F : ℝ ⟶ [0, +∞] \to ((ℝ \times \{0\}) \leq_{f} F \leftrightarrow \forall y \in ℝ 0 \leq F (y))$
22	9 21	mpbird	$⊢ F : ℝ ⟶ [0, +∞] \to (ℝ \times \{0\}) \leq_{f} F$
23		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
24		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land ℝ \times \{0\} \in dom \int^{1} \land (ℝ \times \{0\}) \leq_{f} F) \to \int^{1} (ℝ \times \{0\}) \leq \int^{2} (F)$
25	23 24	mp3an2	$⊢ (F : ℝ ⟶ [0, +∞] \land (ℝ \times \{0\}) \leq_{f} F) \to \int^{1} (ℝ \times \{0\}) \leq \int^{2} (F)$
26	22 25	mpdan	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{1} (ℝ \times \{0\}) \leq \int^{2} (F)$
27	1 26	eqbrtrrid	$⊢ F : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2ge0

Proof