Theorem nn0ge0d 12565

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 12526	. 2 ⊢ (𝐴 ∈ ℕ0 → 0 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  0cc0 11129   ≤ cle 11270  ℕ₀cn0 12501

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-nn 12241  df-n0 12502

This theorem is referenced by:  flmulnn0  13844  zmodfz  13910  modaddmodlo  13953  modsumfzodifsn  13962  addmodlteq  13964  expmulnbnd  14253  facwordi  14307  faclbnd  14308  faclbnd4lem3  14313  faclbnd6  14317  facavg  14319  hashdom  14397  climcnds  15867  geomulcvg  15892  mertenslem1  15900  eftabs  16091  efcllem  16093  efaddlem  16109  eftlub  16127  oexpneg  16364  divalg2  16424  bitsfzolem  16453  bitsmod  16455  sadcaddlem  16476  sadaddlem  16485  sadasslem  16489  sadeq  16491  smueqlem  16509  dfgcd2  16565  dvdssqlem  16585  nn0seqcvgd  16589  mulgcddvds  16674  isprm5  16726  zsqrtelqelz  16777  phibndlem  16789  dfphi2  16793  pythagtriplem3  16838  pythagtriplem10  16840  pythagtriplem6  16841  pythagtriplem7  16842  pythagtriplem12  16846  pythagtriplem14  16848  iserodd  16855  pcge0  16882  pcprmpw2  16902  pcmptdvds  16914  fldivp1  16917  pcbc  16920  qexpz  16921  pockthlem  16925  pockthg  16926  prmreclem3  16938  mul4sqlem  16973  4sqlem12  16976  4sqlem14  16978  4sqlem16  16980  0ram  17040  ram0  17042  ramcl  17049  prmolefac  17066  2expltfac  17112  odmodnn0  19521  pgpfi  19586  ablfac1c  20054  prmirred  21435  psrbaglesupp  21882  psrbagcon  21885  psrlidm  21922  psdmul  22104  coe1tmmul2  22213  lebnumii  24916  mbfi1fseqlem1  25668  mbfi1fseqlem3  25670  mbfi1fseqlem4  25671  mbfi1fseqlem5  25672  itg2cnlem2  25715  fta1g  26127  coemulhi  26211  dgradd2  26226  dgrco  26233  aareccl  26286  aaliou3lem8  26305  radcnvlem1  26374  dvradcnv  26382  dmlogdmgm  26986  wilthlem1  27030  sgmmul  27164  chtublem  27174  fsumvma2  27177  chpchtsum  27182  perfectlem2  27193  bcmono  27240  bposlem5  27251  lgsval2lem  27270  lgsval4a  27282  lgsqrlem2  27310  gausslemma2dlem0c  27321  gausslemma2dlem0d  27322  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  2lgslem1a1  27352  2sqlem3  27383  2sqlem7  27387  2sqlem8  27389  2sqblem  27394  2sqmod  27399  2sqreunnlem1  27412  dchrisum0re  27476  pntrlog2bndlem4  27543  pntpbnd1a  27548  ostth2lem2  27597  ostth2lem3  27598  ostth2  27600  crctcshwlkn0lem4  29795  wwlksubclwwlk  30039  nnmulge  32716  nndiffz1  32763  fzo0opth  32782  nexple  32823  pfxlsw2ccat  32926  wrdt2ind  32929  gsumwrd2dccatlem  33060  ply1unit  33588  constrdircl  33799  iconstr  33800  submateqlem1  33838  oddpwdc  34386  eulerpartlems  34392  eulerpartlemgc  34394  eulerpartlemb  34400  fsum2dsub  34639  breprexplemc  34664  circlemeth  34672  tgoldbachgtde  34692  usgrgt2cycl  35152  subfaclim  35210  cvmliftlem2  35308  cvmliftlem10  35316  snmlff  35351  dfgcd3  37342  poimirlem10  37654  poimirlem23  37667  poimirlem24  37668  itg2addnclem2  37696  rrnequiv  37859  bccl2d  42004  lcmineqlem18  42059  lcmineqlem19  42060  lcmineqlem20  42061  aks4d1p1p2  42083  aks4d1p1p7  42087  aks4d1p7d1  42095  posbezout  42113  aks6d1c1  42129  aks6d1c2lem4  42140  aks6d1c2  42143  deg1gprod  42153  2np3bcnp1  42157  sticksstones6  42164  sticksstones7  42165  sticksstones22  42181  aks6d1c6lem3  42185  aks6d1c6lem4  42186  bcled  42191  bcle2d  42192  aks6d1c7lem1  42193  aks6d1c7lem2  42194  unitscyglem4  42211  metakunt2  42219  fltnlta  42686  irrapxlem2  42846  irrapxlem5  42849  pellexlem1  42852  pellexlem2  42853  pellexlem5  42856  pellexlem6  42857  pell14qrgt0  42882  pell1qrge1  42893  pellfundgt1  42906  rmspecnonsq  42930  rmspecfund  42932  rmspecpos  42940  rmxypos  42971  ltrmxnn0  42973  jm2.24  42987  acongeq  43007  jm2.22  43019  jm2.23  43020  jm2.27a  43029  jm2.27c  43031  nzprmdif  44343  bccbc  44369  binomcxplemnn0  44373  fsumnncl  45601  mccllem  45626  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  dvnxpaek  45971  dvnmul  45972  dvnprodlem1  45975  stoweidlem24  46053  wallispilem4  46097  wallispilem5  46098  wallispi2lem1  46100  stirlinglem4  46106  stirlinglem5  46107  stirlinglem10  46112  stirlinglem15  46117  stirlingr  46119  fourierdlem48  46183  fourierdlem49  46184  fourierdlem92  46227  sqwvfoura  46257  elaa2lem  46262  etransclem19  46282  etransclem23  46286  etransclem27  46290  etransclem44  46307  rrndistlt  46319  oexpnegALTV  47691  perfectALTVlem2  47736  gpgedgvtx0  48065  gpgedgvtx1  48066  blennn  48555  dignn0ldlem  48582  dig2nn1st  48585  digexp  48587  dignn0flhalf  48598  itcovalt2lem2lem1  48653