Theorem 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	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		itg10	⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0
2		ffvelcdm	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
3		0xr	⊢ 0 ∈ ℝ*
4		pnfxr	⊢ +∞ ∈ ℝ*
5		elicc1	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ +∞ ) ) )
6	3 4 5	mp2an	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ +∞ ) )
7	6	simp2bi	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
8	2 7	syl	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
9	8	ralrimiva	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) )
10		0re	⊢ 0 ∈ ℝ
11		fnconstg	⊢ ( 0 ∈ ℝ → ( ℝ × { 0 } ) Fn ℝ )
12	10 11	mp1i	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ℝ × { 0 } ) Fn ℝ )
13		ffn	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 𝐹 Fn ℝ )
14		reex	⊢ ℝ ∈ V
15	14	a1i	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ℝ ∈ V )
16		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
17		c0ex	⊢ 0 ∈ V
18	17	fvconst2	⊢ ( 𝑦 ∈ ℝ → ( ( ℝ × { 0 } ) ‘ 𝑦 ) = 0 )
19	18	adantl	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( ( ℝ × { 0 } ) ‘ 𝑦 ) = 0 )
20		eqidd	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
21	12 13 15 15 16 19 20	ofrfval	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ℝ × { 0 } ) ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
22	9 21	mpbird	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ℝ × { 0 } ) ∘r ≤ 𝐹 )
23		i1f0	⊢ ( ℝ × { 0 } ) ∈ dom ∫1
24		itg2ub	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ℝ × { 0 } ) ∈ dom ∫1 ∧ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) )
25	23 24	mp3an2	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) )
26	22 25	mpdan	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫1 ‘ ( ℝ × { 0 } ) ) ≤ ( ∫2 ‘ 𝐹 ) )
27	1 26	eqbrtrrid	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ 𝐹 ) )