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

Theorem 0le0 10414
Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0le0  |-  0  <_  0

Proof of Theorem 0le0
StepHypRef Expression
1 0re 9389 . 2  |-  0  e.  RR
21leidi 9877 1  |-  0  <_  0
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4295   0cc0 9285    <_ cle 9422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6097  df-er 7104  df-en 7314  df-dom 7315  df-sdom 7316  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427
This theorem is referenced by:  xsubge0  11227  xmulge0  11250  0e0iccpnf  11399  0elunit  11406  0mod  11742  sqlecan  11975  discr  12004  hashle00  12161  cnpart  12732  sqr0lem  12733  resqrex  12743  sqr00  12756  fsumabs  13267  rpnnen2lem4  13503  divalglem7  13606  pcmptdvds  13959  prmreclem4  13983  prmreclem5  13984  prmreclem6  13985  ramz2  14088  ramz  14089  isabvd  16908  prdsxmetlem  19946  metusttoOLD  20135  metustto  20136  cfilucfilOLD  20147  cfilucfil  20148  nmolb2d  20300  nmoi  20310  nmoix  20311  nmoleub  20313  nmo0  20317  pcoval1  20588  pco0  20589  minveclem7  20925  ovolfiniun  20987  ovolicc1  21002  ioorf  21056  itg1ge0a  21192  mbfi1fseqlem5  21200  itg2const  21221  itg2const2  21222  itg2splitlem  21229  itg2cnlem1  21242  itg2cnlem2  21243  iblss  21285  itgle  21290  ibladdlem  21300  iblabs  21309  iblabsr  21310  iblmulc2  21311  bddmulibl  21319  c1lip1  21472  dveq0  21475  dv11cn  21476  fta1g  21642  abelthlem2  21900  sinq12ge0  21973  cxpge0  22131  abscxp2  22141  log2ublem3  22346  chtwordi  22497  ppiwordi  22503  chpub  22562  bposlem1  22626  bposlem6  22631  dchrisum0flblem2  22761  qabvle  22877  ostth2lem2  22886  colinearalg  23159  ex-po  23645  nvz0  24059  nmlnoubi  24199  nmblolbii  24202  blocnilem  24207  siilem2  24255  minvecolem7  24287  pjneli  25129  nmbdoplbi  25431  nmcoplbi  25435  nmbdfnlbi  25456  nmcfnlbi  25459  nmopcoi  25502  unierri  25511  leoprf2  25534  leoprf  25535  stle0i  25646  xrge0iifcnv  26366  xrge0iifiso  26368  xrge0iifhom  26370  dstfrvclim1  26863  ballotlemrc  26916  mblfinlem2  28432  itg2addnclem  28446  itg2gt0cn  28450  ibladdnclem  28451  itgaddnclem2  28454  iblabsnc  28459  iblmulc2nc  28460  bddiblnc  28465  ftc1anclem5  28474  ftc1anclem7  28476  ftc1anclem8  28477  ftc1anc  28478  areacirclem1  28487  areacirclem4  28490  mettrifi  28656  monotoddzzfi  29286  rmxypos  29293  rmygeid  29310  stoweidlem55  29853  ex-gte  31067
  Copyright terms: Public domain W3C validator