Theorem 1nn0 12516

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 12240	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 12508	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2149  1c1 11097  ℕ₀cn0 12500

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 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154

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-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 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12230  df-n0 12501

This theorem is referenced by:  peano2nn0  12540  deccl  12722  11nn0  12723  12nn0  12724  16nn0  12725  10nn0  12729  11nn  12732  numsucc  12752  numadd  12759  numaddc  12760  11multnc  12780  6p5lem  12782  6p6e12  12786  7p5e12  12789  8p4e12  12794  9p2e11  12799  9p3e12  12800  10p10e20  12807  4t4e16  12811  5t2e10  12812  5t4e20  12814  6t3e18  12817  6t4e24  12818  7t3e21  12822  7t4e28  12823  8t3e24  12828  9t3e27  12835  9t9e81  12841  1lt10  12852  xnn0n0n1ge2b  13153  fz0to3un2pr  13653  elfzom1elp1fzo  13757  fzo0sn0fzo1  13780  fvf1tp  13818  fldiv4lem1div2  13866  expn1  14103  nn0expcl  14107  sqval  14146  nn0opthlem1  14300  fac2  14311  faclbnd4lem2  14326  bccl  14354  hashsng  14401  hashen1  14402  hashrabrsn  14404  1elfz0hash  14422  hashgt23el  14457  hashprlei  14501  hashtplei  14517  tpf1ofv1  14530  tpfo  14533  wrdred1hash  14594  pfx1  14736  repsw1  14816  cshw1  14855  s3fv1  14925  s4fv1  14929  pfx2  14980  repsw2  14983  repsw3  14984  wwlktovf  14989  relexp1g  15059  relexpaddg  15086  rtrclreclem1  15090  sgnmulsgn  15142  bcxmas  15885  climcndslem2  15900  climcnds  15901  arisum  15910  geoisum1  15929  geoisum1c  15930  mertenslem2  15935  fprodnn0cl  16007  nn0risefaccl  16072  bpoly1  16101  bpoly4  16109  fsumcube  16110  ege2le3  16140  ef4p  16165  efgt1p2  16166  efgt1p  16167  sin01gt0  16242  rpnnen2lem3  16268  dvds1  16373  3dvds2dec  16387  5ndvds6  16468  bitsmod  16490  bitsinv1lem  16495  sadadd2lem  16513  sadadd  16521  sadass  16525  smupp1  16534  smumul  16547  nn0rppwr  16615  prmdvdsbc  16781  pcelnn  16926  pockthg  16962  vdwlem12  17048  prmo1  17093  dec5nprm  17122  dec2nprm  17123  modxp1i  17126  2exp8  17144  2exp11  17145  2exp16  17146  2expltfac  17148  5prm  17164  11prm  17171  13prm  17172  17prm  17173  19prm  17174  23prm  17175  prmlem2  17176  37prm  17177  43prm  17178  83prm  17179  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  1259prm  17192  2503lem1  17193  2503lem2  17194  2503lem3  17195  2503prm  17196  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  4001prm  17201  ocndx  17430  ocid  17431  basendxnocndx  17432  plendxnocndx  17433  dsndx  17434  dsid  17435  dsndxnn  17436  basendxltdsndx  17437  slotsdifdsndx  17443  unifndx  17444  unifid  17445  unifndxnn  17446  basendxltunifndx  17447  slotsdifunifndx  17450  odrngstr  17452  homndx  17460  homid  17461  ccondx  17462  ccoid  17463  slotsbhcdif  17464  slotsdifplendx2  17465  slotsdifocndx  17466  imasvalstr  17500  prdsvalstr  17501  catstr  18013  ipostr  18581  smndex2dnrinv  18973  cycsubmcl  19268  psgnunilem2  19561  odcau  19670  lt6abl  19961  omndmul2  20199  0ringnnzr  20605  cnfldstr  21489  nn0srg  21552  freshmansdream  21689  mvrid  22098  mvrf1  22100  mplcoe3  22154  psrbagsn  22179  evlslem1  22198  mhpvarcl  22276  psdcl  22289  psdmul  22294  psdmvr  22297  pmatcollpw3fi1lem1  22908  chfacfscmulgsum  22982  chfacfpmmulfsupp  22985  chfacfpmmulgsum  22986  chfacfpmmulgsum2  22987  cpmadugsumlemB  22996  cpmadugsumlemF  22998  dscmet  24694  ehl1eudis  25544  dveflem  26103  c1lip2  26122  itgpowd  26174  ply1remlem  26287  fta1glem1  26290  fta1blem  26293  plyid  26331  coeidp  26385  dgrid  26386  plyn0mulidp  26407  vieta1lem2  26437  vieta1  26438  aalioulem3  26460  aaliou2b  26467  dvtaylp  26495  taylthlem1  26498  taylthlem2  26499  radcnvlem2  26539  dvradcnv  26546  pserdvlem2  26553  logtayllem  26786  logtayl  26787  cxp1  26798  quart1cl  26981  quart1lem  26982  quart1  26983  quartlem1  26984  quartlem2  26985  leibpilem2  27068  log2ublem3  27075  log2ub  27076  birthday  27081  lgamcvg2  27181  gamp1  27184  issqf  27262  ppi2  27296  mumullem2  27306  sqff1o  27308  1sgmprm  27325  ppiublem2  27329  chtublem  27337  logfacbnd3  27349  logexprlim  27351  logfacrlim2  27352  perfectlem1  27355  perfectlem2  27356  bclbnd  27406  bpos1  27409  bposlem6  27415  lgsval  27427  2lgslem3a  27522  2lgslem3c  27524  rpvmasumlem  27613  log2sumbnd  27670  itvndx  28668  lngndx  28669  itvid  28670  lngid  28671  slotsinbpsd  28672  slotslnbpsd  28673  lngndxnitvndx  28674  trkgstr  28675  eengstr  29267  edgfid  29277  edgfndx  29278  edgfndxnn  29279  basendxltedgfndx  29281  usgrexmplef  29546  cusgrsizeindb1  29737  wlk1ewlk  29926  usgr2pthlem  30049  uspgrn2crct  30094  crctcshwlkn0lem5  30100  rusgrnumwwlkl1  30257  rusgrnumwwlkb1  30261  clwwlkccatlem  30277  clwwlkinwwlk  30328  umgr2cwwkdifex  30353  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  konigsbergiedgw  30536  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  konigsberglem4  30543  1kp2ke3k  30734  ex-exp  30738  ex-fac  30739  9p10ne21  30758  sgnmulsgp  33113  nexple  33114  dpmul4  33170  threehalves  33171  1mhdrd  33172  s2f1  33202  cycpm2tr  33376  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  ply1dg1rt  33811  coe1vr1  33822  deg1vr  33823  mplmulmvr  33870  esplylem  33897  esplyfv1  33900  esplyfval1  33904  esplyfvaln  33905  esplyind  33906  drngdimgt0  33949  rtelextdg2lem  34057  fldext2chn  34059  constrdircl  34096  iconstr  34097  2sqr3minply  34111  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminply  34119  lmat22e12  34150  lmat22e21  34151  lmat22e22  34152  madjusmdetlem4  34161  oddpwdc  34685  eulerpartlemd  34697  eulerpartlemgs2  34711  eulerpartlemn  34712  iwrdsplit  34718  fib0  34730  fib1  34731  fibp1  34732  signstfveq0  34905  signsvvf  34907  signsvfn  34910  signshlen  34918  prodfzo03  34931  reprsuc  34943  breprexplemc  34960  hgt750lemd  34976  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  usgrgt2cycl  35517  subfac1  35565  kur14lem9  35601  bccolsum  36126  nn0prpw  36719  12gcd5e1  42655  60gcd6e6  42656  60gcd7e1  42657  420gcd8e4  42658  12lcm5e60  42660  lcmineqlem11  42691  lcmineqlem18  42698  lcmineqlem22  42702  lcmineqlem  42704  3exp7  42705  3lexlogpow5ineq1  42706  3lexlogpow5ineq2  42707  3lexlogpow5ineq5  42712  dvrelogpow2b  42720  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p3  42730  aks6d1c1p8  42767  aks6d1c5lem3  42789  2np3bcnp1  42796  2ap1caineq  42797  sticksstones22  42820  aks6d1c6lem1  42822  aks6d1c7lem1  42832  aks6d1c7  42836  235t711  42949  ex-decpmul  42950  fltnltalem  43279  sum9cubes  43289  3cubeslem3l  43302  3cubeslem3r  43303  pell1qr1  43483  rmspecfund  43521  jm2.23  43608  jm2.27c  43619  areaquad  43828  resqrtvalex  44256  imsqrtvalex  44257  brfvidRP  44299  brfvrcld  44302  corclrcl  44318  dftrcl3  44331  dfrtrcl3  44344  fvrtrcllb1d  44348  corcltrcl  44350  cotrclrcl  44353  inductionexd  44766  radcnvrat  44909  binomcxplemnn0  44944  binomcxplemfrat  44946  binomcxplemnotnn0  44951  rexanuz2nf  46091  wallispilem2  46665  wallispilem5  46668  wallispi2lem2  46671  stirlinglem5  46677  stirlinglem7  46679  stirlinglem10  46682  stirlinglem11  46683  fourierdlem48  46753  ormkglobd  47476  sin5tlem4  47495  goldratmolem2  47505  iccpartigtl  48054  iccpartlt  48055  iccpartgel  48060  fmtnosqrt  48173  fmtno1  48175  fmtno2  48184  fmtno5lem1  48187  fmtno5lem2  48188  fmtno5lem3  48189  fmtno5lem4  48190  fmtno5  48191  257prm  48195  fmtnofac1  48204  fmtno4prmfac  48206  fmtno4prmfac193  48207  fmtno4nprmfac193  48208  fmtno5faclem1  48213  fmtno5faclem2  48214  fmtno5faclem3  48215  fmtno5fac  48216  fmtno5nprm  48217  3ndvds4  48229  139prmALT  48230  31prm  48231  m5prm  48232  127prm  48233  m7prm  48234  m11nprm  48235  lighneallem2  48240  perfectALTVlem1  48368  perfectALTVlem2  48369  11t31e341  48379  2exp340mod341  48380  341fppr2  48381  8exp8mod9  48383  nfermltl8rev  48389  nfermltl2rev  48390  evengpoap3  48446  nnsum4primesevenALTV  48448  bgoldbtbndlem1  48452  bgoldbachlt  48460  tgblthelfgott  48462  cycl3grtri  48594  stgr1  48608  usgrexmpl1lem  48668  usgrexmpl2lem  48673  gpgprismgriedgdmss  48699  gpgprismgr4cycllem3  48744  gpgprismgr4cycllem7  48748  gpgprismgr4cycllem9  48750  gpgprismgr4cycllem10  48751  grlimedgnedg  48778  nnpw2pmod  49241  dig1  49266  dignn0flhalflem2  49274  1aryfvalel  49294  itcoval1  49321  itcoval2  49322  ackval1  49339  ackval2  49340  ackval3  49341  ackendofnn0  49342  ackvalsucsucval  49346  ackval0012  49347  ackval1012  49348  ackval2012  49349  ackval3012  49350  ackval41a  49352  ackval42  49354