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 : 0 +∞ F : 0 𝑝 f F

Proof

Step Hyp Ref Expression
1 rge0ssre 0 +∞
2 fss F : 0 +∞ 0 +∞ F :
3 1 2 mpan2 F : 0 +∞ F :
4 ffvelrn F : x F x
5 elrege0 F x 0 +∞ F x 0 F x
6 5 baib F x F x 0 +∞ 0 F x
7 4 6 syl F : x F x 0 +∞ 0 F x
8 7 ralbidva F : x F x 0 +∞ x 0 F x
9 ffn F : F Fn
10 ffnfv F : 0 +∞ F Fn x F x 0 +∞
11 10 baib F Fn F : 0 +∞ x F x 0 +∞
12 9 11 syl F : F : 0 +∞ x F x 0 +∞
13 0cn 0
14 fnconstg 0 × 0 Fn
15 13 14 ax-mp × 0 Fn
16 df-0p 0 𝑝 = × 0
17 16 fneq1i 0 𝑝 Fn × 0 Fn
18 15 17 mpbir 0 𝑝 Fn
19 18 a1i F : 0 𝑝 Fn
20 cnex V
21 20 a1i F : V
22 reex V
23 22 a1i F : V
24 ax-resscn
25 sseqin2 =
26 24 25 mpbi =
27 0pval x 0 𝑝 x = 0
28 27 adantl F : x 0 𝑝 x = 0
29 eqidd F : x F x = F x
30 19 9 21 23 26 28 29 ofrfval F : 0 𝑝 f F x 0 F x
31 8 12 30 3bitr4d F : F : 0 +∞ 0 𝑝 f F
32 3 31 biadanii F : 0 +∞ F : 0 𝑝 f F