# 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 ${⊢}\left({F}:ℝ⟶ℝ\wedge {0}_{𝑝}{\le }_{f}{F}\right)\to {F}:ℝ⟶\left[0,\mathrm{+\infty }\right]$

### Proof

Step Hyp Ref Expression
1 ffn ${⊢}{F}:ℝ⟶ℝ\to {F}Fnℝ$
2 1 adantr ${⊢}\left({F}:ℝ⟶ℝ\wedge {0}_{𝑝}{\le }_{f}{F}\right)\to {F}Fnℝ$
3 ax-resscn ${⊢}ℝ\subseteq ℂ$
4 3 a1i ${⊢}{F}:ℝ⟶ℝ\to ℝ\subseteq ℂ$
5 4 1 0pledm ${⊢}{F}:ℝ⟶ℝ\to \left({0}_{𝑝}{\le }_{f}{F}↔\left(ℝ×\left\{0\right\}\right){\le }_{f}{F}\right)$
6 0re ${⊢}0\in ℝ$
7 fnconstg ${⊢}0\in ℝ\to \left(ℝ×\left\{0\right\}\right)Fnℝ$
8 6 7 mp1i ${⊢}{F}:ℝ⟶ℝ\to \left(ℝ×\left\{0\right\}\right)Fnℝ$
9 reex ${⊢}ℝ\in \mathrm{V}$
10 9 a1i ${⊢}{F}:ℝ⟶ℝ\to ℝ\in \mathrm{V}$
11 inidm ${⊢}ℝ\cap ℝ=ℝ$
12 c0ex ${⊢}0\in \mathrm{V}$
13 12 fvconst2 ${⊢}{x}\in ℝ\to \left(ℝ×\left\{0\right\}\right)\left({x}\right)=0$
14 13 adantl ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to \left(ℝ×\left\{0\right\}\right)\left({x}\right)=0$
15 eqidd ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to {F}\left({x}\right)={F}\left({x}\right)$
16 8 1 10 10 11 14 15 ofrfval ${⊢}{F}:ℝ⟶ℝ\to \left(\left(ℝ×\left\{0\right\}\right){\le }_{f}{F}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}0\le {F}\left({x}\right)\right)$
17 ffvelrn ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\in ℝ$
18 17 rexrd ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to {F}\left({x}\right)\in {ℝ}^{*}$
19 18 biantrurd ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to \left(0\le {F}\left({x}\right)↔\left({F}\left({x}\right)\in {ℝ}^{*}\wedge 0\le {F}\left({x}\right)\right)\right)$
20 elxrge0 ${⊢}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]↔\left({F}\left({x}\right)\in {ℝ}^{*}\wedge 0\le {F}\left({x}\right)\right)$
21 19 20 syl6bbr ${⊢}\left({F}:ℝ⟶ℝ\wedge {x}\in ℝ\right)\to \left(0\le {F}\left({x}\right)↔{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]\right)$
22 21 ralbidva ${⊢}{F}:ℝ⟶ℝ\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}0\le {F}\left({x}\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]\right)$
23 5 16 22 3bitrd ${⊢}{F}:ℝ⟶ℝ\to \left({0}_{𝑝}{\le }_{f}{F}↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]\right)$
24 23 biimpa ${⊢}\left({F}:ℝ⟶ℝ\wedge {0}_{𝑝}{\le }_{f}{F}\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]$
25 ffnfv ${⊢}{F}:ℝ⟶\left[0,\mathrm{+\infty }\right]↔\left({F}Fnℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]\right)$
26 2 24 25 sylanbrc ${⊢}\left({F}:ℝ⟶ℝ\wedge {0}_{𝑝}{\le }_{f}{F}\right)\to {F}:ℝ⟶\left[0,\mathrm{+\infty }\right]$