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

Proof

Step Hyp Ref Expression
1 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
2 fss
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
3 1 2 mpan2
 |-  ( F : RR --> ( 0 [,) +oo ) -> F : RR --> RR )
4 ffvelrn
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR )
5 elrege0
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
6 5 baib
 |-  ( ( F ` x ) e. RR -> ( ( F ` x ) e. ( 0 [,) +oo ) <-> 0 <_ ( F ` x ) ) )
7 4 6 syl
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( ( F ` x ) e. ( 0 [,) +oo ) <-> 0 <_ ( F ` x ) ) )
8 7 ralbidva
 |-  ( F : RR --> RR -> ( A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) <-> A. x e. RR 0 <_ ( F ` x ) ) )
9 ffn
 |-  ( F : RR --> RR -> F Fn RR )
10 ffnfv
 |-  ( F : RR --> ( 0 [,) +oo ) <-> ( F Fn RR /\ A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) )
11 10 baib
 |-  ( F Fn RR -> ( F : RR --> ( 0 [,) +oo ) <-> A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) )
12 9 11 syl
 |-  ( F : RR --> RR -> ( F : RR --> ( 0 [,) +oo ) <-> A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) )
13 0cn
 |-  0 e. CC
14 fnconstg
 |-  ( 0 e. CC -> ( CC X. { 0 } ) Fn CC )
15 13 14 ax-mp
 |-  ( CC X. { 0 } ) Fn CC
16 df-0p
 |-  0p = ( CC X. { 0 } )
17 16 fneq1i
 |-  ( 0p Fn CC <-> ( CC X. { 0 } ) Fn CC )
18 15 17 mpbir
 |-  0p Fn CC
19 18 a1i
 |-  ( F : RR --> RR -> 0p Fn CC )
20 cnex
 |-  CC e. _V
21 20 a1i
 |-  ( F : RR --> RR -> CC e. _V )
22 reex
 |-  RR e. _V
23 22 a1i
 |-  ( F : RR --> RR -> RR e. _V )
24 ax-resscn
 |-  RR C_ CC
25 sseqin2
 |-  ( RR C_ CC <-> ( CC i^i RR ) = RR )
26 24 25 mpbi
 |-  ( CC i^i RR ) = RR
27 0pval
 |-  ( x e. CC -> ( 0p ` x ) = 0 )
28 27 adantl
 |-  ( ( F : RR --> RR /\ x e. CC ) -> ( 0p ` x ) = 0 )
29 eqidd
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
30 19 9 21 23 26 28 29 ofrfval
 |-  ( F : RR --> RR -> ( 0p oR <_ F <-> A. x e. RR 0 <_ ( F ` x ) ) )
31 8 12 30 3bitr4d
 |-  ( F : RR --> RR -> ( F : RR --> ( 0 [,) +oo ) <-> 0p oR <_ F ) )
32 3 31 biadanii
 |-  ( F : RR --> ( 0 [,) +oo ) <-> ( F : RR --> RR /\ 0p oR <_ F ) )