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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn | |
|
2 | 1 | adantr | |
3 | ax-resscn | |
|
4 | 3 | a1i | |
5 | 4 1 | 0pledm | |
6 | 0re | |
|
7 | fnconstg | |
|
8 | 6 7 | mp1i | |
9 | reex | |
|
10 | 9 | a1i | |
11 | inidm | |
|
12 | c0ex | |
|
13 | 12 | fvconst2 | |
14 | 13 | adantl | |
15 | eqidd | |
|
16 | 8 1 10 10 11 14 15 | ofrfval | |
17 | ffvelrn | |
|
18 | 17 | rexrd | |
19 | 18 | biantrurd | |
20 | elxrge0 | |
|
21 | 19 20 | bitr4di | |
22 | 21 | ralbidva | |
23 | 5 16 22 | 3bitrd | |
24 | 23 | biimpa | |
25 | ffnfv | |
|
26 | 2 24 25 | sylanbrc | |