Theorem nn0ge0d 12448

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  0cc0 11009   ≤ cle 11150  ℕ₀cn0 12384

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385

This theorem is referenced by:  flmulnn0  13731  zmodfz  13797  modaddmodlo  13842  modsumfzodifsn  13851  addmodlteq  13853  expmulnbnd  14142  facwordi  14196  faclbnd  14197  faclbnd4lem3  14202  faclbnd6  14206  facavg  14208  hashdom  14286  climcnds  15758  geomulcvg  15783  mertenslem1  15791  eftabs  15982  efcllem  15984  efaddlem  16000  eftlub  16018  oexpneg  16256  divalg2  16316  bitsfzolem  16345  bitsmod  16347  sadcaddlem  16368  sadaddlem  16377  sadasslem  16381  sadeq  16383  smueqlem  16401  dfgcd2  16457  dvdssqlem  16477  nn0seqcvgd  16481  mulgcddvds  16566  isprm5  16618  zsqrtelqelz  16669  phibndlem  16681  dfphi2  16685  pythagtriplem3  16730  pythagtriplem10  16732  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem12  16738  pythagtriplem14  16740  iserodd  16747  pcge0  16774  pcprmpw2  16794  pcmptdvds  16806  fldivp1  16809  pcbc  16812  qexpz  16813  pockthlem  16817  pockthg  16818  prmreclem3  16830  mul4sqlem  16865  4sqlem12  16868  4sqlem14  16870  4sqlem16  16872  0ram  16932  ram0  16934  ramcl  16941  prmolefac  16958  2expltfac  17004  odmodnn0  19419  pgpfi  19484  ablfac1c  19952  prmirred  21381  psrbaglesupp  21829  psrbagcon  21832  psrlidm  21869  psdmul  22051  coe1tmmul2  22160  lebnumii  24863  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  itg2cnlem2  25661  fta1g  26073  coemulhi  26157  dgradd2  26172  dgrco  26179  aareccl  26232  aaliou3lem8  26251  radcnvlem1  26320  dvradcnv  26328  dmlogdmgm  26932  wilthlem1  26976  sgmmul  27110  chtublem  27120  fsumvma2  27123  chpchtsum  27128  perfectlem2  27139  bcmono  27186  bposlem5  27197  lgsval2lem  27216  lgsval4a  27228  lgsqrlem2  27256  gausslemma2dlem0c  27267  gausslemma2dlem0d  27268  lgseisenlem1  27284  lgseisenlem2  27285  lgsquadlem1  27289  2lgslem1a1  27298  2sqlem3  27329  2sqlem7  27333  2sqlem8  27335  2sqblem  27340  2sqmod  27345  2sqreunnlem1  27358  dchrisum0re  27422  pntrlog2bndlem4  27489  pntpbnd1a  27494  ostth2lem2  27543  ostth2lem3  27544  ostth2  27546  crctcshwlkn0lem4  29758  wwlksubclwwlk  30002  nnmulge  32682  nndiffz1  32729  fzo0opth  32748  nexple  32789  pfxlsw2ccat  32892  wrdt2ind  32895  gsumwrd2dccatlem  33019  ply1unit  33510  constrdircl  33732  iconstr  33733  submateqlem1  33774  oddpwdc  34322  eulerpartlems  34328  eulerpartlemgc  34330  eulerpartlemb  34336  fsum2dsub  34575  breprexplemc  34600  circlemeth  34608  tgoldbachgtde  34628  usgrgt2cycl  35103  subfaclim  35161  cvmliftlem2  35259  cvmliftlem10  35267  snmlff  35302  dfgcd3  37298  poimirlem10  37610  poimirlem23  37623  poimirlem24  37624  itg2addnclem2  37652  rrnequiv  37815  bccl2d  41964  lcmineqlem18  42019  lcmineqlem19  42020  lcmineqlem20  42021  aks4d1p1p2  42043  aks4d1p1p7  42047  aks4d1p7d1  42055  posbezout  42073  aks6d1c1  42089  aks6d1c2lem4  42100  aks6d1c2  42103  deg1gprod  42113  2np3bcnp1  42117  sticksstones6  42124  sticksstones7  42125  sticksstones22  42141  aks6d1c6lem3  42145  aks6d1c6lem4  42146  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  unitscyglem4  42171  fltnlta  42636  irrapxlem2  42796  irrapxlem5  42799  pellexlem1  42802  pellexlem2  42803  pellexlem5  42806  pellexlem6  42807  pell14qrgt0  42832  pell1qrge1  42843  pellfundgt1  42856  rmspecnonsq  42880  rmspecfund  42882  rmspecpos  42889  rmxypos  42920  ltrmxnn0  42922  jm2.24  42936  acongeq  42956  jm2.22  42968  jm2.23  42969  jm2.27a  42978  jm2.27c  42980  nzprmdif  44292  bccbc  44318  binomcxplemnn0  44322  fsumnncl  45553  mccllem  45578  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnxpaek  45923  dvnmul  45924  dvnprodlem1  45927  stoweidlem24  46005  wallispilem4  46049  wallispilem5  46050  wallispi2lem1  46052  stirlinglem4  46058  stirlinglem5  46059  stirlinglem10  46064  stirlinglem15  46069  stirlingr  46071  fourierdlem48  46135  fourierdlem49  46136  fourierdlem92  46179  sqwvfoura  46209  elaa2lem  46214  etransclem19  46234  etransclem23  46238  etransclem27  46242  etransclem44  46259  rrndistlt  46271  modlt0b  47347  oexpnegALTV  47661  perfectALTVlem2  47706  gpgedgvtx0  48045  gpgedgvtx1  48046  blennn  48560  dignn0ldlem  48587  dig2nn1st  48590  digexp  48592  dignn0flhalf  48603  itcovalt2lem2lem1  48658