Theorem nn0ge0d 12677

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  0cc0 11207   ≤ cle 11351  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-n0 12614

This theorem is used by:  flmulnn0  13974  zmodfz  14040  modaddmodlo  14085  modsumfzodifsn  14094  addmodlteq  14096  expmulnbnd  14386  facwordi  14440  faclbnd  14441  faclbnd4lem3  14446  faclbnd6  14450  facavg  14452  hashdom  14530  climcnds  16029  geomulcvg  16054  mertenslem1  16062  eftabs  16250  efcllem  16252  efaddlem  16268  eftlub  16286  oexpneg  16524  divalg2  16584  bitsfzolem  16613  bitsmod  16615  sadcaddlem  16636  sadaddlem  16645  sadasslem  16649  sadeq  16651  smueqlem  16669  dfgcd2  16728  nn0seqcvgd  16754  mulgcddvds  16839  isprm5  16892  zsqrtelqelz  16943  phibndlem  16956  dfphi2  16960  pythagtriplem3  17005  pythagtriplem10  17007  pythagtriplem6  17008  pythagtriplem7  17009  pythagtriplem12  17013  pythagtriplem14  17015  iserodd  17022  pcge0  17049  pcprmpw2  17069  pcmptdvds  17081  fldivp1  17084  pcbc  17087  qexpz  17088  pockthlem  17092  pockthg  17093  prmreclem3  17105  mul4sqlem  17140  4sqlem12  17143  4sqlem14  17145  4sqlem16  17147  0ram  17207  ram0  17209  ramcl  17216  prmolefac  17233  2expltfac  17279  odmodnn0  19763  pgpfi  19828  ablfac1c  20296  prmirred  21789  psrbaglesupp  22239  psrbagcon  22242  psrlidm  22278  psdmul  22496  coe1tmmul2  22604  lebnumii  25296  mbfi1fseqlem1  26045  mbfi1fseqlem3  26047  mbfi1fseqlem4  26048  mbfi1fseqlem5  26049  itg2cnlem2  26092  fta1g  26497  coemulhi  26582  dgradd2  26596  dgrco  26603  aareccl  26662  aaliou3lem8  26681  radcnvlem1  26749  dvradcnv  26757  dmlogdmgm  27360  wilthlem1  27404  sgmmul  27537  chtublem  27547  fsumvma2  27550  chpchtsum  27555  perfectlem2  27566  bcmono  27613  bposlem5  27624  lgsval2lem  27643  lgsval4a  27655  lgsqrlem2  27683  gausslemma2dlem0c  27694  gausslemma2dlem0d  27695  lgseisenlem1  27711  lgseisenlem2  27712  lgsquadlem1  27716  2lgslem1a1  27725  2sqlem3  27756  2sqlem7  27760  2sqlem8  27762  2sqblem  27767  2sqmod  27772  2sqreunnlem1  27785  dchrisum0re  27849  pntrlog2bndlem4  27916  pntpbnd1a  27921  ostth2lem2  27970  ostth2lem3  27971  ostth2  27973  crctcshwlkn0lem4  30411  wwlksubclwwlk  30658  nnmulge  33381  nndiffz1  33428  fzo0opth  33445  nexple  33474  pfxlsw2ccat  33563  wrdt2ind  33566  gsumwrd2dccatlem  33688  ply1unit  34157  selvply1rhmlemb  34201  mplmulmvr  34221  esplyind  34257  constrdircl  34447  iconstr  34448  submateqlem1  34489  oddpwdc  35036  eulerpartlems  35042  eulerpartlemgc  35044  eulerpartlemb  35050  fsum2dsub  35286  breprexplemc  35311  circlemeth  35319  tgoldbachgtde  35339  usgrgt2cycl  35989  subfaclim  36043  cvmliftlem2  36141  cvmliftlem10  36149  snmlff  36184  dfgcd3  38354  poimirlem10  38657  poimirlem23  38670  poimirlem24  38671  itg2addnclem2  38699  rrnequiv  38878  bccl2d  43150  lcmineqlem18  43205  lcmineqlem19  43206  lcmineqlem20  43207  aks4d1p1p2  43229  aks4d1p1p7  43233  aks4d1p7d1  43241  posbezout  43259  aks6d1c1  43275  aks6d1c2lem4  43286  aks6d1c2  43289  deg1gprod  43299  2np3bcnp1  43303  sticksstones6  43310  sticksstones7  43311  sticksstones22  43327  aks6d1c6lem3  43331  aks6d1c6lem4  43332  bcled  43337  bcle2d  43338  aks6d1c7lem1  43339  aks6d1c7lem2  43340  unitscyglem4  43357  fltnlta  43783  irrapxlem2  43939  irrapxlem5  43942  pellexlem1  43945  pellexlem2  43946  pellexlem5  43949  pellexlem6  43950  pell14qrgt0  43975  pell1qrge1  43986  pellfundgt1  43999  rmspecnonsq  44023  rmspecfund  44025  rmspecpos  44032  rmxypos  44063  ltrmxnn0  44065  jm2.24  44079  acongeq  44099  jm2.22  44111  jm2.23  44112  jm2.27a  44121  jm2.27c  44123  nzprmdif  45412  bccbc  45438  binomcxplemnn0  45442  fsumnncl  46692  mccllem  46717  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  dvnxpaek  47060  dvnmul  47061  dvnprodlem1  47064  stoweidlem24  47142  wallispilem4  47186  wallispilem5  47187  wallispi2lem1  47189  stirlinglem4  47195  stirlinglem5  47196  stirlinglem10  47201  stirlinglem15  47206  stirlingr  47208  fourierdlem48  47272  fourierdlem49  47273  fourierdlem92  47316  sqwvfoura  47346  elaa2lem  47351  etransclem19  47371  etransclem23  47375  etransclem27  47379  etransclem44  47396  rrndistlt  47408  chnsubseqwl  47997  modlt0b  48547  oexpnegALTV  48883  perfectALTVlem2  48928  gpgedgvtx0  49267  gpgedgvtx1  49268  blennn  49795  dignn0ldlem  49822  dig2nn1st  49825  digexp  49827  dignn0flhalf  49838  itcovalt2lem2lem1  49893