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

Theorem 0plef 19567
 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 0re 9096 . . . 4
2 pnfxr 10718 . . . 4
3 icossre 10996 . . . 4
41, 2, 3mp2an 655 . . 3
5 fss 5602 . . 3
64, 5mpan2 654 . 2
7 ffvelrn 5871 . . . . 5
8 elrege0 11012 . . . . . 6
98baib 873 . . . . 5
107, 9syl 16 . . . 4
1110ralbidva 2723 . . 3
12 ffn 5594 . . . 4
13 ffnfv 5897 . . . . 5
1413baib 873 . . . 4
1512, 14syl 16 . . 3
16 0cn 9089 . . . . . . 7
17 fnconstg 5634 . . . . . . 7
1816, 17ax-mp 5 . . . . . 6
19 df-0p 19565 . . . . . . 7
2019fneq1i 5542 . . . . . 6
2118, 20mpbir 202 . . . . 5
2221a1i 11 . . . 4
23 cnex 9076 . . . . 5
2423a1i 11 . . . 4
25 reex 9086 . . . . 5
2625a1i 11 . . . 4
27 ax-resscn 9052 . . . . 5
28 sseqin2 3562 . . . . 5
2927, 28mpbi 201 . . . 4
30 0pval 19566 . . . . 5
3130adantl 454 . . . 4
32 eqidd 2439 . . . 4
3322, 12, 24, 26, 29, 31, 32ofrfval 6316 . . 3
3411, 15, 333bitr4d 278 . 2