Theorem nn0ge0d 12563

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  0cc0 11095   ≤ cle 11239  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-n0 12500

This theorem is referenced by:  flmulnn0  13856  zmodfz  13922  modaddmodlo  13967  modsumfzodifsn  13976  addmodlteq  13978  expmulnbnd  14267  facwordi  14321  faclbnd  14322  faclbnd4lem3  14327  faclbnd6  14331  facavg  14333  hashdom  14411  climcnds  15901  geomulcvg  15926  mertenslem1  15934  eftabs  16124  efcllem  16126  efaddlem  16142  eftlub  16160  oexpneg  16398  divalg2  16458  bitsfzolem  16487  bitsmod  16489  sadcaddlem  16510  sadaddlem  16519  sadasslem  16523  sadeq  16525  smueqlem  16543  dfgcd2  16599  dvdssqlem  16619  nn0seqcvgd  16623  mulgcddvds  16708  isprm5  16761  zsqrtelqelz  16812  phibndlem  16824  dfphi2  16828  pythagtriplem3  16873  pythagtriplem10  16875  pythagtriplem6  16876  pythagtriplem7  16877  pythagtriplem12  16881  pythagtriplem14  16883  iserodd  16890  pcge0  16917  pcprmpw2  16937  pcmptdvds  16949  fldivp1  16952  pcbc  16955  qexpz  16956  pockthlem  16960  pockthg  16961  prmreclem3  16973  mul4sqlem  17008  4sqlem12  17011  4sqlem14  17013  4sqlem16  17015  0ram  17075  ram0  17077  ramcl  17084  prmolefac  17101  2expltfac  17147  odmodnn0  19605  pgpfi  19670  ablfac1c  20138  prmirred  21624  psrbaglesupp  22072  psrbagcon  22075  psrlidm  22111  psdmul  22329  coe1tmmul2  22437  lebnumii  25125  mbfi1fseqlem1  25874  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  itg2cnlem2  25921  fta1g  26327  coemulhi  26411  dgradd2  26425  dgrco  26432  aareccl  26489  aaliou3lem8  26508  radcnvlem1  26576  dvradcnv  26584  dmlogdmgm  27188  wilthlem1  27232  sgmmul  27365  chtublem  27375  fsumvma2  27378  chpchtsum  27383  perfectlem2  27394  bcmono  27441  bposlem5  27452  lgsval2lem  27471  lgsval4a  27483  lgsqrlem2  27511  gausslemma2dlem0c  27522  gausslemma2dlem0d  27523  lgseisenlem1  27539  lgseisenlem2  27540  lgsquadlem1  27544  2lgslem1a1  27553  2sqlem3  27584  2sqlem7  27588  2sqlem8  27590  2sqblem  27595  2sqmod  27600  2sqreunnlem1  27613  dchrisum0re  27677  pntrlog2bndlem4  27744  pntpbnd1a  27749  ostth2lem2  27798  ostth2lem3  27799  ostth2  27801  crctcshwlkn0lem4  30162  wwlksubclwwlk  30409  nnmulge  33084  nndiffz1  33131  fzo0opth  33148  nexple  33177  pfxlsw2ccat  33270  wrdt2ind  33273  gsumwrd2dccatlem  33397  ply1unit  33865  selvply1rhmlemb  33909  mplmulmvr  33929  esplyind  33965  constrdircl  34155  iconstr  34156  submateqlem1  34197  oddpwdc  34744  eulerpartlems  34750  eulerpartlemgc  34752  eulerpartlemb  34758  fsum2dsub  34994  breprexplemc  35019  circlemeth  35027  tgoldbachgtde  35047  usgrgt2cycl  35622  subfaclim  35680  cvmliftlem2  35778  cvmliftlem10  35786  snmlff  35821  dfgcd3  37968  poimirlem10  38281  poimirlem23  38294  poimirlem24  38295  itg2addnclem2  38323  rrnequiv  38486  bccl2d  42758  lcmineqlem18  42813  lcmineqlem19  42814  lcmineqlem20  42815  aks4d1p1p2  42837  aks4d1p1p7  42841  aks4d1p7d1  42849  posbezout  42867  aks6d1c1  42883  aks6d1c2lem4  42894  aks6d1c2  42897  deg1gprod  42907  2np3bcnp1  42911  sticksstones6  42918  sticksstones7  42919  sticksstones22  42935  aks6d1c6lem3  42939  aks6d1c6lem4  42940  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  aks6d1c7lem2  42948  unitscyglem4  42965  fltnlta  43395  irrapxlem2  43550  irrapxlem5  43553  pellexlem1  43556  pellexlem2  43557  pellexlem5  43560  pellexlem6  43561  pell14qrgt0  43586  pell1qrge1  43597  pellfundgt1  43610  rmspecnonsq  43634  rmspecfund  43636  rmspecpos  43643  rmxypos  43674  ltrmxnn0  43676  jm2.24  43690  acongeq  43710  jm2.22  43722  jm2.23  43723  jm2.27a  43732  jm2.27c  43734  nzprmdif  45029  bccbc  45055  binomcxplemnn0  45059  fsumnncl  46288  mccllem  46313  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnxpaek  46656  dvnmul  46657  dvnprodlem1  46660  stoweidlem24  46738  wallispilem4  46782  wallispilem5  46783  wallispi2lem1  46785  stirlinglem4  46791  stirlinglem5  46792  stirlinglem10  46797  stirlinglem15  46802  stirlingr  46804  fourierdlem48  46868  fourierdlem49  46869  fourierdlem92  46912  sqwvfoura  46942  elaa2lem  46947  etransclem19  46967  etransclem23  46971  etransclem27  46975  etransclem44  46992  rrndistlt  47004  chnsubseqwl  47595  modlt0b  48106  oexpnegALTV  48442  perfectALTVlem2  48487  gpgedgvtx0  48826  gpgedgvtx1  48827  blennn  49355  dignn0ldlem  49382  dig2nn1st  49385  digexp  49387  dignn0flhalf  49398  itcovalt2lem2lem1  49453