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 +∞