This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm 
 |-  ( ( 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 ) )