Metamath Proof Explorer

Theorem xrge0f

Description: A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion xrge0f ⊢ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F → F : ℝ ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 ffn ⊢ F : ℝ ⟶ ℝ → F Fn ℝ
2 1 adantr ⊢ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F → F Fn ℝ
3 ax-resscn ⊢ ℝ ⊆ ℂ
4 3 a1i ⊢ F : ℝ ⟶ ℝ → ℝ ⊆ ℂ
5 4 1 0pledm ⊢ F : ℝ ⟶ ℝ → 0 𝑝 ≤ f F ↔ ℝ × 0 ≤ f F
6 0re ⊢ 0 ∈ ℝ
7 fnconstg ⊢ 0 ∈ ℝ → ℝ × 0 Fn ℝ
8 6 7 mp1i ⊢ F : ℝ ⟶ ℝ → ℝ × 0 Fn ℝ
9 reex ⊢ ℝ ∈ V
10 9 a1i ⊢ F : ℝ ⟶ ℝ → ℝ ∈ V
11 inidm ⊢ ℝ ∩ ℝ = ℝ
12 c0ex ⊢ 0 ∈ V
13 12 fvconst2 ⊢ x ∈ ℝ → ℝ × 0 ⁡ x = 0
14 13 adantl ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → ℝ × 0 ⁡ x = 0
15 eqidd ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x = F ⁡ x
16 8 1 10 10 11 14 15 ofrfval ⊢ F : ℝ ⟶ ℝ → ℝ × 0 ≤ f F ↔ ∀ x ∈ ℝ 0 ≤ F ⁡ x
17 ffvelrn ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x ∈ ℝ
18 17 rexrd ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x ∈ ℝ *
19 18 biantrurd ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → 0 ≤ F ⁡ x ↔ F ⁡ x ∈ ℝ * ∧ 0 ≤ F ⁡ x
20 elxrge0 ⊢ F ⁡ x ∈ 0 +∞ ↔ F ⁡ x ∈ ℝ * ∧ 0 ≤ F ⁡ x
21 19 20 bitr4di ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → 0 ≤ F ⁡ x ↔ F ⁡ x ∈ 0 +∞
22 21 ralbidva ⊢ F : ℝ ⟶ ℝ → ∀ x ∈ ℝ 0 ≤ F ⁡ x ↔ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
23 5 16 22 3bitrd ⊢ F : ℝ ⟶ ℝ → 0 𝑝 ≤ f F ↔ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
24 23 biimpa ⊢ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F → ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
25 ffnfv ⊢ F : ℝ ⟶ 0 +∞ ↔ F Fn ℝ ∧ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
26 2 24 25 sylanbrc ⊢ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F → F : ℝ ⟶ 0 +∞