Theorem 0le0 11110

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 10040	. 2 |- 0 e. RR
2	1	leidi 10562	1 |- 0 <_ 0

Syntax hints:   class class class wbr 4653   0cc0 9936   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  nn0ledivnn  11941  xsubge0  12091  xmulge0  12114  0e0icopnf  12282  0e0iccpnf  12283  0elunit  12290  0mod  12701  sqlecan  12971  discr  13001  cnpart  13980  sqr0lem  13981  resqrex  13991  sqrt00  14004  fsumabs  14533  rpnnen2lem4  14946  divalglem7  15122  pcmptdvds  15598  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  ramz2  15728  ramz  15729  isabvd  18820  prdsxmetlem  22173  metustto  22358  cfilucfil  22364  nmolb2d  22522  nmoi  22532  nmoix  22533  nmoleub  22535  nmo0  22539  pcoval1  22813  pco0  22814  minveclem7  23206  ovolfiniun  23269  ovolicc1  23284  ioorf  23341  itg1ge0a  23478  mbfi1fseqlem5  23486  itg2const  23507  itg2const2  23508  itg2splitlem  23515  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  itgle  23576  ibladdlem  23586  iblabs  23595  iblabsr  23596  iblmulc2  23597  bddmulibl  23605  c1lip1  23760  dveq0  23763  dv11cn  23764  fta1g  23927  abelthlem2  24186  sinq12ge0  24260  cxpge0  24429  abscxp2  24439  log2ublem3  24675  chtwordi  24882  ppiwordi  24888  chpub  24945  bposlem1  25009  bposlem6  25014  dchrisum0flblem2  25198  qabvle  25314  ostth2lem2  25323  colinearalg  25790  eucrct2eupth  27105  ex-po  27292  nvz0  27523  nmlnoubi  27651  nmblolbii  27654  blocnilem  27659  siilem2  27707  minvecolem7  27739  pjneli  28582  nmbdoplbi  28883  nmcoplbi  28887  nmbdfnlbi  28908  nmcfnlbi  28911  nmopcoi  28954  unierri  28963  leoprf2  28986  leoprf  28987  stle0i  29098  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  esumrnmpt2  30130  dstfrvclim1  30539  ballotlemrc  30592  signsply0  30628  chtvalz  30707  poimirlem23  33432  mblfinlem2  33447  itg2addnclem  33461  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem2  33469  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem1  33500  areacirclem4  33503  mettrifi  33553  monotoddzzfi  37507  rmxypos  37514  rmygeid  37531  stoweidlem55  40272  fourierdlem14  40338  fourierdlem20  40344  fourierdlem92  40415  fourierdlem93  40416  fouriersw  40448  isomennd  40745  ovnssle  40775  hoidmvlelem3  40811  ovnhoilem1  40815  nnlog2ge0lt1  42360  dig1  42402  ex-gte  42470