This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) )