Theorem nn0ge0d 12590

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  0cc0 11155   ≤ cle 11296  ℕ₀cn0 12526

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527

This theorem is referenced by:  flmulnn0  13867  zmodfz  13933  modaddmodlo  13976  modsumfzodifsn  13985  addmodlteq  13987  expmulnbnd  14274  facwordi  14328  faclbnd  14329  faclbnd4lem3  14334  faclbnd6  14338  facavg  14340  hashdom  14418  climcnds  15887  geomulcvg  15912  mertenslem1  15920  eftabs  16111  efcllem  16113  efaddlem  16129  eftlub  16145  oexpneg  16382  divalg2  16442  bitsfzolem  16471  bitsmod  16473  sadcaddlem  16494  sadaddlem  16503  sadasslem  16507  sadeq  16509  smueqlem  16527  dfgcd2  16583  dvdssqlem  16603  nn0seqcvgd  16607  mulgcddvds  16692  isprm5  16744  zsqrtelqelz  16795  phibndlem  16807  dfphi2  16811  pythagtriplem3  16856  pythagtriplem10  16858  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem12  16864  pythagtriplem14  16866  iserodd  16873  pcge0  16900  pcprmpw2  16920  pcmptdvds  16932  fldivp1  16935  pcbc  16938  qexpz  16939  pockthlem  16943  pockthg  16944  prmreclem3  16956  mul4sqlem  16991  4sqlem12  16994  4sqlem14  16996  4sqlem16  16998  0ram  17058  ram0  17060  ramcl  17067  prmolefac  17084  2expltfac  17130  odmodnn0  19558  pgpfi  19623  ablfac1c  20091  prmirred  21485  psrbaglesupp  21942  psrbagcon  21945  psrlidm  21982  psdmul  22170  coe1tmmul2  22279  lebnumii  24998  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  itg2cnlem2  25797  fta1g  26209  coemulhi  26293  dgradd2  26308  dgrco  26315  aareccl  26368  aaliou3lem8  26387  radcnvlem1  26456  dvradcnv  26464  dmlogdmgm  27067  wilthlem1  27111  sgmmul  27245  chtublem  27255  fsumvma2  27258  chpchtsum  27263  perfectlem2  27274  bcmono  27321  bposlem5  27332  lgsval2lem  27351  lgsval4a  27363  lgsqrlem2  27391  gausslemma2dlem0c  27402  gausslemma2dlem0d  27403  lgseisenlem1  27419  lgseisenlem2  27420  lgsquadlem1  27424  2lgslem1a1  27433  2sqlem3  27464  2sqlem7  27468  2sqlem8  27470  2sqblem  27475  2sqmod  27480  2sqreunnlem1  27493  dchrisum0re  27557  pntrlog2bndlem4  27624  pntpbnd1a  27629  ostth2lem2  27678  ostth2lem3  27679  ostth2  27681  crctcshwlkn0lem4  29833  wwlksubclwwlk  30077  nnmulge  32749  nndiffz1  32788  fzo0opth  32807  nexple  32833  pfxlsw2ccat  32935  wrdt2ind  32938  gsumwrd2dccatlem  33069  ply1unit  33600  submateqlem1  33806  oddpwdc  34356  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemb  34370  fsum2dsub  34622  breprexplemc  34647  circlemeth  34655  tgoldbachgtde  34675  usgrgt2cycl  35135  subfaclim  35193  cvmliftlem2  35291  cvmliftlem10  35299  snmlff  35334  dfgcd3  37325  poimirlem10  37637  poimirlem23  37650  poimirlem24  37651  itg2addnclem2  37679  rrnequiv  37842  bccl2d  41992  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem20  42049  aks4d1p1p2  42071  aks4d1p1p7  42075  aks4d1p7d1  42083  posbezout  42101  aks6d1c1  42117  aks6d1c2lem4  42128  aks6d1c2  42131  deg1gprod  42141  2np3bcnp1  42145  sticksstones6  42152  sticksstones7  42153  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  unitscyglem4  42199  metakunt2  42207  fltnlta  42673  irrapxlem2  42834  irrapxlem5  42837  pellexlem1  42840  pellexlem2  42841  pellexlem5  42844  pellexlem6  42845  pell14qrgt0  42870  pell1qrge1  42881  pellfundgt1  42894  rmspecnonsq  42918  rmspecfund  42920  rmspecpos  42928  rmxypos  42959  ltrmxnn0  42961  jm2.24  42975  acongeq  42995  jm2.22  43007  jm2.23  43008  jm2.27a  43017  jm2.27c  43019  nzprmdif  44338  bccbc  44364  binomcxplemnn0  44368  fsumnncl  45587  mccllem  45612  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnmul  45958  dvnprodlem1  45961  stoweidlem24  46039  wallispilem4  46083  wallispilem5  46084  wallispi2lem1  46086  stirlinglem4  46092  stirlinglem5  46093  stirlinglem10  46098  stirlinglem15  46103  stirlingr  46105  fourierdlem48  46169  fourierdlem49  46170  fourierdlem92  46213  sqwvfoura  46243  elaa2lem  46248  etransclem19  46268  etransclem23  46272  etransclem27  46276  etransclem44  46293  rrndistlt  46305  oexpnegALTV  47664  perfectALTVlem2  47709  gpgedgvtx0  48019  gpgedgvtx1  48020  blennn  48496  dignn0ldlem  48523  dig2nn1st  48526  digexp  48528  dignn0flhalf  48539  itcovalt2lem2lem1  48594