Theorem nn0ge0d 12445

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  0cc0 11006   ≤ cle 11147  ℕ₀cn0 12381

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-n0 12382

This theorem is referenced by:  flmulnn0  13731  zmodfz  13797  modaddmodlo  13842  modsumfzodifsn  13851  addmodlteq  13853  expmulnbnd  14142  facwordi  14196  faclbnd  14197  faclbnd4lem3  14202  faclbnd6  14206  facavg  14208  hashdom  14286  climcnds  15758  geomulcvg  15783  mertenslem1  15791  eftabs  15982  efcllem  15984  efaddlem  16000  eftlub  16018  oexpneg  16256  divalg2  16316  bitsfzolem  16345  bitsmod  16347  sadcaddlem  16368  sadaddlem  16377  sadasslem  16381  sadeq  16383  smueqlem  16401  dfgcd2  16457  dvdssqlem  16477  nn0seqcvgd  16481  mulgcddvds  16566  isprm5  16618  zsqrtelqelz  16669  phibndlem  16681  dfphi2  16685  pythagtriplem3  16730  pythagtriplem10  16732  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem12  16738  pythagtriplem14  16740  iserodd  16747  pcge0  16774  pcprmpw2  16794  pcmptdvds  16806  fldivp1  16809  pcbc  16812  qexpz  16813  pockthlem  16817  pockthg  16818  prmreclem3  16830  mul4sqlem  16865  4sqlem12  16868  4sqlem14  16870  4sqlem16  16872  0ram  16932  ram0  16934  ramcl  16941  prmolefac  16958  2expltfac  17004  odmodnn0  19452  pgpfi  19517  ablfac1c  19985  prmirred  21411  psrbaglesupp  21859  psrbagcon  21862  psrlidm  21899  psdmul  22081  coe1tmmul2  22190  lebnumii  24892  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  itg2cnlem2  25690  fta1g  26102  coemulhi  26186  dgradd2  26201  dgrco  26208  aareccl  26261  aaliou3lem8  26280  radcnvlem1  26349  dvradcnv  26357  dmlogdmgm  26961  wilthlem1  27005  sgmmul  27139  chtublem  27149  fsumvma2  27152  chpchtsum  27157  perfectlem2  27168  bcmono  27215  bposlem5  27226  lgsval2lem  27245  lgsval4a  27257  lgsqrlem2  27285  gausslemma2dlem0c  27296  gausslemma2dlem0d  27297  lgseisenlem1  27313  lgseisenlem2  27314  lgsquadlem1  27318  2lgslem1a1  27327  2sqlem3  27358  2sqlem7  27362  2sqlem8  27364  2sqblem  27369  2sqmod  27374  2sqreunnlem1  27387  dchrisum0re  27451  pntrlog2bndlem4  27518  pntpbnd1a  27523  ostth2lem2  27572  ostth2lem3  27573  ostth2  27575  crctcshwlkn0lem4  29791  wwlksubclwwlk  30038  nnmulge  32722  nndiffz1  32769  fzo0opth  32785  nexple  32827  pfxlsw2ccat  32931  wrdt2ind  32934  gsumwrd2dccatlem  33046  ply1unit  33538  constrdircl  33778  iconstr  33779  submateqlem1  33820  oddpwdc  34367  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemb  34381  fsum2dsub  34620  breprexplemc  34645  circlemeth  34653  tgoldbachgtde  34673  usgrgt2cycl  35174  subfaclim  35232  cvmliftlem2  35330  cvmliftlem10  35338  snmlff  35373  dfgcd3  37366  poimirlem10  37678  poimirlem23  37691  poimirlem24  37692  itg2addnclem2  37720  rrnequiv  37883  bccl2d  42032  lcmineqlem18  42087  lcmineqlem19  42088  lcmineqlem20  42089  aks4d1p1p2  42111  aks4d1p1p7  42115  aks4d1p7d1  42123  posbezout  42141  aks6d1c1  42157  aks6d1c2lem4  42168  aks6d1c2  42171  deg1gprod  42181  2np3bcnp1  42185  sticksstones6  42192  sticksstones7  42193  sticksstones22  42209  aks6d1c6lem3  42213  aks6d1c6lem4  42214  bcled  42219  bcle2d  42220  aks6d1c7lem1  42221  aks6d1c7lem2  42222  unitscyglem4  42239  fltnlta  42704  irrapxlem2  42864  irrapxlem5  42867  pellexlem1  42870  pellexlem2  42871  pellexlem5  42874  pellexlem6  42875  pell14qrgt0  42900  pell1qrge1  42911  pellfundgt1  42924  rmspecnonsq  42948  rmspecfund  42950  rmspecpos  42957  rmxypos  42988  ltrmxnn0  42990  jm2.24  43004  acongeq  43024  jm2.22  43036  jm2.23  43037  jm2.27a  43046  jm2.27c  43048  nzprmdif  44360  bccbc  44386  binomcxplemnn0  44390  fsumnncl  45620  mccllem  45645  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  dvnxpaek  45988  dvnmul  45989  dvnprodlem1  45992  stoweidlem24  46070  wallispilem4  46114  wallispilem5  46115  wallispi2lem1  46117  stirlinglem4  46123  stirlinglem5  46124  stirlinglem10  46129  stirlinglem15  46134  stirlingr  46136  fourierdlem48  46200  fourierdlem49  46201  fourierdlem92  46244  sqwvfoura  46274  elaa2lem  46279  etransclem19  46299  etransclem23  46303  etransclem27  46307  etransclem44  46324  rrndistlt  46336  modlt0b  47402  oexpnegALTV  47716  perfectALTVlem2  47761  gpgedgvtx0  48100  gpgedgvtx1  48101  blennn  48615  dignn0ldlem  48642  dig2nn1st  48645  digexp  48647  dignn0flhalf  48658  itcovalt2lem2lem1  48713