Theorem 1nn0 12453

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

Syntax hints:   ∈ wcel 2114  1c1 11039  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-n0 12438

This theorem is referenced by:  peano2nn0  12477  deccl  12659  10nn0  12662  numsucc  12684  numadd  12691  numaddc  12692  11multnc  12712  6p5lem  12714  6p6e12  12718  7p5e12  12721  8p4e12  12726  9p2e11  12731  9p3e12  12732  10p10e20  12739  4t4e16  12743  5t2e10  12744  5t4e20  12746  6t3e18  12749  6t4e24  12750  7t3e21  12754  7t4e28  12755  8t3e24  12760  9t3e27  12767  9t9e81  12773  xnn0n0n1ge2b  13083  fz0to3un2pr  13583  elfzom1elp1fzo  13687  fzo0sn0fzo1  13710  fvf1tp  13748  fldiv4lem1div2  13796  expn1  14033  nn0expcl  14037  sqval  14076  nn0opthlem1  14230  fac2  14241  faclbnd4lem2  14256  bccl  14284  hashsng  14331  hashen1  14332  hashrabrsn  14334  1elfz0hash  14352  hashgt23el  14386  hashprlei  14430  hashtplei  14446  tpf1ofv1  14459  tpfo  14462  wrdred1hash  14523  pfx1  14665  repsw1  14745  cshw1  14784  s3fv1  14854  s4fv1  14858  pfx2  14909  repsw2  14912  repsw3  14913  wwlktovf  14918  relexp1g  14988  relexpaddg  15015  rtrclreclem1  15019  bcxmas  15800  climcndslem2  15815  climcnds  15816  arisum  15825  geoisum1  15844  geoisum1c  15845  mertenslem2  15850  fprodnn0cl  15922  nn0risefaccl  15987  bpoly1  16016  bpoly4  16024  fsumcube  16025  ege2le3  16055  ef4p  16080  efgt1p2  16081  efgt1p  16082  sin01gt0  16157  rpnnen2lem3  16183  dvds1  16288  3dvds2dec  16302  5ndvds6  16383  bitsmod  16405  bitsinv1lem  16410  sadadd2lem  16428  sadadd  16436  sadass  16440  smupp1  16449  smumul  16462  nn0rppwr  16530  prmdvdsbc  16696  pcelnn  16841  pockthg  16877  vdwlem12  16963  prmo1  17008  dec5nprm  17037  dec2nprm  17038  modxp1i  17041  2exp8  17059  2exp11  17060  2exp16  17061  2expltfac  17063  5prm  17079  11prm  17085  13prm  17086  17prm  17087  19prm  17088  23prm  17089  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  ocndx  17344  ocid  17345  basendxnocndx  17346  plendxnocndx  17347  dsndx  17348  dsid  17349  dsndxnn  17350  basendxltdsndx  17351  slotsdifdsndx  17357  unifndx  17358  unifid  17359  unifndxnn  17360  basendxltunifndx  17361  slotsdifunifndx  17364  odrngstr  17366  homndx  17374  homid  17375  ccondx  17376  ccoid  17377  slotsbhcdif  17378  slotsdifplendx2  17379  slotsdifocndx  17380  imasvalstr  17414  prdsvalstr  17415  catstr  17927  ipostr  18495  smndex2dnrinv  18886  cycsubmcl  19176  psgnunilem2  19470  odcau  19579  lt6abl  19870  omndmul2  20108  0ringnnzr  20502  cnfldstr  21354  nn0srg  21417  freshmansdream  21554  mvrid  21962  mvrf1  21964  mplcoe3  22016  psrbagsn  22041  evlslem1  22060  mhpvarcl  22114  psdcl  22127  psdmul  22132  psdmvr  22135  pmatcollpw3fi1lem1  22751  chfacfscmulgsum  22825  chfacfpmmulfsupp  22828  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cpmadugsumlemB  22839  cpmadugsumlemF  22841  dscmet  24537  ehl1eudis  25387  dveflem  25946  c1lip2  25965  itgpowd  26017  ply1remlem  26130  fta1glem1  26133  fta1blem  26136  plyid  26174  coeidp  26228  dgrid  26229  vieta1lem2  26277  vieta1  26278  aalioulem3  26300  aaliou2b  26307  dvtaylp  26335  taylthlem1  26338  taylthlem2  26339  radcnvlem2  26379  dvradcnv  26386  pserdvlem2  26393  logtayllem  26623  logtayl  26624  cxp1  26635  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  leibpilem2  26905  log2ublem3  26912  log2ub  26913  birthday  26918  lgamcvg2  27018  gamp1  27021  issqf  27099  ppi2  27133  mumullem2  27143  sqff1o  27145  1sgmprm  27162  ppiublem2  27166  chtublem  27174  logfacbnd3  27186  logexprlim  27188  logfacrlim2  27189  perfectlem1  27192  perfectlem2  27193  bclbnd  27243  bpos1  27246  bposlem6  27252  lgsval  27264  2lgslem3a  27359  2lgslem3c  27361  rpvmasumlem  27450  log2sumbnd  27507  itvndx  28505  lngndx  28506  itvid  28507  lngid  28508  slotsinbpsd  28509  slotslnbpsd  28510  lngndxnitvndx  28511  trkgstr  28512  eengstr  29049  edgfid  29059  edgfndx  29060  edgfndxnn  29061  basendxltedgfndx  29063  usgrexmplef  29328  cusgrsizeindb1  29519  wlk1ewlk  29708  usgr2pthlem  29831  uspgrn2crct  29876  crctcshwlkn0lem5  29882  rusgrnumwwlkl1  30039  rusgrnumwwlkb1  30043  clwwlkccatlem  30059  clwwlkinwwlk  30110  umgr2cwwkdifex  30135  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberglem4  30325  1kp2ke3k  30516  ex-exp  30520  ex-fac  30521  9p10ne21  30540  sgnmulsgn  32915  sgnmulsgp  32916  nexple  32917  dpmul4  32973  threehalves  32974  1mhdrd  32975  s2f1  33005  cycpm2tr  33180  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1dg1rt  33640  coe1vr1  33651  deg1vr  33652  mplmulmvr  33683  esplylem  33710  esplyfv1  33713  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  drngdimgt0  33762  rtelextdg2lem  33870  fldext2chn  33872  constrdircl  33909  iconstr  33910  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminply  33932  lmat22e12  33963  lmat22e21  33964  lmat22e22  33965  madjusmdetlem4  33974  oddpwdc  34498  eulerpartlemd  34510  eulerpartlemgs2  34524  eulerpartlemn  34525  iwrdsplit  34531  fib0  34543  fib1  34544  fibp1  34545  plymulx0  34691  signstfveq0  34721  signsvvf  34723  signsvfn  34726  signshlen  34734  prodfzo03  34747  reprsuc  34759  breprexplemc  34776  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  usgrgt2cycl  35312  subfac1  35360  kur14lem9  35396  bccolsum  35921  nn0prpw  36505  12gcd5e1  42442  60gcd6e6  42443  60gcd7e1  42444  420gcd8e4  42445  12lcm5e60  42447  lcmineqlem11  42478  lcmineqlem18  42485  lcmineqlem22  42489  lcmineqlem  42491  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq5  42499  dvrelogpow2b  42507  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p3  42517  aks6d1c1p8  42554  aks6d1c5lem3  42576  2np3bcnp1  42583  2ap1caineq  42584  sticksstones22  42607  aks6d1c6lem1  42609  aks6d1c7lem1  42619  aks6d1c7  42623  235t711  42737  ex-decpmul  42738  fltnltalem  43095  sum9cubes  43105  3cubeslem3l  43118  3cubeslem3r  43119  pell1qr1  43299  rmspecfund  43337  jm2.23  43424  jm2.27c  43435  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  brfvidRP  44115  brfvrcld  44118  corclrcl  44134  dftrcl3  44147  dfrtrcl3  44160  fvrtrcllb1d  44164  corcltrcl  44166  cotrclrcl  44169  inductionexd  44582  radcnvrat  44741  binomcxplemnn0  44776  binomcxplemfrat  44778  binomcxplemnotnn0  44783  rexanuz2nf  45920  wallispilem2  46494  wallispilem5  46497  wallispi2lem2  46500  stirlinglem5  46506  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  fourierdlem48  46582  ormkglobd  47305  sin5tlem4  47324  sin5tlem5  47325  goldratmolem2  47334  iccpartigtl  47883  iccpartlt  47884  iccpartgel  47889  fmtnosqrt  48002  fmtno1  48004  fmtno2  48013  fmtno5lem1  48016  fmtno5lem2  48017  fmtno5lem3  48018  fmtno5lem4  48019  fmtno5  48020  257prm  48024  fmtnofac1  48033  fmtno4prmfac  48035  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  fmtno5faclem1  48042  fmtno5faclem2  48043  fmtno5faclem3  48044  fmtno5fac  48045  fmtno5nprm  48046  3ndvds4  48058  139prmALT  48059  31prm  48060  m5prm  48061  127prm  48062  m7prm  48063  m11nprm  48064  lighneallem2  48069  perfectALTVlem1  48197  perfectALTVlem2  48198  11t31e341  48208  2exp340mod341  48209  341fppr2  48210  8exp8mod9  48212  nfermltl8rev  48218  nfermltl2rev  48219  evengpoap3  48275  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  bgoldbachlt  48289  tgblthelfgott  48291  cycl3grtri  48423  stgr1  48437  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgprismgriedgdmss  48528  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem9  48579  gpgprismgr4cycllem10  48580  grlimedgnedg  48607  nnpw2pmod  49059  dig1  49084  dignn0flhalflem2  49092  1aryfvalel  49112  itcoval1  49139  itcoval2  49140  ackval1  49157  ackval2  49158  ackval3  49159  ackendofnn0  49160  ackvalsucsucval  49164  ackval0012  49165  ackval1012  49166  ackval2012  49167  ackval3012  49168  ackval41a  49170  ackval42  49172