Theorem nn0ge0d 12545

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  0cc0 11073   ≤ cle 11217  ℕ₀cn0 12481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482

This theorem is referenced by:  flmulnn0  13837  zmodfz  13903  modaddmodlo  13948  modsumfzodifsn  13957  addmodlteq  13959  expmulnbnd  14248  facwordi  14302  faclbnd  14303  faclbnd4lem3  14308  faclbnd6  14312  facavg  14314  hashdom  14392  climcnds  15881  geomulcvg  15906  mertenslem1  15914  eftabs  16105  efcllem  16107  efaddlem  16123  eftlub  16141  oexpneg  16379  divalg2  16439  bitsfzolem  16468  bitsmod  16470  sadcaddlem  16491  sadaddlem  16500  sadasslem  16504  sadeq  16506  smueqlem  16524  dfgcd2  16580  dvdssqlem  16600  nn0seqcvgd  16604  mulgcddvds  16689  isprm5  16742  zsqrtelqelz  16793  phibndlem  16805  dfphi2  16809  pythagtriplem3  16854  pythagtriplem10  16856  pythagtriplem6  16857  pythagtriplem7  16858  pythagtriplem12  16862  pythagtriplem14  16864  iserodd  16871  pcge0  16898  pcprmpw2  16918  pcmptdvds  16930  fldivp1  16933  pcbc  16936  qexpz  16937  pockthlem  16941  pockthg  16942  prmreclem3  16954  mul4sqlem  16989  4sqlem12  16992  4sqlem14  16994  4sqlem16  16996  0ram  17056  ram0  17058  ramcl  17065  prmolefac  17082  2expltfac  17128  odmodnn0  19580  pgpfi  19645  ablfac1c  20113  prmirred  21523  psrbaglesupp  21971  psrbagcon  21974  psrlidm  22010  psdmul  22228  coe1tmmul2  22336  lebnumii  25025  mbfi1fseqlem1  25774  mbfi1fseqlem3  25776  mbfi1fseqlem4  25777  mbfi1fseqlem5  25778  itg2cnlem2  25821  fta1g  26227  coemulhi  26311  dgradd2  26325  dgrco  26332  aareccl  26387  aaliou3lem8  26406  radcnvlem1  26473  dvradcnv  26481  dmlogdmgm  27085  wilthlem1  27129  sgmmul  27262  chtublem  27272  fsumvma2  27275  chpchtsum  27280  perfectlem2  27291  bcmono  27338  bposlem5  27349  lgsval2lem  27368  lgsval4a  27380  lgsqrlem2  27408  gausslemma2dlem0c  27419  gausslemma2dlem0d  27420  lgseisenlem1  27436  lgseisenlem2  27437  lgsquadlem1  27441  2lgslem1a1  27450  2sqlem3  27481  2sqlem7  27485  2sqlem8  27487  2sqblem  27492  2sqmod  27497  2sqreunnlem1  27510  dchrisum0re  27574  pntrlog2bndlem4  27641  pntpbnd1a  27646  ostth2lem2  27695  ostth2lem3  27696  ostth2  27698  crctcshwlkn0lem4  30010  wwlksubclwwlk  30257  nnmulge  32938  nndiffz1  32985  fzo0opth  33002  nexple  33032  pfxlsw2ccat  33125  wrdt2ind  33128  gsumwrd2dccatlem  33254  ply1unit  33768  selvply1rhmlemb  33813  mplmulmvr  33833  esplyind  33869  constrdircl  34059  iconstr  34060  submateqlem1  34101  oddpwdc  34648  eulerpartlems  34654  eulerpartlemgc  34656  eulerpartlemb  34662  fsum2dsub  34898  breprexplemc  34923  circlemeth  34931  tgoldbachgtde  34951  usgrgt2cycl  35477  subfaclim  35535  cvmliftlem2  35633  cvmliftlem10  35641  snmlff  35676  dfgcd3  37813  poimirlem10  38126  poimirlem23  38139  poimirlem24  38140  itg2addnclem2  38168  rrnequiv  38331  bccl2d  42605  lcmineqlem18  42660  lcmineqlem19  42661  lcmineqlem20  42662  aks4d1p1p2  42684  aks4d1p1p7  42688  aks4d1p7d1  42696  posbezout  42714  aks6d1c1  42730  aks6d1c2lem4  42741  aks6d1c2  42744  deg1gprod  42754  2np3bcnp1  42758  sticksstones6  42765  sticksstones7  42766  sticksstones22  42782  aks6d1c6lem3  42786  aks6d1c6lem4  42787  bcled  42792  bcle2d  42793  aks6d1c7lem1  42794  aks6d1c7lem2  42795  unitscyglem4  42812  fltnlta  43242  irrapxlem2  43397  irrapxlem5  43400  pellexlem1  43403  pellexlem2  43404  pellexlem5  43407  pellexlem6  43408  pell14qrgt0  43433  pell1qrge1  43444  pellfundgt1  43457  rmspecnonsq  43481  rmspecfund  43483  rmspecpos  43490  rmxypos  43521  ltrmxnn0  43523  jm2.24  43537  acongeq  43557  jm2.22  43569  jm2.23  43570  jm2.27a  43579  jm2.27c  43581  nzprmdif  44892  bccbc  44918  binomcxplemnn0  44922  fsumnncl  46145  mccllem  46170  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  dvnxpaek  46513  dvnmul  46514  dvnprodlem1  46517  stoweidlem24  46595  wallispilem4  46639  wallispilem5  46640  wallispi2lem1  46642  stirlinglem4  46648  stirlinglem5  46649  stirlinglem10  46654  stirlinglem15  46659  stirlingr  46661  fourierdlem48  46725  fourierdlem49  46726  fourierdlem92  46769  sqwvfoura  46799  elaa2lem  46804  etransclem19  46824  etransclem23  46828  etransclem27  46832  etransclem44  46849  rrndistlt  46861  chnsubseqwl  47452  modlt0b  47960  oexpnegALTV  48296  perfectALTVlem2  48341  gpgedgvtx0  48680  gpgedgvtx1  48681  blennn  49194  dignn0ldlem  49221  dig2nn1st  49224  digexp  49226  dignn0flhalf  49237  itcovalt2lem2lem1  49292