Theorem nn0ge0d 12495

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  0cc0 11032   ≤ cle 11174  ℕ₀cn0 12431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432

This theorem is referenced by:  flmulnn0  13780  zmodfz  13846  modaddmodlo  13891  modsumfzodifsn  13900  addmodlteq  13902  expmulnbnd  14191  facwordi  14245  faclbnd  14246  faclbnd4lem3  14251  faclbnd6  14255  facavg  14257  hashdom  14335  climcnds  15810  geomulcvg  15835  mertenslem1  15843  eftabs  16034  efcllem  16036  efaddlem  16052  eftlub  16070  oexpneg  16308  divalg2  16368  bitsfzolem  16397  bitsmod  16399  sadcaddlem  16420  sadaddlem  16429  sadasslem  16433  sadeq  16435  smueqlem  16453  dfgcd2  16509  dvdssqlem  16529  nn0seqcvgd  16533  mulgcddvds  16618  isprm5  16671  zsqrtelqelz  16722  phibndlem  16734  dfphi2  16738  pythagtriplem3  16783  pythagtriplem10  16785  pythagtriplem6  16786  pythagtriplem7  16787  pythagtriplem12  16791  pythagtriplem14  16793  iserodd  16800  pcge0  16827  pcprmpw2  16847  pcmptdvds  16859  fldivp1  16862  pcbc  16865  qexpz  16866  pockthlem  16870  pockthg  16871  prmreclem3  16883  mul4sqlem  16918  4sqlem12  16921  4sqlem14  16923  4sqlem16  16925  0ram  16985  ram0  16987  ramcl  16994  prmolefac  17011  2expltfac  17057  odmodnn0  19509  pgpfi  19574  ablfac1c  20042  prmirred  21467  psrbaglesupp  21915  psrbagcon  21918  psrlidm  21953  psdmul  22145  coe1tmmul2  22254  lebnumii  24946  mbfi1fseqlem1  25695  mbfi1fseqlem3  25697  mbfi1fseqlem4  25698  mbfi1fseqlem5  25699  itg2cnlem2  25742  fta1g  26148  coemulhi  26232  dgradd2  26246  dgrco  26253  aareccl  26306  aaliou3lem8  26325  radcnvlem1  26394  dvradcnv  26402  dmlogdmgm  27004  wilthlem1  27048  sgmmul  27181  chtublem  27191  fsumvma2  27194  chpchtsum  27199  perfectlem2  27210  bcmono  27257  bposlem5  27268  lgsval2lem  27287  lgsval4a  27299  lgsqrlem2  27327  gausslemma2dlem0c  27338  gausslemma2dlem0d  27339  lgseisenlem1  27355  lgseisenlem2  27356  lgsquadlem1  27360  2lgslem1a1  27369  2sqlem3  27400  2sqlem7  27404  2sqlem8  27406  2sqblem  27411  2sqmod  27416  2sqreunnlem1  27429  dchrisum0re  27493  pntrlog2bndlem4  27560  pntpbnd1a  27565  ostth2lem2  27614  ostth2lem3  27615  ostth2  27617  crctcshwlkn0lem4  29899  wwlksubclwwlk  30146  nnmulge  32830  nndiffz1  32877  fzo0opth  32894  nexple  32935  pfxlsw2ccat  33028  wrdt2ind  33031  gsumwrd2dccatlem  33156  ply1unit  33653  mplmulmvr  33701  esplyind  33737  constrdircl  33928  iconstr  33929  submateqlem1  33970  oddpwdc  34517  eulerpartlems  34523  eulerpartlemgc  34525  eulerpartlemb  34531  fsum2dsub  34770  breprexplemc  34795  circlemeth  34803  tgoldbachgtde  34823  usgrgt2cycl  35331  subfaclim  35389  cvmliftlem2  35487  cvmliftlem10  35495  snmlff  35530  dfgcd3  37657  poimirlem10  37968  poimirlem23  37981  poimirlem24  37982  itg2addnclem2  38010  rrnequiv  38173  bccl2d  42447  lcmineqlem18  42502  lcmineqlem19  42503  lcmineqlem20  42504  aks4d1p1p2  42526  aks4d1p1p7  42530  aks4d1p7d1  42538  posbezout  42556  aks6d1c1  42572  aks6d1c2lem4  42583  aks6d1c2  42586  deg1gprod  42596  2np3bcnp1  42600  sticksstones6  42607  sticksstones7  42608  sticksstones22  42624  aks6d1c6lem3  42628  aks6d1c6lem4  42629  bcled  42634  bcle2d  42635  aks6d1c7lem1  42636  aks6d1c7lem2  42637  unitscyglem4  42654  fltnlta  43113  irrapxlem2  43272  irrapxlem5  43275  pellexlem1  43278  pellexlem2  43279  pellexlem5  43282  pellexlem6  43283  pell14qrgt0  43308  pell1qrge1  43319  pellfundgt1  43332  rmspecnonsq  43356  rmspecfund  43358  rmspecpos  43365  rmxypos  43396  ltrmxnn0  43398  jm2.24  43412  acongeq  43432  jm2.22  43444  jm2.23  43445  jm2.27a  43454  jm2.27c  43456  nzprmdif  44767  bccbc  44793  binomcxplemnn0  44797  fsumnncl  46023  mccllem  46048  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnxpaek  46391  dvnmul  46392  dvnprodlem1  46395  stoweidlem24  46473  wallispilem4  46517  wallispilem5  46518  wallispi2lem1  46520  stirlinglem4  46526  stirlinglem5  46527  stirlinglem10  46532  stirlinglem15  46537  stirlingr  46539  fourierdlem48  46603  fourierdlem49  46604  fourierdlem92  46647  sqwvfoura  46677  elaa2lem  46682  etransclem19  46702  etransclem23  46706  etransclem27  46710  etransclem44  46727  rrndistlt  46739  chnsubseqwl  47328  modlt0b  47832  oexpnegALTV  48168  perfectALTVlem2  48213  gpgedgvtx0  48552  gpgedgvtx1  48553  blennn  49066  dignn0ldlem  49093  dig2nn1st  49096  digexp  49098  dignn0flhalf  49109  itcovalt2lem2lem1  49164