![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0le0 | Structured version Visualization version GIF version |
Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
0le0 | ⊢ 0 ≤ 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 11260 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | leidi 11794 | 1 ⊢ 0 ≤ 0 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5147 0cc0 11152 ≤ cle 11293 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-resscn 11209 ax-1cn 11210 ax-addrcl 11213 ax-rnegex 11223 ax-cnre 11225 ax-pre-lttri 11226 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 |
This theorem is referenced by: nn0ledivnn 13145 xsubge0 13299 xmulge0 13322 0e0icopnf 13494 0e0iccpnf 13495 0elunit 13505 0mod 13938 sqlecan 14244 discr 14275 cnpart 15275 sqrt0 15276 resqrex 15285 sqrt00 15298 fsumabs 15833 rpnnen2lem4 16249 divalglem7 16432 pcmptdvds 16927 prmreclem4 16952 prmreclem5 16953 prmreclem6 16954 ramz2 17057 ramz 17058 isabvd 20829 prdsxmetlem 24393 metustto 24581 cfilucfil 24587 nmolb2d 24754 nmoi 24764 nmoix 24765 nmoleub 24767 nmo0 24771 pcoval1 25059 pco0 25060 minveclem7 25482 ovolfiniun 25549 ovolicc1 25564 ioorf 25621 itg1ge0a 25760 mbfi1fseqlem5 25768 itg2const 25789 itg2const2 25790 itg2splitlem 25797 itg2cnlem1 25810 itg2cnlem2 25811 iblss 25854 itgle 25859 ibladdlem 25869 iblabs 25878 iblabsr 25879 iblmulc2 25880 bddmulibl 25888 bddiblnc 25891 c1lip1 26050 dveq0 26053 dv11cn 26054 fta1g 26223 abelthlem2 26490 sinq12ge0 26564 cxpge0 26739 abscxp2 26749 log2ublem3 27005 chtwordi 27213 ppiwordi 27219 chpub 27278 bposlem1 27342 bposlem6 27347 dchrisum0flblem2 27567 qabvle 27683 ostth2lem2 27692 colinearalg 28939 eucrct2eupth 30273 ex-po 30463 nvz0 30696 nmlnoubi 30824 nmblolbii 30827 blocnilem 30832 siilem2 30880 minvecolem7 30911 pjneli 31751 nmbdoplbi 32052 nmcoplbi 32056 nmbdfnlbi 32077 nmcfnlbi 32080 nmopcoi 32123 unierri 32132 leoprf2 32155 leoprf 32156 stle0i 32267 fzo0opth 32812 m1pmeq 33587 xrge0iifcnv 33893 xrge0iifiso 33895 xrge0iifhom 33897 esumrnmpt2 34048 dstfrvclim1 34458 ballotlemrc 34511 signsply0 34544 chtvalz 34622 poimirlem23 37629 mblfinlem2 37644 itg2addnclem 37657 itg2gt0cn 37661 ibladdnclem 37662 itgaddnclem2 37665 iblabsnc 37670 iblmulc2nc 37671 ftc1anclem5 37683 ftc1anclem7 37685 ftc1anclem8 37686 ftc1anc 37687 areacirclem1 37694 areacirclem4 37697 mettrifi 37743 aks6d1c1 42097 bcled 42159 bcle2d 42160 readvrec2 42369 monotoddzzfi 42930 rmxypos 42935 rmygeid 42952 stoweidlem55 46010 fourierdlem14 46076 fourierdlem20 46082 fourierdlem92 46153 fourierdlem93 46154 fouriersw 46186 isomennd 46486 ovnssle 46516 hoidmvlelem3 46552 ovnhoilem1 46556 nnlog2ge0lt1 48415 dig1 48457 sepfsepc 48723 seppcld 48725 ex-gte 48959 |
Copyright terms: Public domain | W3C validator |