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𝑝fFF:0+∞

Proof

Step Hyp Ref Expression
1 ffn F:FFn
2 1 adantr F:0𝑝fFFFn
3 ax-resscn
4 3 a1i F:
5 4 1 0pledm F:0𝑝fF×0fF
6 0re 0
7 fnconstg 0×0Fn
8 6 7 mp1i F:×0Fn
9 reex V
10 9 a1i F:V
11 inidm =
12 c0ex 0V
13 12 fvconst2 x×0x=0
14 13 adantl F:x×0x=0
15 eqidd F:xFx=Fx
16 8 1 10 10 11 14 15 ofrfval F:×0fFx0Fx
17 ffvelrn F:xFx
18 17 rexrd F:xFx*
19 18 biantrurd F:x0FxFx*0Fx
20 elxrge0 Fx0+∞Fx*0Fx
21 19 20 bitr4di F:x0FxFx0+∞
22 21 ralbidva F:x0FxxFx0+∞
23 5 16 22 3bitrd F:0𝑝fFxFx0+∞
24 23 biimpa F:0𝑝fFxFx0+∞
25 ffnfv F:0+∞FFnxFx0+∞
26 2 24 25 sylanbrc F:0𝑝fFF:0+∞