Theorem 0le0 12313

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

Syntax hints:   class class class wbr 5097  0cc0 11067   ≤ cle 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-addrcl 11128  ax-rnegex 11138  ax-cnre 11140  ax-pre-lttri 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216

This theorem is referenced by:  nn0ledivnn  13102  xsubge0  13258  xmulge0  13281  0e0icopnf  13456  0e0iccpnf  13457  0elunit  13467  0mod  13906  sqlecan  14216  discr  14247  cnpart  15258  sqrt0  15259  resqrex  15268  sqrt00  15281  fsumabs  15820  rpnnen2lem4  16240  divalglem7  16424  pcmptdvds  16921  prmreclem4  16946  prmreclem5  16947  prmreclem6  16948  ramz2  17051  ramz  17052  isabvd  20849  prdsxmetlem  24416  metustto  24601  cfilucfil  24607  nmolb2d  24766  nmoi  24776  nmoix  24777  nmoleub  24779  nmo0  24783  pcoval1  25063  pco0  25064  minveclem7  25485  ovolfiniun  25551  ovolicc1  25566  ioorf  25623  itg1ge0a  25761  mbfi1fseqlem5  25769  itg2const  25790  itg2const2  25791  itg2splitlem  25798  itg2cnlem1  25811  itg2cnlem2  25812  iblss  25855  itgle  25860  ibladdlem  25870  iblabs  25879  iblabsr  25880  iblmulc2  25881  bddmulibl  25889  bddiblnc  25892  c1lip1  26047  dveq0  26050  dv11cn  26051  fta1g  26218  abelthlem2  26483  sinq12ge0  26561  cxpge0  26736  abscxp2  26746  log2ublem3  27001  chtwordi  27208  ppiwordi  27214  chpub  27272  bposlem1  27336  bposlem6  27341  dchrisum0flblem2  27561  qabvle  27677  ostth2lem2  27686  colinearalg  29068  eucrct2eupth  30404  ex-po  30594  nvz0  30828  nmlnoubi  30956  nmblolbii  30959  blocnilem  30964  siilem2  31012  minvecolem7  31043  pjneli  31883  nmbdoplbi  32184  nmcoplbi  32188  nmbdfnlbi  32209  nmcfnlbi  32212  nmopcoi  32255  unierri  32264  leoprf2  32287  leoprf  32288  stle0i  32399  fzo0opth  32966  m1pmeq  33742  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  esumrnmpt2  34326  dstfrvclim1  34736  ballotlemrc  34789  signsply0  34806  chtvalz  34884  poimirlem23  38103  mblfinlem2  38118  itg2addnclem  38131  itg2gt0cn  38135  ibladdnclem  38136  itgaddnclem2  38139  iblabsnc  38144  iblmulc2nc  38145  ftc1anclem5  38157  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  areacirclem1  38168  areacirclem4  38171  mettrifi  38217  aks6d1c1  42694  bcled  42756  bcle2d  42757  readvrec2  42931  monotoddzzfi  43480  rmxypos  43485  rmygeid  43502  stoweidlem55  46590  fourierdlem14  46656  fourierdlem20  46662  fourierdlem92  46733  fourierdlem93  46734  fouriersw  46766  isomennd  47066  ovnssle  47096  hoidmvlelem3  47132  ovnhoilem1  47136  chnsubseqwl  47416  nnlog2ge0lt1  49149  dig1  49191  sepfsepc  49510  seppcld  49512  ex-gte  50311