Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  0plef Structured version   Unicode version

Theorem 0plef 22567
 Description: Two ways to say that the function on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.)
Assertion
Ref Expression
0plef

Proof of Theorem 0plef
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rge0ssre 11686 . . 3
2 fss 5692 . . 3
31, 2mpan2 675 . 2
4 ffvelrn 5974 . . . . 5
5 elrege0 11684 . . . . . 6
65baib 911 . . . . 5
74, 6syl 17 . . . 4
87ralbidva 2796 . . 3
9 ffn 5684 . . . 4
10 ffnfv 6003 . . . . 5
1110baib 911 . . . 4
129, 11syl 17 . . 3
13 0cn 9581 . . . . . . 7
14 fnconstg 5726 . . . . . . 7
1513, 14ax-mp 5 . . . . . 6
16 df-0p 22565 . . . . . . 7
1716fneq1i 5626 . . . . . 6
1815, 17mpbir 212 . . . . 5
1918a1i 11 . . . 4
20 cnex 9566 . . . . 5
2120a1i 11 . . . 4
22 reex 9576 . . . . 5
2322a1i 11 . . . 4
24 ax-resscn 9542 . . . . 5
25 sseqin2 3619 . . . . 5
2624, 25mpbi 211 . . . 4
27 0pval 22566 . . . . 5
2827adantl 467 . . . 4
29 eqidd 2424 . . . 4
3019, 9, 21, 23, 26, 28, 29ofrfval 6492 . . 3
318, 12, 303bitr4d 288 . 2