Theorem 0le0 12343

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

Syntax hints:   class class class wbr 5110  0cc0 11101   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174  ax-pre-lttri 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  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 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  nn0ledivnn  13132  xsubge0  13288  xmulge0  13311  0e0icopnf  13486  0e0iccpnf  13487  0elunit  13497  0mod  13937  sqlecan  14247  discr  14278  cnpart  15293  sqrt0  15294  resqrex  15303  sqrt00  15316  fsumabs  15855  rpnnen2lem4  16274  divalglem7  16458  pcmptdvds  16955  prmreclem4  16980  prmreclem5  16981  prmreclem6  16982  ramz2  17085  ramz  17086  isabvd  20896  prdsxmetlem  24506  metustto  24691  cfilucfil  24697  nmolb2d  24856  nmoi  24866  nmoix  24867  nmoleub  24869  nmo0  24873  pcoval1  25153  pco0  25154  minveclem7  25575  ovolfiniun  25641  ovolicc1  25656  ioorf  25713  itg1ge0a  25851  mbfi1fseqlem5  25859  itg2const  25880  itg2const2  25881  itg2splitlem  25888  itg2cnlem1  25901  itg2cnlem2  25902  iblss  25945  itgle  25950  ibladdlem  25960  iblabs  25969  iblabsr  25970  iblmulc2  25971  bddmulibl  25979  bddiblnc  25982  c1lip1  26137  dveq0  26140  dv11cn  26141  fta1g  26308  abelthlem2  26576  sinq12ge0  26654  cxpge0  26829  abscxp2  26839  log2ublem3  27094  chtwordi  27301  ppiwordi  27307  chpub  27365  bposlem1  27429  bposlem6  27434  dchrisum0flblem2  27654  qabvle  27770  ostth2lem2  27779  colinearalg  29241  eucrct2eupth  30577  ex-po  30767  nvz0  31001  nmlnoubi  31129  nmblolbii  31132  blocnilem  31137  siilem2  31185  minvecolem7  31216  pjneli  32056  nmbdoplbi  32357  nmcoplbi  32361  nmbdfnlbi  32382  nmcfnlbi  32385  nmopcoi  32428  unierri  32437  leoprf2  32460  leoprf  32461  stle0i  32572  fzo0opth  33129  m1pmeq  33856  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  esumrnmpt2  34439  dstfrvclim1  34849  ballotlemrc  34902  signsply0  34919  chtvalz  34997  poimirlem23  38275  mblfinlem2  38290  itg2addnclem  38303  itg2gt0cn  38307  ibladdnclem  38308  itgaddnclem2  38311  iblabsnc  38316  iblmulc2nc  38317  ftc1anclem5  38329  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  areacirclem1  38340  areacirclem4  38343  mettrifi  38389  aks6d1c1  42864  bcled  42926  bcle2d  42927  readvrec2  43103  monotoddzzfi  43652  rmxypos  43657  rmygeid  43674  stoweidlem55  46752  fourierdlem14  46818  fourierdlem20  46824  fourierdlem92  46895  fourierdlem93  46896  fouriersw  46928  isomennd  47228  ovnssle  47258  hoidmvlelem3  47294  ovnhoilem1  47298  chnsubseqwl  47578  nnlog2ge0lt1  49329  dig1  49371  sepfsepc  49689  seppcld  49691  ex-gte  50490