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 ffvelrn ( ( 𝐹 : ℝ ⟶ ( 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𝐹 ) )