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 10645 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | leidi 11176 | 1 ⊢ 0 ≤ 0 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5068 0cc0 10539 ≤ cle 10678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-resscn 10596 ax-1cn 10597 ax-addrcl 10600 ax-rnegex 10610 ax-cnre 10612 ax-pre-lttri 10613 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 |
This theorem is referenced by: nn0ledivnn 12505 xsubge0 12657 xmulge0 12680 0e0icopnf 12849 0e0iccpnf 12850 0elunit 12858 0mod 13273 sqlecan 13574 discr 13604 cnpart 14601 sqr0lem 14602 resqrex 14612 sqrt00 14625 fsumabs 15158 rpnnen2lem4 15572 divalglem7 15752 pcmptdvds 16232 prmreclem4 16257 prmreclem5 16258 prmreclem6 16259 ramz2 16362 ramz 16363 isabvd 19593 prdsxmetlem 22980 metustto 23165 cfilucfil 23171 nmolb2d 23329 nmoi 23339 nmoix 23340 nmoleub 23342 nmo0 23346 pcoval1 23619 pco0 23620 minveclem7 24040 ovolfiniun 24104 ovolicc1 24119 ioorf 24176 itg1ge0a 24314 mbfi1fseqlem5 24322 itg2const 24343 itg2const2 24344 itg2splitlem 24351 itg2cnlem1 24364 itg2cnlem2 24365 iblss 24407 itgle 24412 ibladdlem 24422 iblabs 24431 iblabsr 24432 iblmulc2 24433 bddmulibl 24441 c1lip1 24596 dveq0 24599 dv11cn 24600 fta1g 24763 abelthlem2 25022 sinq12ge0 25096 cxpge0 25268 abscxp2 25278 log2ublem3 25528 chtwordi 25735 ppiwordi 25741 chpub 25798 bposlem1 25862 bposlem6 25867 dchrisum0flblem2 26087 qabvle 26203 ostth2lem2 26212 colinearalg 26698 eucrct2eupth 28026 ex-po 28216 nvz0 28447 nmlnoubi 28575 nmblolbii 28578 blocnilem 28583 siilem2 28631 minvecolem7 28662 pjneli 29502 nmbdoplbi 29803 nmcoplbi 29807 nmbdfnlbi 29828 nmcfnlbi 29831 nmopcoi 29874 unierri 29883 leoprf2 29906 leoprf 29907 stle0i 30018 xrge0iifcnv 31178 xrge0iifiso 31180 xrge0iifhom 31182 esumrnmpt2 31329 dstfrvclim1 31737 ballotlemrc 31790 signsply0 31823 chtvalz 31902 poimirlem23 34917 mblfinlem2 34932 itg2addnclem 34945 itg2gt0cn 34949 ibladdnclem 34950 itgaddnclem2 34953 iblabsnc 34958 iblmulc2nc 34959 bddiblnc 34964 ftc1anclem5 34973 ftc1anclem7 34975 ftc1anclem8 34976 ftc1anc 34977 areacirclem1 34984 areacirclem4 34987 mettrifi 35034 monotoddzzfi 39546 rmxypos 39551 rmygeid 39568 stoweidlem55 42347 fourierdlem14 42413 fourierdlem20 42419 fourierdlem92 42490 fourierdlem93 42491 fouriersw 42523 isomennd 42820 ovnssle 42850 hoidmvlelem3 42886 ovnhoilem1 42890 nnlog2ge0lt1 44633 dig1 44675 ex-gte 44835 |
Copyright terms: Public domain | W3C validator |