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𝑝≤fF

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:ℝ⟶ℝ→FFnℝ
10 ffnfv ⊢F:ℝ⟶0+∞↔FFnℝ∧∀x∈ℝF⁡x∈0+∞
11 10 baib ⊢FFnℝ→F:ℝ⟶0+∞↔∀x∈ℝF⁡x∈0+∞
12 9 11 syl ⊢F:ℝ⟶ℝ→F:ℝ⟶0+∞↔∀x∈ℝF⁡x∈0+∞
13 0cn ⊢0∈ℂ
14 fnconstg ⊢0∈ℂ→ℂ×0Fnℂ
15 13 14 ax-mp ⊢ℂ×0Fnℂ
16 df-0p ⊢0𝑝=ℂ×0
17 16 fneq1i ⊢0𝑝Fnℂ↔ℂ×0Fnℂ
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𝑝≤fF↔∀x∈ℝ0≤F⁡x
31 8 12 30 3bitr4d ⊢F:ℝ⟶ℝ→F:ℝ⟶0+∞↔0𝑝≤fF
32 3 31 biadanii ⊢F:ℝ⟶0+∞↔F:ℝ⟶ℝ∧0𝑝≤fF