Metamath Proof Explorer

Theorem 0plef

Description: Two ways to say that the function F on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Assertion 0plef ⊢ F : ℝ ⟶ 0 +∞ ↔ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F

Proof

Step Hyp Ref Expression
1 rge0ssre ⊢ 0 +∞ ⊆ ℝ
2 fss ⊢ F : ℝ ⟶ 0 +∞ ∧ 0 +∞ ⊆ ℝ → F : ℝ ⟶ ℝ
3 1 2 mpan2 ⊢ F : ℝ ⟶ 0 +∞ → F : ℝ ⟶ ℝ
4 ffvelcdm ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x ∈ ℝ
5 elrege0 ⊢ F ⁡ x ∈ 0 +∞ ↔ F ⁡ x ∈ ℝ ∧ 0 ≤ F ⁡ x
6 5 baib ⊢ F ⁡ x ∈ ℝ → F ⁡ x ∈ 0 +∞ ↔ 0 ≤ F ⁡ x
7 4 6 syl ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x ∈ 0 +∞ ↔ 0 ≤ F ⁡ x
8 7 ralbidva ⊢ F : ℝ ⟶ ℝ → ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞ ↔ ∀ x ∈ ℝ 0 ≤ F ⁡ x
9 ffn ⊢ F : ℝ ⟶ ℝ → F Fn ℝ
10 ffnfv ⊢ F : ℝ ⟶ 0 +∞ ↔ F Fn ℝ ∧ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
11 10 baib ⊢ F Fn ℝ → F : ℝ ⟶ 0 +∞ ↔ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
12 9 11 syl ⊢ F : ℝ ⟶ ℝ → F : ℝ ⟶ 0 +∞ ↔ ∀ x ∈ ℝ F ⁡ x ∈ 0 +∞
13 0cn ⊢ 0 ∈ ℂ
14 fnconstg ⊢ 0 ∈ ℂ → ℂ × 0 Fn ℂ
15 13 14 ax-mp ⊢ ℂ × 0 Fn ℂ
16 df-0p ⊢ 0 𝑝 = ℂ × 0
17 16 fneq1i ⊢ 0 𝑝 Fn ℂ ↔ ℂ × 0 Fn ℂ
18 15 17 mpbir ⊢ 0 𝑝 Fn ℂ
19 18 a1i ⊢ F : ℝ ⟶ ℝ → 0 𝑝 Fn ℂ
20 cnex ⊢ ℂ ∈ V
21 20 a1i ⊢ F : ℝ ⟶ ℝ → ℂ ∈ V
22 reex ⊢ ℝ ∈ V
23 22 a1i ⊢ F : ℝ ⟶ ℝ → ℝ ∈ V
24 ax-resscn ⊢ ℝ ⊆ ℂ
25 sseqin2 ⊢ ℝ ⊆ ℂ ↔ ℂ ∩ ℝ = ℝ
26 24 25 mpbi ⊢ ℂ ∩ ℝ = ℝ
27 0pval ⊢ x ∈ ℂ → 0 𝑝 ⁡ x = 0
28 27 adantl ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℂ → 0 𝑝 ⁡ x = 0
29 eqidd ⊢ F : ℝ ⟶ ℝ ∧ x ∈ ℝ → F ⁡ x = F ⁡ x
30 19 9 21 23 26 28 29 ofrfval ⊢ F : ℝ ⟶ ℝ → 0 𝑝 ≤ f F ↔ ∀ x ∈ ℝ 0 ≤ F ⁡ x
31 8 12 30 3bitr4d ⊢ F : ℝ ⟶ ℝ → F : ℝ ⟶ 0 +∞ ↔ 0 𝑝 ≤ f F
32 3 31 biadanii ⊢ F : ℝ ⟶ 0 +∞ ↔ F : ℝ ⟶ ℝ ∧ 0 𝑝 ≤ f F