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 ⊢ F : ℝ ⟶ 0 +∞ → 0 ≤ ∫ 2 ⁡ F

Proof

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