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 10832 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | leidi 11363 | 1 ⊢ 0 ≤ 0 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5050 0cc0 10726 ≤ cle 10865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pow 5255 ax-pr 5319 ax-un 7520 ax-resscn 10783 ax-1cn 10784 ax-addrcl 10787 ax-rnegex 10797 ax-cnre 10799 ax-pre-lttri 10800 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-nel 3044 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-sbc 3692 df-csb 3809 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-opab 5113 df-mpt 5133 df-id 5452 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-er 8388 df-en 8624 df-dom 8625 df-sdom 8626 df-pnf 10866 df-mnf 10867 df-xr 10868 df-ltxr 10869 df-le 10870 |
This theorem is referenced by: nn0ledivnn 12696 xsubge0 12848 xmulge0 12871 0e0icopnf 13043 0e0iccpnf 13044 0elunit 13054 0mod 13472 sqlecan 13774 discr 13804 cnpart 14800 sqr0lem 14801 resqrex 14811 sqrt00 14824 fsumabs 15362 rpnnen2lem4 15775 divalglem7 15957 pcmptdvds 16444 prmreclem4 16469 prmreclem5 16470 prmreclem6 16471 ramz2 16574 ramz 16575 isabvd 19853 prdsxmetlem 23263 metustto 23448 cfilucfil 23454 nmolb2d 23613 nmoi 23623 nmoix 23624 nmoleub 23626 nmo0 23630 pcoval1 23907 pco0 23908 minveclem7 24329 ovolfiniun 24395 ovolicc1 24410 ioorf 24467 itg1ge0a 24606 mbfi1fseqlem5 24614 itg2const 24635 itg2const2 24636 itg2splitlem 24643 itg2cnlem1 24656 itg2cnlem2 24657 iblss 24699 itgle 24704 ibladdlem 24714 iblabs 24723 iblabsr 24724 iblmulc2 24725 bddmulibl 24733 bddiblnc 24736 c1lip1 24891 dveq0 24894 dv11cn 24895 fta1g 25062 abelthlem2 25321 sinq12ge0 25395 cxpge0 25568 abscxp2 25578 log2ublem3 25828 chtwordi 26035 ppiwordi 26041 chpub 26098 bposlem1 26162 bposlem6 26167 dchrisum0flblem2 26387 qabvle 26503 ostth2lem2 26512 colinearalg 26998 eucrct2eupth 28325 ex-po 28515 nvz0 28746 nmlnoubi 28874 nmblolbii 28877 blocnilem 28882 siilem2 28930 minvecolem7 28961 pjneli 29801 nmbdoplbi 30102 nmcoplbi 30106 nmbdfnlbi 30127 nmcfnlbi 30130 nmopcoi 30173 unierri 30182 leoprf2 30205 leoprf 30206 stle0i 30317 xrge0iifcnv 31594 xrge0iifiso 31596 xrge0iifhom 31598 esumrnmpt2 31745 dstfrvclim1 32153 ballotlemrc 32206 signsply0 32239 chtvalz 32318 poimirlem23 35535 mblfinlem2 35550 itg2addnclem 35563 itg2gt0cn 35567 ibladdnclem 35568 itgaddnclem2 35571 iblabsnc 35576 iblmulc2nc 35577 ftc1anclem5 35589 ftc1anclem7 35591 ftc1anclem8 35592 ftc1anc 35593 areacirclem1 35600 areacirclem4 35603 mettrifi 35650 monotoddzzfi 40465 rmxypos 40470 rmygeid 40487 stoweidlem55 43269 fourierdlem14 43335 fourierdlem20 43341 fourierdlem92 43412 fourierdlem93 43413 fouriersw 43445 isomennd 43742 ovnssle 43772 hoidmvlelem3 43808 ovnhoilem1 43812 nnlog2ge0lt1 45583 dig1 45625 sepfsepc 45892 seppcld 45894 ex-gte 46100 |
Copyright terms: Public domain | W3C validator |