Theorem nn0ge0d 12567

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  0cc0 11099   ≤ cle 11243  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-n0 12504

This theorem is referenced by:  flmulnn0  13859  zmodfz  13925  modaddmodlo  13970  modsumfzodifsn  13979  addmodlteq  13981  expmulnbnd  14270  facwordi  14324  faclbnd  14325  faclbnd4lem3  14330  faclbnd6  14334  facavg  14336  hashdom  14414  climcnds  15904  geomulcvg  15929  mertenslem1  15937  eftabs  16128  efcllem  16130  efaddlem  16146  eftlub  16164  oexpneg  16402  divalg2  16462  bitsfzolem  16491  bitsmod  16493  sadcaddlem  16514  sadaddlem  16523  sadasslem  16527  sadeq  16529  smueqlem  16547  dfgcd2  16603  dvdssqlem  16623  nn0seqcvgd  16627  mulgcddvds  16712  isprm5  16765  zsqrtelqelz  16816  phibndlem  16828  dfphi2  16832  pythagtriplem3  16877  pythagtriplem10  16879  pythagtriplem6  16880  pythagtriplem7  16881  pythagtriplem12  16885  pythagtriplem14  16887  iserodd  16894  pcge0  16921  pcprmpw2  16941  pcmptdvds  16953  fldivp1  16956  pcbc  16959  qexpz  16960  pockthlem  16964  pockthg  16965  prmreclem3  16977  mul4sqlem  17012  4sqlem12  17015  4sqlem14  17017  4sqlem16  17019  0ram  17079  ram0  17081  ramcl  17088  prmolefac  17105  2expltfac  17151  odmodnn0  19609  pgpfi  19674  ablfac1c  20142  prmirred  21592  psrbaglesupp  22040  psrbagcon  22043  psrlidm  22079  psdmul  22297  coe1tmmul2  22405  lebnumii  25093  mbfi1fseqlem1  25842  mbfi1fseqlem3  25844  mbfi1fseqlem4  25845  mbfi1fseqlem5  25846  itg2cnlem2  25889  fta1g  26295  coemulhi  26379  dgradd2  26393  dgrco  26400  aareccl  26455  aaliou3lem8  26474  radcnvlem1  26541  dvradcnv  26549  dmlogdmgm  27153  wilthlem1  27197  sgmmul  27330  chtublem  27340  fsumvma2  27343  chpchtsum  27348  perfectlem2  27359  bcmono  27406  bposlem5  27417  lgsval2lem  27436  lgsval4a  27448  lgsqrlem2  27476  gausslemma2dlem0c  27487  gausslemma2dlem0d  27488  lgseisenlem1  27504  lgseisenlem2  27505  lgsquadlem1  27509  2lgslem1a1  27518  2sqlem3  27549  2sqlem7  27553  2sqlem8  27555  2sqblem  27560  2sqmod  27565  2sqreunnlem1  27578  dchrisum0re  27642  pntrlog2bndlem4  27709  pntpbnd1a  27714  ostth2lem2  27763  ostth2lem3  27764  ostth2  27766  crctcshwlkn0lem4  30102  wwlksubclwwlk  30349  nnmulge  33024  nndiffz1  33071  fzo0opth  33088  nexple  33117  pfxlsw2ccat  33210  wrdt2ind  33213  gsumwrd2dccatlem  33337  ply1unit  33809  selvply1rhmlemb  33853  mplmulmvr  33873  esplyind  33909  constrdircl  34099  iconstr  34100  submateqlem1  34141  oddpwdc  34688  eulerpartlems  34694  eulerpartlemgc  34696  eulerpartlemb  34702  fsum2dsub  34938  breprexplemc  34963  circlemeth  34971  tgoldbachgtde  34991  usgrgt2cycl  35520  subfaclim  35578  cvmliftlem2  35676  cvmliftlem10  35684  snmlff  35719  dfgcd3  37855  poimirlem10  38168  poimirlem23  38181  poimirlem24  38182  itg2addnclem2  38210  rrnequiv  38373  bccl2d  42647  lcmineqlem18  42702  lcmineqlem19  42703  lcmineqlem20  42704  aks4d1p1p2  42726  aks4d1p1p7  42730  aks4d1p7d1  42738  posbezout  42756  aks6d1c1  42772  aks6d1c2lem4  42783  aks6d1c2  42786  deg1gprod  42796  2np3bcnp1  42800  sticksstones6  42807  sticksstones7  42808  sticksstones22  42824  aks6d1c6lem3  42828  aks6d1c6lem4  42829  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  aks6d1c7lem2  42837  unitscyglem4  42854  fltnlta  43286  irrapxlem2  43441  irrapxlem5  43444  pellexlem1  43447  pellexlem2  43448  pellexlem5  43451  pellexlem6  43452  pell14qrgt0  43477  pell1qrge1  43488  pellfundgt1  43501  rmspecnonsq  43525  rmspecfund  43527  rmspecpos  43534  rmxypos  43565  ltrmxnn0  43567  jm2.24  43581  acongeq  43601  jm2.22  43613  jm2.23  43614  jm2.27a  43623  jm2.27c  43625  nzprmdif  44920  bccbc  44946  binomcxplemnn0  44950  fsumnncl  46179  mccllem  46204  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnxpaek  46547  dvnmul  46548  dvnprodlem1  46551  stoweidlem24  46629  wallispilem4  46673  wallispilem5  46674  wallispi2lem1  46676  stirlinglem4  46682  stirlinglem5  46683  stirlinglem10  46688  stirlinglem15  46693  stirlingr  46695  fourierdlem48  46759  fourierdlem49  46760  fourierdlem92  46803  sqwvfoura  46833  elaa2lem  46838  etransclem19  46858  etransclem23  46862  etransclem27  46866  etransclem44  46883  rrndistlt  46895  chnsubseqwl  47486  modlt0b  47994  oexpnegALTV  48330  perfectALTVlem2  48375  gpgedgvtx0  48714  gpgedgvtx1  48715  blennn  49239  dignn0ldlem  49266  dig2nn1st  49269  digexp  49271  dignn0flhalf  49282  itcovalt2lem2lem1  49337