Theorem 0le0 12366

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 11234	. 2 ⊢ 0 ∈ ℝ
2	1	leidi 11772	1 ⊢ 0 ≤ 0

This proof depends on syntax axioms:   class class class wbr 5103  0cc0 11124   ≤ cle 11268

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-addrcl 11185  ax-rnegex 11195  ax-cnre 11197  ax-pre-lttri 11198

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  nn0ledivnn  13157  xsubge0  13313  xmulge0  13336  0e0icopnf  13511  0e0iccpnf  13512  0elunit  13522  0mod  13963  sqlecan  14273  discr  14304  cnpart  15327  sqrt0  15328  resqrex  15337  sqrt00  15350  fsumabs  15888  rpnnen2lem4  16305  divalglem7  16489  pcmptdvds  16986  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  ramz2  17116  ramz  17117  isabvd  20978  prdsxmetlem  24594  metustto  24779  cfilucfil  24785  nmolb2d  24944  nmoi  24954  nmoix  24955  nmoleub  24957  nmo0  24961  pcoval1  25241  pco0  25242  minveclem7  25663  ovolfiniun  25729  ovolicc1  25744  ioorf  25801  itg1ge0a  25939  mbfi1fseqlem5  25947  itg2const  25968  itg2const2  25969  itg2splitlem  25976  itg2cnlem1  25989  itg2cnlem2  25990  iblss  26032  itgle  26037  ibladdlem  26047  iblabs  26056  iblabsr  26057  iblmulc2  26058  bddmulibl  26066  bddiblnc  26069  c1lip1  26224  dveq0  26227  dv11cn  26228  fta1g  26395  abelthlem2  26668  sinq12ge0  26746  cxpge0  26920  abscxp2  26930  log2ublem3  27185  chtwordi  27392  ppiwordi  27398  chpub  27456  bposlem1  27520  bposlem6  27525  dchrisum0flblem2  27745  qabvle  27861  ostth2lem2  27870  colinearalg  29367  eucrct2eupth  30725  ex-po  30915  nvz0  31149  nmlnoubi  31277  nmblolbii  31280  blocnilem  31285  siilem2  31333  minvecolem7  31364  pjneli  32204  nmbdoplbi  32505  nmcoplbi  32509  nmbdfnlbi  32530  nmcfnlbi  32533  nmopcoi  32576  unierri  32585  leoprf2  32608  leoprf  32609  stle0i  32720  fzo0opth  33274  m1pmeq  33995  xrge0iifcnv  34443  xrge0iifiso  34445  xrge0iifhom  34447  esumrnmpt2  34578  dstfrvclim1  34989  ballotlemrc  35042  signsply0  35059  chtvalz  35137  poimirlem23  38392  mblfinlem2  38407  itg2addnclem  38420  itg2gt0cn  38424  ibladdnclem  38425  itgaddnclem2  38428  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  areacirclem1  38457  areacirclem4  38460  mettrifi  38507  aks6d1c1  42982  bcled  43044  bcle2d  43045  readvrec2  43236  monotoddzzfi  43783  rmxypos  43788  rmygeid  43805  stoweidlem55  46883  fourierdlem14  46949  fourierdlem20  46955  fourierdlem92  47026  fourierdlem93  47027  fouriersw  47059  isomennd  47359  ovnssle  47389  hoidmvlelem3  47425  ovnhoilem1  47429  chnsubseqwl  47707  nnlog2ge0lt1  49496  dig1  49538  sepfsepc  49854  seppcld  49856  ex-gte  50655