Theorem nn0ge0d 12583

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  0cc0 11115   ≤ cle 11259  ℕ₀cn0 12519

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-n0 12520

This theorem is used by:  flmulnn0  13878  zmodfz  13944  modaddmodlo  13989  modsumfzodifsn  13998  addmodlteq  14000  expmulnbnd  14289  facwordi  14343  faclbnd  14344  faclbnd4lem3  14349  faclbnd6  14353  facavg  14355  hashdom  14433  climcnds  15928  geomulcvg  15953  mertenslem1  15961  eftabs  16151  efcllem  16153  efaddlem  16169  eftlub  16187  oexpneg  16425  divalg2  16485  bitsfzolem  16514  bitsmod  16516  sadcaddlem  16537  sadaddlem  16546  sadasslem  16550  sadeq  16552  smueqlem  16570  dfgcd2  16626  dvdssqlem  16646  nn0seqcvgd  16650  mulgcddvds  16735  isprm5  16788  zsqrtelqelz  16839  phibndlem  16851  dfphi2  16855  pythagtriplem3  16900  pythagtriplem10  16902  pythagtriplem6  16903  pythagtriplem7  16904  pythagtriplem12  16908  pythagtriplem14  16910  iserodd  16917  pcge0  16944  pcprmpw2  16964  pcmptdvds  16976  fldivp1  16979  pcbc  16982  qexpz  16983  pockthlem  16987  pockthg  16988  prmreclem3  17000  mul4sqlem  17035  4sqlem12  17038  4sqlem14  17040  4sqlem16  17042  0ram  17102  ram0  17104  ramcl  17111  prmolefac  17128  2expltfac  17174  odmodnn0  19654  pgpfi  19719  ablfac1c  20187  prmirred  21674  psrbaglesupp  22122  psrbagcon  22125  psrlidm  22161  psdmul  22379  coe1tmmul2  22487  lebnumii  25176  mbfi1fseqlem1  25925  mbfi1fseqlem3  25927  mbfi1fseqlem4  25928  mbfi1fseqlem5  25929  itg2cnlem2  25972  fta1g  26378  coemulhi  26462  dgradd2  26476  dgrco  26483  aareccl  26540  aaliou3lem8  26559  radcnvlem1  26627  dvradcnv  26635  dmlogdmgm  27239  wilthlem1  27283  sgmmul  27416  chtublem  27426  fsumvma2  27429  chpchtsum  27434  perfectlem2  27445  bcmono  27492  bposlem5  27503  lgsval2lem  27522  lgsval4a  27534  lgsqrlem2  27562  gausslemma2dlem0c  27573  gausslemma2dlem0d  27574  lgseisenlem1  27590  lgseisenlem2  27591  lgsquadlem1  27595  2lgslem1a1  27604  2sqlem3  27635  2sqlem7  27639  2sqlem8  27641  2sqblem  27646  2sqmod  27651  2sqreunnlem1  27664  dchrisum0re  27728  pntrlog2bndlem4  27795  pntpbnd1a  27800  ostth2lem2  27849  ostth2lem3  27850  ostth2  27852  crctcshwlkn0lem4  30229  wwlksubclwwlk  30476  nnmulge  33154  nndiffz1  33201  fzo0opth  33218  nexple  33247  pfxlsw2ccat  33336  wrdt2ind  33339  gsumwrd2dccatlem  33461  ply1unit  33929  selvply1rhmlemb  33973  mplmulmvr  33993  esplyind  34029  constrdircl  34219  iconstr  34220  submateqlem1  34261  oddpwdc  34809  eulerpartlems  34815  eulerpartlemgc  34817  eulerpartlemb  34823  fsum2dsub  35059  breprexplemc  35084  circlemeth  35092  tgoldbachgtde  35112  usgrgt2cycl  35667  subfaclim  35717  cvmliftlem2  35815  cvmliftlem10  35823  snmlff  35858  dfgcd3  38025  poimirlem10  38338  poimirlem23  38351  poimirlem24  38352  itg2addnclem2  38380  rrnequiv  38544  bccl2d  42816  lcmineqlem18  42871  lcmineqlem19  42872  lcmineqlem20  42873  aks4d1p1p2  42895  aks4d1p1p7  42899  aks4d1p7d1  42907  posbezout  42925  aks6d1c1  42941  aks6d1c2lem4  42952  aks6d1c2  42955  deg1gprod  42965  2np3bcnp1  42969  sticksstones6  42976  sticksstones7  42977  sticksstones22  42993  aks6d1c6lem3  42997  aks6d1c6lem4  42998  bcled  43003  bcle2d  43004  aks6d1c7lem1  43005  aks6d1c7lem2  43006  unitscyglem4  43023  fltnlta  43453  irrapxlem2  43608  irrapxlem5  43611  pellexlem1  43614  pellexlem2  43615  pellexlem5  43618  pellexlem6  43619  pell14qrgt0  43644  pell1qrge1  43655  pellfundgt1  43668  rmspecnonsq  43692  rmspecfund  43694  rmspecpos  43701  rmxypos  43732  ltrmxnn0  43734  jm2.24  43748  acongeq  43768  jm2.22  43780  jm2.23  43781  jm2.27a  43790  jm2.27c  43792  nzprmdif  45087  bccbc  45113  binomcxplemnn0  45117  fsumnncl  46346  mccllem  46371  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnxpaek  46714  dvnmul  46715  dvnprodlem1  46718  stoweidlem24  46796  wallispilem4  46840  wallispilem5  46841  wallispi2lem1  46843  stirlinglem4  46849  stirlinglem5  46850  stirlinglem10  46855  stirlinglem15  46860  stirlingr  46862  fourierdlem48  46926  fourierdlem49  46927  fourierdlem92  46970  sqwvfoura  47000  elaa2lem  47005  etransclem19  47025  etransclem23  47029  etransclem27  47033  etransclem44  47050  rrndistlt  47062  chnsubseqwl  47653  modlt0b  48164  oexpnegALTV  48500  perfectALTVlem2  48545  gpgedgvtx0  48884  gpgedgvtx1  48885  blennn  49412  dignn0ldlem  49439  dig2nn1st  49442  digexp  49444  dignn0flhalf  49455  itcovalt2lem2lem1  49510