Theorem 1nn0 12544

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

This proof depends on syntax axioms:   ∈ wcel 2145  1c1 11125  ℕ₀cn0 12528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  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 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12258  df-n0 12529

This theorem is used by:  peano2nn0  12568  deccl  12751  11nn0  12752  12nn0  12753  16nn0  12754  10nn0  12758  11nn  12761  numsucc  12781  numadd  12788  numaddc  12789  11multnc  12809  6p5lem  12811  6p6e12  12815  7p5e12  12818  8p4e12  12823  9p2e11  12828  9p3e12  12829  10p10e20  12836  4t4e16  12840  5t2e10  12841  5t4e20  12843  6t3e18  12846  6t4e24  12847  7t3e21  12851  7t4e28  12852  8t3e24  12857  9t3e27  12864  9t9e81  12870  1lt10  12881  xnn0n0n1ge2b  13183  fz0to3un2pr  13684  elfzom1elp1fzo  13788  fzo0sn0fzo1  13811  fvf1tp  13850  fldiv4lem1div2  13898  expn1  14135  nn0expcl  14139  sqval  14178  nn0opthlem1  14332  fac2  14343  faclbnd4lem2  14358  bccl  14386  hashsng  14433  hashen1  14434  hashrabrsn  14436  1elfz0hash  14454  hashgt23el  14489  hashprlei  14533  hashtplei  14549  tpf1ofv1  14562  tpfo  14565  wrdred1hash  14626  pfx1  14772  repsw1  14854  cshw1  14893  s3fv1  14963  s4fv1  14967  pfx2  15018  repsw2  15023  repsw3  15024  wwlktovf  15029  relexp1g  15099  relexpaddg  15126  rtrclreclem1  15130  sgnmulsgn  15182  bcxmas  15924  climcndslem2  15939  climcnds  15940  arisum  15949  geoisum1  15968  geoisum1c  15969  mertenslem2  15974  fprodnn0cl  16044  nn0risefaccl  16109  bpoly1  16137  bpoly4  16145  fsumcube  16146  ege2le3  16176  ef4p  16201  efgt1p2  16202  efgt1p  16203  sin01gt0  16278  rpnnen2lem3  16304  dvds1  16409  3dvds2dec  16423  5ndvds6  16504  bitsmod  16526  bitsinv1lem  16531  sadadd2lem  16549  sadadd  16557  sadass  16561  smupp1  16570  smumul  16583  nn0rppwr  16651  prmdvdsbc  16817  pcelnn  16962  pockthg  16998  vdwlem12  17084  prmo1  17129  dec5nprm  17158  dec2nprm  17159  modxp1i  17162  2exp8  17180  2exp11  17181  2exp16  17182  2expltfac  17184  5prm  17200  11prm  17207  13prm  17208  17prm  17209  19prm  17210  23prm  17211  prmlem2  17212  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  ocndx  17466  ocid  17467  basendxnocndx  17468  plendxnocndx  17469  dsndx  17470  dsid  17471  dsndxnn  17472  basendxltdsndx  17473  slotsdifdsndx  17479  unifndx  17480  unifid  17481  unifndxnn  17482  basendxltunifndx  17483  slotsdifunifndx  17486  odrngstr  17488  homndx  17496  homid  17497  ccondx  17498  ccoid  17499  slotsbhcdif  17500  slotsdifplendx2  17501  slotsdifocndx  17502  imasvalstr  17536  prdsvalstr  17537  catstr  18049  ipostr  18617  smndex2dnrinv  19027  cycsubmcl  19329  psgnunilem2  19622  odcau  19731  lt6abl  20022  omndmul2  20260  0ringnnzr  20686  cnfldstr  21587  nn0srg  21650  freshmansdream  21787  mvrid  22198  mvrf1  22200  mplcoe3  22254  psrbagsn  22279  evlslem1  22298  mhpvarcl  22376  psdcl  22389  psdmul  22394  psdmvr  22397  pmatcollpw3fi1lem1  23011  chfacfscmulgsum  23085  chfacfpmmulfsupp  23088  chfacfpmmulgsum  23089  chfacfpmmulgsum2  23090  cpmadugsumlemB  23099  cpmadugsumlemF  23101  dscmet  24798  ehl1eudis  25648  dveflem  26206  c1lip2  26225  itgpowd  26277  ply1remlem  26390  fta1glem1  26393  fta1blem  26396  plyid  26434  coeidp  26489  dgrid  26490  plyn0mulidp  26511  vieta1lem2  26543  vieta1  26544  aalioulem3  26570  aaliou2b  26577  dvtaylp  26606  taylthlem1  26609  taylthlem2  26610  radcnvlem2  26650  dvradcnv  26657  pserdvlem2  26664  logtayllem  26896  logtayl  26897  cxp1  26908  quart1cl  27091  quart1lem  27092  quart1  27093  quartlem1  27094  quartlem2  27095  leibpilem2  27178  log2ublem3  27185  log2ub  27186  birthday  27191  lgamcvg2  27291  gamp1  27294  issqf  27372  ppi2  27406  mumullem2  27416  sqff1o  27418  1sgmprm  27435  ppiublem2  27439  chtublem  27447  logfacbnd3  27459  logexprlim  27461  logfacrlim2  27462  perfectlem1  27465  perfectlem2  27466  bclbnd  27516  bpos1  27519  bposlem6  27525  lgsval  27537  2lgslem3a  27632  2lgslem3c  27634  rpvmasumlem  27723  log2sumbnd  27780  itvndx  28778  lngndx  28779  itvid  28780  lngid  28781  slotsinbpsd  28782  slotslnbpsd  28783  lngndxnitvndx  28784  trkgstr  28785  eengstr  29437  edgfid  29447  edgfndx  29448  edgfndxnn  29449  basendxltedgfndx  29451  usgrexmplef  29719  cusgrsizeindb1  29910  wlk1ewlk  30099  usgr2pthlem  30228  uspgrn2crct  30276  crctcshwlkn0lem5  30282  rusgrnumwwlkl1  30439  rusgrnumwwlkb1  30443  clwwlkccatlem  30459  clwwlkinwwlk  30510  umgr2cwwkdifex  30535  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  konigsbergiedgw  30728  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  konigsberglem4  30735  1kp2ke3k  30926  ex-exp  30930  ex-fac  30931  9p10ne21  30950  sgnmulsgp  33302  nexple  33303  dpmul4  33359  threehalves  33360  1mhdrd  33361  s2f1  33389  cycpm2tr  33559  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  ply1dg1rt  33990  coe1vr1  34001  deg1vr  34002  mplmulmvr  34049  esplylem  34076  esplyfv1  34079  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  drngdimgt0  34128  rtelextdg2lem  34236  fldext2chn  34238  constrdircl  34275  iconstr  34276  2sqr3minply  34290  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminply  34298  lmat22e12  34329  lmat22e21  34330  lmat22e22  34331  madjusmdetlem4  34340  oddpwdc  34865  eulerpartlemd  34877  eulerpartlemgs2  34891  eulerpartlemn  34892  iwrdsplit  34898  fib0  34910  fib1  34911  fibp1  34912  signstfveq0  35085  signsvvf  35087  signsvfn  35090  signshlen  35098  prodfzo03  35111  reprsuc  35123  breprexplemc  35140  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  hgt750leme  35166  usgrgt2cycl  35723  subfac1  35757  kur14lem9  35793  bccolsum  36318  nn0prpw  36942  12gcd5e1  42869  60gcd6e6  42870  60gcd7e1  42871  420gcd8e4  42872  12lcm5e60  42874  lcmineqlem11  42905  lcmineqlem18  42912  lcmineqlem22  42916  lcmineqlem  42918  3exp7  42919  3lexlogpow5ineq1  42920  3lexlogpow5ineq2  42921  3lexlogpow5ineq5  42926  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p3  42944  aks6d1c1p8  42981  aks6d1c5lem3  43003  2np3bcnp1  43010  2ap1caineq  43011  sticksstones22  43034  aks6d1c6lem1  43036  aks6d1c7lem1  43046  aks6d1c7  43050  25or6to4  43072  235t711  43180  ex-decpmul  43181  fltnltalem  43508  sum9cubes  43518  3cubeslem3l  43531  3cubeslem3r  43532  pell1qr1  43712  rmspecfund  43750  jm2.23  43837  jm2.27c  43848  areaquad  44057  resqrtvalex  44485  imsqrtvalex  44486  brfvidRP  44528  brfvrcld  44531  corclrcl  44547  dftrcl3  44560  dfrtrcl3  44573  fvrtrcllb1d  44577  corcltrcl  44579  cotrclrcl  44582  inductionexd  44995  radcnvrat  45138  binomcxplemnn0  45173  binomcxplemfrat  45175  binomcxplemnotnn0  45180  rexanuz2nf  46320  wallispilem2  46894  wallispilem5  46897  wallispi2lem2  46900  stirlinglem5  46906  stirlinglem7  46908  stirlinglem10  46911  stirlinglem11  46912  fourierdlem48  46982  ormkglobd  47705  goldratmolem2  47751  iccpartigtl  48323  iccpartlt  48324  iccpartgel  48329  fmtnosqrt  48442  fmtno1  48444  fmtno2  48453  fmtno5lem1  48456  fmtno5lem2  48457  fmtno5lem3  48458  fmtno5lem4  48459  fmtno5  48460  257prm  48464  fmtnofac1  48473  fmtno4prmfac  48475  fmtno4prmfac193  48476  fmtno4nprmfac193  48477  fmtno5faclem1  48482  fmtno5faclem2  48483  fmtno5faclem3  48484  fmtno5fac  48485  fmtno5nprm  48486  3ndvds4  48498  139prmALT  48499  31prm  48500  m5prm  48501  127prm  48502  m7prm  48503  m11nprm  48504  lighneallem2  48509  perfectALTVlem1  48637  perfectALTVlem2  48638  11t31e341  48648  2exp340mod341  48649  341fppr2  48650  8exp8mod9  48652  nfermltl8rev  48658  nfermltl2rev  48659  evengpoap3  48715  nnsum4primesevenALTV  48717  bgoldbtbndlem1  48721  bgoldbachlt  48729  tgblthelfgott  48731  cycl3grtri  48863  stgr1  48877  usgrexmpl1lem  48937  usgrexmpl2lem  48942  gpgprismgriedgdmss  48968  gpgprismgr4cycllem3  49013  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem9  49019  gpgprismgr4cycllem10  49020  grlimedgnedg  49047  nnpw2pmod  49513  dig1  49538  dignn0flhalflem2  49546  1aryfvalel  49566  itcoval1  49593  itcoval2  49594  ackval1  49611  ackval2  49612  ackval3  49613  ackendofnn0  49614  ackvalsucsucval  49618  ackval0012  49619  ackval1012  49620  ackval2012  49621  ackval3012  49622  ackval41a  49624  ackval42  49626