Theorem nn0ge0d 12463

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  0cc0 11024   ≤ cle 11165  ℕ₀cn0 12399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-n0 12400

This theorem is referenced by:  flmulnn0  13745  zmodfz  13811  modaddmodlo  13856  modsumfzodifsn  13865  addmodlteq  13867  expmulnbnd  14156  facwordi  14210  faclbnd  14211  faclbnd4lem3  14216  faclbnd6  14220  facavg  14222  hashdom  14300  climcnds  15772  geomulcvg  15797  mertenslem1  15805  eftabs  15996  efcllem  15998  efaddlem  16014  eftlub  16032  oexpneg  16270  divalg2  16330  bitsfzolem  16359  bitsmod  16361  sadcaddlem  16382  sadaddlem  16391  sadasslem  16395  sadeq  16397  smueqlem  16415  dfgcd2  16471  dvdssqlem  16491  nn0seqcvgd  16495  mulgcddvds  16580  isprm5  16632  zsqrtelqelz  16683  phibndlem  16695  dfphi2  16699  pythagtriplem3  16744  pythagtriplem10  16746  pythagtriplem6  16747  pythagtriplem7  16748  pythagtriplem12  16752  pythagtriplem14  16754  iserodd  16761  pcge0  16788  pcprmpw2  16808  pcmptdvds  16820  fldivp1  16823  pcbc  16826  qexpz  16827  pockthlem  16831  pockthg  16832  prmreclem3  16844  mul4sqlem  16879  4sqlem12  16882  4sqlem14  16884  4sqlem16  16886  0ram  16946  ram0  16948  ramcl  16955  prmolefac  16972  2expltfac  17018  odmodnn0  19467  pgpfi  19532  ablfac1c  20000  prmirred  21427  psrbaglesupp  21876  psrbagcon  21879  psrlidm  21915  psdmul  22107  coe1tmmul2  22216  lebnumii  24919  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  itg2cnlem2  25717  fta1g  26129  coemulhi  26213  dgradd2  26228  dgrco  26235  aareccl  26288  aaliou3lem8  26307  radcnvlem1  26376  dvradcnv  26384  dmlogdmgm  26988  wilthlem1  27032  sgmmul  27166  chtublem  27176  fsumvma2  27179  chpchtsum  27184  perfectlem2  27195  bcmono  27242  bposlem5  27253  lgsval2lem  27272  lgsval4a  27284  lgsqrlem2  27312  gausslemma2dlem0c  27323  gausslemma2dlem0d  27324  lgseisenlem1  27340  lgseisenlem2  27341  lgsquadlem1  27345  2lgslem1a1  27354  2sqlem3  27385  2sqlem7  27389  2sqlem8  27391  2sqblem  27396  2sqmod  27401  2sqreunnlem1  27414  dchrisum0re  27478  pntrlog2bndlem4  27545  pntpbnd1a  27550  ostth2lem2  27599  ostth2lem3  27600  ostth2  27602  crctcshwlkn0lem4  29835  wwlksubclwwlk  30082  nnmulge  32767  nndiffz1  32815  fzo0opth  32832  nexple  32874  pfxlsw2ccat  32981  wrdt2ind  32984  gsumwrd2dccatlem  33108  ply1unit  33605  mplmulmvr  33653  esplyind  33680  constrdircl  33871  iconstr  33872  submateqlem1  33913  oddpwdc  34460  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemb  34474  fsum2dsub  34713  breprexplemc  34738  circlemeth  34746  tgoldbachgtde  34766  usgrgt2cycl  35273  subfaclim  35331  cvmliftlem2  35429  cvmliftlem10  35437  snmlff  35472  dfgcd3  37468  poimirlem10  37770  poimirlem23  37783  poimirlem24  37784  itg2addnclem2  37812  rrnequiv  37975  bccl2d  42184  lcmineqlem18  42239  lcmineqlem19  42240  lcmineqlem20  42241  aks4d1p1p2  42263  aks4d1p1p7  42267  aks4d1p7d1  42275  posbezout  42293  aks6d1c1  42309  aks6d1c2lem4  42320  aks6d1c2  42323  deg1gprod  42333  2np3bcnp1  42337  sticksstones6  42344  sticksstones7  42345  sticksstones22  42361  aks6d1c6lem3  42365  aks6d1c6lem4  42366  bcled  42371  bcle2d  42372  aks6d1c7lem1  42373  aks6d1c7lem2  42374  unitscyglem4  42391  fltnlta  42848  irrapxlem2  43007  irrapxlem5  43010  pellexlem1  43013  pellexlem2  43014  pellexlem5  43017  pellexlem6  43018  pell14qrgt0  43043  pell1qrge1  43054  pellfundgt1  43067  rmspecnonsq  43091  rmspecfund  43093  rmspecpos  43100  rmxypos  43131  ltrmxnn0  43133  jm2.24  43147  acongeq  43167  jm2.22  43179  jm2.23  43180  jm2.27a  43189  jm2.27c  43191  nzprmdif  44502  bccbc  44528  binomcxplemnn0  44532  fsumnncl  45760  mccllem  45785  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnxpaek  46128  dvnmul  46129  dvnprodlem1  46132  stoweidlem24  46210  wallispilem4  46254  wallispilem5  46255  wallispi2lem1  46257  stirlinglem4  46263  stirlinglem5  46264  stirlinglem10  46269  stirlinglem15  46274  stirlingr  46276  fourierdlem48  46340  fourierdlem49  46341  fourierdlem92  46384  sqwvfoura  46414  elaa2lem  46419  etransclem19  46439  etransclem23  46443  etransclem27  46447  etransclem44  46464  rrndistlt  46476  chnsubseqwl  47065  modlt0b  47551  oexpnegALTV  47865  perfectALTVlem2  47910  gpgedgvtx0  48249  gpgedgvtx1  48250  blennn  48763  dignn0ldlem  48790  dig2nn1st  48793  digexp  48795  dignn0flhalf  48806  itcovalt2lem2lem1  48861