Theorem nn0ge0d 12506

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  0cc0 11068   ≤ cle 11209  ℕ₀cn0 12442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443

This theorem is referenced by:  flmulnn0  13789  zmodfz  13855  modaddmodlo  13900  modsumfzodifsn  13909  addmodlteq  13911  expmulnbnd  14200  facwordi  14254  faclbnd  14255  faclbnd4lem3  14260  faclbnd6  14264  facavg  14266  hashdom  14344  climcnds  15817  geomulcvg  15842  mertenslem1  15850  eftabs  16041  efcllem  16043  efaddlem  16059  eftlub  16077  oexpneg  16315  divalg2  16375  bitsfzolem  16404  bitsmod  16406  sadcaddlem  16427  sadaddlem  16436  sadasslem  16440  sadeq  16442  smueqlem  16460  dfgcd2  16516  dvdssqlem  16536  nn0seqcvgd  16540  mulgcddvds  16625  isprm5  16677  zsqrtelqelz  16728  phibndlem  16740  dfphi2  16744  pythagtriplem3  16789  pythagtriplem10  16791  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem12  16797  pythagtriplem14  16799  iserodd  16806  pcge0  16833  pcprmpw2  16853  pcmptdvds  16865  fldivp1  16868  pcbc  16871  qexpz  16872  pockthlem  16876  pockthg  16877  prmreclem3  16889  mul4sqlem  16924  4sqlem12  16927  4sqlem14  16929  4sqlem16  16931  0ram  16991  ram0  16993  ramcl  17000  prmolefac  17017  2expltfac  17063  odmodnn0  19470  pgpfi  19535  ablfac1c  20003  prmirred  21384  psrbaglesupp  21831  psrbagcon  21834  psrlidm  21871  psdmul  22053  coe1tmmul2  22162  lebnumii  24865  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  itg2cnlem2  25663  fta1g  26075  coemulhi  26159  dgradd2  26174  dgrco  26181  aareccl  26234  aaliou3lem8  26253  radcnvlem1  26322  dvradcnv  26330  dmlogdmgm  26934  wilthlem1  26978  sgmmul  27112  chtublem  27122  fsumvma2  27125  chpchtsum  27130  perfectlem2  27141  bcmono  27188  bposlem5  27199  lgsval2lem  27218  lgsval4a  27230  lgsqrlem2  27258  gausslemma2dlem0c  27269  gausslemma2dlem0d  27270  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  2lgslem1a1  27300  2sqlem3  27331  2sqlem7  27335  2sqlem8  27337  2sqblem  27342  2sqmod  27347  2sqreunnlem1  27360  dchrisum0re  27424  pntrlog2bndlem4  27491  pntpbnd1a  27496  ostth2lem2  27545  ostth2lem3  27546  ostth2  27548  crctcshwlkn0lem4  29743  wwlksubclwwlk  29987  nnmulge  32662  nndiffz1  32709  fzo0opth  32728  nexple  32769  pfxlsw2ccat  32872  wrdt2ind  32875  gsumwrd2dccatlem  33006  ply1unit  33544  constrdircl  33755  iconstr  33756  submateqlem1  33797  oddpwdc  34345  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  fsum2dsub  34598  breprexplemc  34623  circlemeth  34631  tgoldbachgtde  34651  usgrgt2cycl  35117  subfaclim  35175  cvmliftlem2  35273  cvmliftlem10  35281  snmlff  35316  dfgcd3  37312  poimirlem10  37624  poimirlem23  37637  poimirlem24  37638  itg2addnclem2  37666  rrnequiv  37829  bccl2d  41979  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem20  42036  aks4d1p1p2  42058  aks4d1p1p7  42062  aks4d1p7d1  42070  posbezout  42088  aks6d1c1  42104  aks6d1c2lem4  42115  aks6d1c2  42118  deg1gprod  42128  2np3bcnp1  42132  sticksstones6  42139  sticksstones7  42140  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem4  42186  fltnlta  42651  irrapxlem2  42811  irrapxlem5  42814  pellexlem1  42817  pellexlem2  42818  pellexlem5  42821  pellexlem6  42822  pell14qrgt0  42847  pell1qrge1  42858  pellfundgt1  42871  rmspecnonsq  42895  rmspecfund  42897  rmspecpos  42905  rmxypos  42936  ltrmxnn0  42938  jm2.24  42952  acongeq  42972  jm2.22  42984  jm2.23  42985  jm2.27a  42994  jm2.27c  42996  nzprmdif  44308  bccbc  44334  binomcxplemnn0  44338  fsumnncl  45570  mccllem  45595  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnmul  45941  dvnprodlem1  45944  stoweidlem24  46022  wallispilem4  46066  wallispilem5  46067  wallispi2lem1  46069  stirlinglem4  46075  stirlinglem5  46076  stirlinglem10  46081  stirlinglem15  46086  stirlingr  46088  fourierdlem48  46152  fourierdlem49  46153  fourierdlem92  46196  sqwvfoura  46226  elaa2lem  46231  etransclem19  46251  etransclem23  46255  etransclem27  46259  etransclem44  46276  rrndistlt  46288  modlt0b  47364  oexpnegALTV  47678  perfectALTVlem2  47723  gpgedgvtx0  48052  gpgedgvtx1  48053  blennn  48564  dignn0ldlem  48591  dig2nn1st  48594  digexp  48596  dignn0flhalf  48607  itcovalt2lem2lem1  48662