Theorem nn0ge0d 12539

Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0ge0d	⊢ (𝜑 → 0 ≤ 𝐴)

Proof of Theorem nn0ge0d

Step	Hyp	Ref	Expression
1		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2		nn0ge0 12501	. 2 ⊢ (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5147  0cc0 11112   ≤ cle 11253  ℕ₀cn0 12476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477

This theorem is referenced by:  flmulnn0  13796  zmodfz  13862  modaddmodlo  13904  modsumfzodifsn  13913  addmodlteq  13915  expmulnbnd  14202  facwordi  14253  faclbnd  14254  faclbnd4lem3  14259  faclbnd6  14263  facavg  14265  hashdom  14343  climcnds  15801  geomulcvg  15826  mertenslem1  15834  eftabs  16023  efcllem  16025  efaddlem  16040  eftlub  16056  oexpneg  16292  divalg2  16352  bitsfzolem  16379  bitsmod  16381  sadcaddlem  16402  sadaddlem  16411  sadasslem  16415  sadeq  16417  smueqlem  16435  dfgcd2  16492  dvdssqlem  16507  nn0seqcvgd  16511  mulgcddvds  16596  isprm5  16648  zsqrtelqelz  16698  phibndlem  16707  dfphi2  16711  pythagtriplem3  16755  pythagtriplem10  16757  pythagtriplem6  16758  pythagtriplem7  16759  pythagtriplem12  16763  pythagtriplem14  16765  iserodd  16772  pcge0  16799  pcprmpw2  16819  pcmptdvds  16831  fldivp1  16834  pcbc  16837  qexpz  16838  pockthlem  16842  pockthg  16843  prmreclem3  16855  mul4sqlem  16890  4sqlem12  16893  4sqlem14  16895  4sqlem16  16897  0ram  16957  ram0  16959  ramcl  16966  prmolefac  16983  2expltfac  17030  odmodnn0  19449  pgpfi  19514  ablfac1c  19982  prmirred  21245  psrbaglesupp  21696  psrbaglesuppOLD  21697  psrbagcon  21702  psrbagconOLD  21703  psrlidm  21742  coe1tmmul2  22018  lebnumii  24712  mbfi1fseqlem1  25465  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  itg2cnlem2  25512  fta1g  25920  coemulhi  26003  dgradd2  26018  dgrco  26025  aareccl  26075  aaliou3lem8  26094  radcnvlem1  26161  dvradcnv  26169  dmlogdmgm  26764  wilthlem1  26808  sgmmul  26940  chtublem  26950  fsumvma2  26953  chpchtsum  26958  perfectlem2  26969  bcmono  27016  bposlem5  27027  lgsval2lem  27046  lgsval4a  27058  lgsqrlem2  27086  gausslemma2dlem0c  27097  gausslemma2dlem0d  27098  lgseisenlem1  27114  lgseisenlem2  27115  lgsquadlem1  27119  2lgslem1a1  27128  2sqlem3  27159  2sqlem7  27163  2sqlem8  27165  2sqblem  27170  2sqmod  27175  2sqreunnlem1  27188  dchrisum0re  27252  pntrlog2bndlem4  27319  pntpbnd1a  27324  ostth2lem2  27373  ostth2lem3  27374  ostth2  27376  crctcshwlkn0lem4  29334  wwlksubclwwlk  29578  nnmulge  32230  nndiffz1  32264  pfxlsw2ccat  32383  wrdt2ind  32384  submateqlem1  33085  nexple  33305  oddpwdc  33651  eulerpartlems  33657  eulerpartlemgc  33659  eulerpartlemb  33665  fsum2dsub  33917  breprexplemc  33942  circlemeth  33950  tgoldbachgtde  33970  usgrgt2cycl  34419  subfaclim  34477  cvmliftlem2  34575  cvmliftlem10  34583  snmlff  34618  dfgcd3  36508  poimirlem10  36801  poimirlem23  36814  poimirlem24  36815  itg2addnclem2  36843  rrnequiv  37006  bccl2d  41163  lcmineqlem18  41217  lcmineqlem19  41218  lcmineqlem20  41219  aks4d1p1p2  41241  aks4d1p1p7  41245  aks4d1p7d1  41253  2np3bcnp1  41266  sticksstones6  41273  sticksstones7  41274  sticksstones22  41290  metakunt2  41292  fltnlta  41707  irrapxlem2  41863  irrapxlem5  41866  pellexlem1  41869  pellexlem2  41870  pellexlem5  41873  pellexlem6  41874  pell14qrgt0  41899  pell1qrge1  41910  pellfundgt1  41923  rmspecnonsq  41947  rmspecfund  41949  rmspecpos  41957  rmxypos  41988  ltrmxnn0  41990  jm2.24  42004  acongeq  42024  jm2.22  42036  jm2.23  42037  jm2.27a  42046  jm2.27c  42048  nzprmdif  43380  bccbc  43406  binomcxplemnn0  43410  fsumnncl  44586  mccllem  44611  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnxpaek  44956  dvnmul  44957  dvnprodlem1  44960  stoweidlem24  45038  wallispilem4  45082  wallispilem5  45083  wallispi2lem1  45085  stirlinglem4  45091  stirlinglem5  45092  stirlinglem10  45097  stirlinglem15  45102  stirlingr  45104  fourierdlem48  45168  fourierdlem49  45169  fourierdlem92  45212  sqwvfoura  45242  elaa2lem  45247  etransclem19  45267  etransclem23  45271  etransclem27  45275  etransclem44  45292  rrndistlt  45304  oexpnegALTV  46643  perfectALTVlem2  46688  blennn  47348  dignn0ldlem  47375  dig2nn1st  47378  digexp  47380  dignn0flhalf  47391  itcovalt2lem2lem1  47446