Theorem 1nn0 12521

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	⊢ 1 ∈ ℕ0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 12245	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 12513	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2143  1c1 11102  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  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 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235  df-n0 12506

This theorem is referenced by:  peano2nn0  12545  deccl  12727  11nn0  12728  12nn0  12729  16nn0  12730  10nn0  12734  11nn  12737  numsucc  12757  numadd  12764  numaddc  12765  11multnc  12785  6p5lem  12787  6p6e12  12791  7p5e12  12794  8p4e12  12799  9p2e11  12804  9p3e12  12805  10p10e20  12812  4t4e16  12816  5t2e10  12817  5t4e20  12819  6t3e18  12822  6t4e24  12823  7t3e21  12827  7t4e28  12828  8t3e24  12833  9t3e27  12840  9t9e81  12846  1lt10  12857  xnn0n0n1ge2b  13158  fz0to3un2pr  13659  elfzom1elp1fzo  13763  fzo0sn0fzo1  13786  fvf1tp  13824  fldiv4lem1div2  13872  expn1  14109  nn0expcl  14113  sqval  14152  nn0opthlem1  14306  fac2  14317  faclbnd4lem2  14332  bccl  14360  hashsng  14407  hashen1  14408  hashrabrsn  14410  1elfz0hash  14428  hashgt23el  14463  hashprlei  14507  hashtplei  14523  tpf1ofv1  14536  tpfo  14539  wrdred1hash  14600  pfx1  14742  repsw1  14822  cshw1  14861  s3fv1  14931  s4fv1  14935  pfx2  14986  repsw2  14989  repsw3  14990  wwlktovf  14995  relexp1g  15065  relexpaddg  15092  rtrclreclem1  15096  sgnmulsgn  15148  bcxmas  15891  climcndslem2  15906  climcnds  15907  arisum  15916  geoisum1  15935  geoisum1c  15936  mertenslem2  15941  fprodnn0cl  16013  nn0risefaccl  16078  bpoly1  16106  bpoly4  16114  fsumcube  16115  ege2le3  16145  ef4p  16170  efgt1p2  16171  efgt1p  16172  sin01gt0  16247  rpnnen2lem3  16273  dvds1  16378  3dvds2dec  16392  5ndvds6  16473  bitsmod  16495  bitsinv1lem  16500  sadadd2lem  16518  sadadd  16526  sadass  16530  smupp1  16539  smumul  16552  nn0rppwr  16620  prmdvdsbc  16786  pcelnn  16931  pockthg  16967  vdwlem12  17053  prmo1  17098  dec5nprm  17127  dec2nprm  17128  modxp1i  17131  2exp8  17149  2exp11  17150  2exp16  17151  2expltfac  17153  5prm  17169  11prm  17176  13prm  17177  17prm  17178  19prm  17179  23prm  17180  prmlem2  17181  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  ocndx  17435  ocid  17436  basendxnocndx  17437  plendxnocndx  17438  dsndx  17439  dsid  17440  dsndxnn  17441  basendxltdsndx  17442  slotsdifdsndx  17448  unifndx  17449  unifid  17450  unifndxnn  17451  basendxltunifndx  17452  slotsdifunifndx  17455  odrngstr  17457  homndx  17465  homid  17466  ccondx  17467  ccoid  17468  slotsbhcdif  17469  slotsdifplendx2  17470  slotsdifocndx  17471  imasvalstr  17505  prdsvalstr  17506  catstr  18018  ipostr  18586  smndex2dnrinv  18978  cycsubmcl  19273  psgnunilem2  19566  odcau  19675  lt6abl  19966  omndmul2  20204  0ringnnzr  20610  cnfldstr  21505  nn0srg  21568  freshmansdream  21705  mvrid  22114  mvrf1  22116  mplcoe3  22170  psrbagsn  22195  evlslem1  22214  mhpvarcl  22292  psdcl  22305  psdmul  22310  psdmvr  22313  pmatcollpw3fi1lem1  22924  chfacfscmulgsum  22998  chfacfpmmulfsupp  23001  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cpmadugsumlemB  23012  cpmadugsumlemF  23014  dscmet  24710  ehl1eudis  25560  dveflem  26119  c1lip2  26138  itgpowd  26190  ply1remlem  26303  fta1glem1  26306  fta1blem  26309  plyid  26347  coeidp  26401  dgrid  26402  plyn0mulidp  26423  vieta1lem2  26453  vieta1  26454  aalioulem3  26478  aaliou2b  26485  dvtaylp  26514  taylthlem1  26517  taylthlem2  26518  radcnvlem2  26558  dvradcnv  26565  pserdvlem2  26572  logtayllem  26805  logtayl  26806  cxp1  26817  quart1cl  27000  quart1lem  27001  quart1  27002  quartlem1  27003  quartlem2  27004  leibpilem2  27087  log2ublem3  27094  log2ub  27095  birthday  27100  lgamcvg2  27200  gamp1  27203  issqf  27281  ppi2  27315  mumullem2  27325  sqff1o  27327  1sgmprm  27344  ppiublem2  27348  chtublem  27356  logfacbnd3  27368  logexprlim  27370  logfacrlim2  27371  perfectlem1  27374  perfectlem2  27375  bclbnd  27425  bpos1  27428  bposlem6  27434  lgsval  27446  2lgslem3a  27541  2lgslem3c  27543  rpvmasumlem  27632  log2sumbnd  27689  itvndx  28687  lngndx  28688  itvid  28689  lngid  28690  slotsinbpsd  28691  slotslnbpsd  28692  lngndxnitvndx  28693  trkgstr  28694  eengstr  29311  edgfid  29321  edgfndx  29322  edgfndxnn  29323  basendxltedgfndx  29325  usgrexmplef  29590  cusgrsizeindb1  29781  wlk1ewlk  29970  usgr2pthlem  30093  uspgrn2crct  30138  crctcshwlkn0lem5  30144  rusgrnumwwlkl1  30301  rusgrnumwwlkb1  30305  clwwlkccatlem  30321  clwwlkinwwlk  30372  umgr2cwwkdifex  30397  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  konigsbergiedgw  30580  konigsberglem1  30584  konigsberglem2  30585  konigsberglem3  30586  konigsberglem4  30587  1kp2ke3k  30778  ex-exp  30782  ex-fac  30783  9p10ne21  30802  sgnmulsgp  33157  nexple  33158  dpmul4  33214  threehalves  33215  1mhdrd  33216  s2f1  33246  cycpm2tr  33420  evl1deg1  33847  evl1deg2  33848  evl1deg3  33849  ply1dg1rt  33851  coe1vr1  33862  deg1vr  33863  mplmulmvr  33910  esplylem  33937  esplyfv1  33940  esplyfval1  33944  esplyfvaln  33945  esplyind  33946  drngdimgt0  33989  rtelextdg2lem  34097  fldext2chn  34099  constrdircl  34136  iconstr  34137  2sqr3minply  34151  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  cos9thpiminply  34159  lmat22e12  34190  lmat22e21  34191  lmat22e22  34192  madjusmdetlem4  34201  oddpwdc  34725  eulerpartlemd  34737  eulerpartlemgs2  34751  eulerpartlemn  34752  iwrdsplit  34758  fib0  34770  fib1  34771  fibp1  34772  signstfveq0  34945  signsvvf  34947  signsvfn  34950  signshlen  34958  prodfzo03  34971  reprsuc  34983  breprexplemc  35000  hgt750lemd  35016  hgt750lem  35019  hgt750lem2  35020  hgt750leme  35026  usgrgt2cycl  35603  subfac1  35651  kur14lem9  35687  bccolsum  36212  nn0prpw  36815  12gcd5e1  42751  60gcd6e6  42752  60gcd7e1  42753  420gcd8e4  42754  12lcm5e60  42756  lcmineqlem11  42787  lcmineqlem18  42794  lcmineqlem22  42798  lcmineqlem  42800  3exp7  42801  3lexlogpow5ineq1  42802  3lexlogpow5ineq2  42803  3lexlogpow5ineq5  42808  dvrelogpow2b  42816  aks4d1p1p2  42818  aks4d1p1p4  42819  aks4d1p1p6  42821  aks4d1p1p7  42822  aks4d1p1p5  42823  aks4d1p1  42824  aks4d1p3  42826  aks6d1c1p8  42863  aks6d1c5lem3  42885  2np3bcnp1  42892  2ap1caineq  42893  sticksstones22  42916  aks6d1c6lem1  42918  aks6d1c7lem1  42928  aks6d1c7  42932  25or6to4  42954  235t711  43047  ex-decpmul  43048  fltnltalem  43377  sum9cubes  43387  3cubeslem3l  43400  3cubeslem3r  43401  pell1qr1  43581  rmspecfund  43619  jm2.23  43706  jm2.27c  43717  areaquad  43926  resqrtvalex  44354  imsqrtvalex  44355  brfvidRP  44397  brfvrcld  44400  corclrcl  44416  dftrcl3  44429  dfrtrcl3  44442  fvrtrcllb1d  44446  corcltrcl  44448  cotrclrcl  44451  inductionexd  44864  radcnvrat  45007  binomcxplemnn0  45042  binomcxplemfrat  45044  binomcxplemnotnn0  45049  rexanuz2nf  46189  wallispilem2  46763  wallispilem5  46766  wallispi2lem2  46769  stirlinglem5  46775  stirlinglem7  46777  stirlinglem10  46780  stirlinglem11  46781  fourierdlem48  46851  ormkglobd  47574  sin5tlem4  47596  goldratmolem2  47606  iccpartigtl  48155  iccpartlt  48156  iccpartgel  48161  fmtnosqrt  48274  fmtno1  48276  fmtno2  48285  fmtno5lem1  48288  fmtno5lem2  48289  fmtno5lem3  48290  fmtno5lem4  48291  fmtno5  48292  257prm  48296  fmtnofac1  48305  fmtno4prmfac  48307  fmtno4prmfac193  48308  fmtno4nprmfac193  48309  fmtno5faclem1  48314  fmtno5faclem2  48315  fmtno5faclem3  48316  fmtno5fac  48317  fmtno5nprm  48318  3ndvds4  48330  139prmALT  48331  31prm  48332  m5prm  48333  127prm  48334  m7prm  48335  m11nprm  48336  lighneallem2  48341  perfectALTVlem1  48469  perfectALTVlem2  48470  11t31e341  48480  2exp340mod341  48481  341fppr2  48482  8exp8mod9  48484  nfermltl8rev  48490  nfermltl2rev  48491  evengpoap3  48547  nnsum4primesevenALTV  48549  bgoldbtbndlem1  48553  bgoldbachlt  48561  tgblthelfgott  48563  cycl3grtri  48695  stgr1  48709  usgrexmpl1lem  48769  usgrexmpl2lem  48774  gpgprismgriedgdmss  48800  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem7  48849  gpgprismgr4cycllem9  48851  gpgprismgr4cycllem10  48852  grlimedgnedg  48879  nnpw2pmod  49346  dig1  49371  dignn0flhalflem2  49379  1aryfvalel  49399  itcoval1  49426  itcoval2  49427  ackval1  49444  ackval2  49445  ackval3  49446  ackendofnn0  49447  ackvalsucsucval  49451  ackval0012  49452  ackval1012  49453  ackval2012  49454  ackval3012  49455  ackval41a  49457  ackval42  49459