Theorem 0le0 12237

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

Syntax hints:   class class class wbr 5095  0cc0 11017   ≤ cle 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-addrcl 11078  ax-rnegex 11088  ax-cnre 11090  ax-pre-lttri 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163

This theorem is referenced by:  nn0ledivnn  13011  xsubge0  13167  xmulge0  13190  0e0icopnf  13365  0e0iccpnf  13366  0elunit  13376  0mod  13813  sqlecan  14123  discr  14154  cnpart  15154  sqrt0  15155  resqrex  15164  sqrt00  15177  fsumabs  15715  rpnnen2lem4  16133  divalglem7  16317  pcmptdvds  16813  prmreclem4  16838  prmreclem5  16839  prmreclem6  16840  ramz2  16943  ramz  16944  isabvd  20736  prdsxmetlem  24303  metustto  24488  cfilucfil  24494  nmolb2d  24653  nmoi  24663  nmoix  24664  nmoleub  24666  nmo0  24670  pcoval1  24960  pco0  24961  minveclem7  25382  ovolfiniun  25449  ovolicc1  25464  ioorf  25521  itg1ge0a  25659  mbfi1fseqlem5  25667  itg2const  25688  itg2const2  25689  itg2splitlem  25696  itg2cnlem1  25709  itg2cnlem2  25710  iblss  25753  itgle  25758  ibladdlem  25768  iblabs  25777  iblabsr  25778  iblmulc2  25779  bddmulibl  25787  bddiblnc  25790  c1lip1  25949  dveq0  25952  dv11cn  25953  fta1g  26122  abelthlem2  26389  sinq12ge0  26464  cxpge0  26639  abscxp2  26649  log2ublem3  26905  chtwordi  27113  ppiwordi  27119  chpub  27178  bposlem1  27242  bposlem6  27247  dchrisum0flblem2  27467  qabvle  27583  ostth2lem2  27592  colinearalg  28909  eucrct2eupth  30246  ex-po  30436  nvz0  30669  nmlnoubi  30797  nmblolbii  30800  blocnilem  30805  siilem2  30853  minvecolem7  30884  pjneli  31724  nmbdoplbi  32025  nmcoplbi  32029  nmbdfnlbi  32050  nmcfnlbi  32053  nmopcoi  32096  unierri  32105  leoprf2  32128  leoprf  32129  stle0i  32240  fzo0opth  32811  m1pmeq  33594  xrge0iifcnv  34018  xrge0iifiso  34020  xrge0iifhom  34022  esumrnmpt2  34153  dstfrvclim1  34563  ballotlemrc  34616  signsply0  34636  chtvalz  34714  poimirlem23  37756  mblfinlem2  37771  itg2addnclem  37784  itg2gt0cn  37788  ibladdnclem  37789  itgaddnclem2  37792  iblabsnc  37797  iblmulc2nc  37798  ftc1anclem5  37810  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  areacirclem1  37821  areacirclem4  37824  mettrifi  37870  aks6d1c1  42282  bcled  42344  bcle2d  42345  readvrec2  42531  monotoddzzfi  43099  rmxypos  43104  rmygeid  43121  stoweidlem55  46215  fourierdlem14  46281  fourierdlem20  46287  fourierdlem92  46358  fourierdlem93  46359  fouriersw  46391  isomennd  46691  ovnssle  46721  hoidmvlelem3  46757  ovnhoilem1  46761  chnsubseqwl  47039  nnlog2ge0lt1  48728  dig1  48770  sepfsepc  49089  seppcld  49091  ex-gte  49890