Theorem 0le0 12353

Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
0le0	⊢ 0 ≤ 0

Proof of Theorem 0le0

Step	Hyp	Ref	Expression
1		0re 11221	. 2 ⊢ 0 ∈ ℝ
2	1	leidi 11759	1 ⊢ 0 ≤ 0

This proof depends on syntax axioms:   class class class wbr 5111  0cc0 11111   ≤ cle 11255

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-1cn 11169  ax-addrcl 11172  ax-rnegex 11182  ax-cnre 11184  ax-pre-lttri 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260

This theorem is used by:  nn0ledivnn  13142  xsubge0  13298  xmulge0  13321  0e0icopnf  13496  0e0iccpnf  13497  0elunit  13507  0mod  13948  sqlecan  14258  discr  14289  cnpart  15310  sqrt0  15311  resqrex  15320  sqrt00  15333  fsumabs  15871  rpnnen2lem4  16290  divalglem7  16474  pcmptdvds  16971  prmreclem4  16996  prmreclem5  16997  prmreclem6  16998  ramz2  17101  ramz  17102  isabvd  20944  prdsxmetlem  24554  metustto  24739  cfilucfil  24745  nmolb2d  24904  nmoi  24914  nmoix  24915  nmoleub  24917  nmo0  24921  pcoval1  25201  pco0  25202  minveclem7  25623  ovolfiniun  25689  ovolicc1  25704  ioorf  25761  itg1ge0a  25899  mbfi1fseqlem5  25907  itg2const  25928  itg2const2  25929  itg2splitlem  25936  itg2cnlem1  25949  itg2cnlem2  25950  iblss  25993  itgle  25998  ibladdlem  26008  iblabs  26017  iblabsr  26018  iblmulc2  26019  bddmulibl  26027  bddiblnc  26030  c1lip1  26185  dveq0  26188  dv11cn  26189  fta1g  26356  abelthlem2  26624  sinq12ge0  26702  cxpge0  26877  abscxp2  26887  log2ublem3  27142  chtwordi  27349  ppiwordi  27355  chpub  27413  bposlem1  27477  bposlem6  27482  dchrisum0flblem2  27702  qabvle  27818  ostth2lem2  27827  colinearalg  29289  eucrct2eupth  30625  ex-po  30815  nvz0  31049  nmlnoubi  31177  nmblolbii  31180  blocnilem  31185  siilem2  31233  minvecolem7  31264  pjneli  32104  nmbdoplbi  32405  nmcoplbi  32409  nmbdfnlbi  32430  nmcfnlbi  32433  nmopcoi  32476  unierri  32485  leoprf2  32508  leoprf  32509  stle0i  32620  fzo0opth  33177  m1pmeq  33898  xrge0iifcnv  34346  xrge0iifiso  34348  xrge0iifhom  34350  esumrnmpt2  34481  dstfrvclim1  34892  ballotlemrc  34945  signsply0  34962  chtvalz  35040  poimirlem23  38327  mblfinlem2  38342  itg2addnclem  38355  itg2gt0cn  38359  ibladdnclem  38360  itgaddnclem2  38363  iblabsnc  38368  iblmulc2nc  38369  ftc1anclem5  38381  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  areacirclem1  38392  areacirclem4  38395  mettrifi  38441  aks6d1c1  42916  bcled  42978  bcle2d  42979  readvrec2  43155  monotoddzzfi  43702  rmxypos  43707  rmygeid  43724  stoweidlem55  46802  fourierdlem14  46868  fourierdlem20  46874  fourierdlem92  46945  fourierdlem93  46946  fouriersw  46978  isomennd  47278  ovnssle  47308  hoidmvlelem3  47344  ovnhoilem1  47348  chnsubseqwl  47628  nnlog2ge0lt1  49379  dig1  49421  sepfsepc  49739  seppcld  49741  ex-gte  50540