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 : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 ffn
 |-  ( F : RR --> RR -> F Fn RR )
2 1 adantr
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> F Fn RR )
3 ax-resscn
 |-  RR C_ CC
4 3 a1i
 |-  ( F : RR --> RR -> RR C_ CC )
5 4 1 0pledm
 |-  ( F : RR --> RR -> ( 0p oR <_ F <-> ( RR X. { 0 } ) oR <_ F ) )
6 0re
 |-  0 e. RR
7 fnconstg
 |-  ( 0 e. RR -> ( RR X. { 0 } ) Fn RR )
8 6 7 mp1i
 |-  ( F : RR --> RR -> ( RR X. { 0 } ) Fn RR )
9 reex
 |-  RR e. _V
10 9 a1i
 |-  ( F : RR --> RR -> RR e. _V )
11 inidm
 |-  ( RR i^i RR ) = RR
12 c0ex
 |-  0 e. _V
13 12 fvconst2
 |-  ( x e. RR -> ( ( RR X. { 0 } ) ` x ) = 0 )
14 13 adantl
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( ( RR X. { 0 } ) ` x ) = 0 )
15 eqidd
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
16 8 1 10 10 11 14 15 ofrfval
 |-  ( F : RR --> RR -> ( ( RR X. { 0 } ) oR <_ F <-> A. x e. RR 0 <_ ( F ` x ) ) )
17 ffvelrn
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR )
18 17 rexrd
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR* )
19 18 biantrurd
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) ) )
20 elxrge0
 |-  ( ( F ` x ) e. ( 0 [,] +oo ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
21 19 20 bitr4di
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( F ` x ) e. ( 0 [,] +oo ) ) )
22 21 ralbidva
 |-  ( F : RR --> RR -> ( A. x e. RR 0 <_ ( F ` x ) <-> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
23 5 16 22 3bitrd
 |-  ( F : RR --> RR -> ( 0p oR <_ F <-> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
24 23 biimpa
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) )
25 ffnfv
 |-  ( F : RR --> ( 0 [,] +oo ) <-> ( F Fn RR /\ A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
26 2 24 25 sylanbrc
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )