Theorem 1nn0 11914

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

Syntax hints:   ∈ wcel 2114  1c1 10538  ℕ₀cn0 11898

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-n0 11899

This theorem is referenced by:  peano2nn0  11938  deccl  12114  10nn0  12117  numsucc  12139  numadd  12146  numaddc  12147  11multnc  12167  6p5lem  12169  6p6e12  12173  7p5e12  12176  8p4e12  12181  9p2e11  12186  9p3e12  12187  10p10e20  12194  4t4e16  12198  5t2e10  12199  5t4e20  12201  6t3e18  12204  6t4e24  12205  7t3e21  12209  7t4e28  12210  8t3e24  12215  9t3e27  12222  9t9e81  12228  xnn0n0n1ge2b  12527  fz0to3un2pr  13010  elfzom1elp1fzo  13105  fzo0sn0fzo1  13127  fldiv4lem1div2  13208  expn1  13440  nn0expcl  13444  sqval  13482  nn0opthlem1  13629  fac2  13640  faclbnd4lem2  13655  bccl  13683  hashsng  13731  hashen1  13732  hashrabrsn  13734  1elfz0hash  13752  hashgt23el  13786  hashprlei  13827  hashtplei  13843  wrdred1hash  13913  pfx1  14065  repsw1  14145  cshw1  14184  s3fv1  14254  s4fv1  14258  pfx2  14309  repsw2  14312  repsw3  14313  wwlktovf  14320  relexp1g  14385  relexpaddg  14412  rtrclreclem2  14418  bcxmas  15190  climcndslem2  15205  climcnds  15206  arisum  15215  geoisum1  15235  geoisum1c  15236  mertenslem2  15241  fprodnn0cl  15311  nn0risefaccl  15376  bpoly1  15405  bpoly4  15413  fsumcube  15414  ege2le3  15443  ef4p  15466  efgt1p2  15467  efgt1p  15468  sin01gt0  15543  rpnnen2lem3  15569  dvds1  15669  3dvds2dec  15682  bitsmod  15785  bitsinv1lem  15790  sadadd2lem  15808  sadadd  15816  sadass  15820  smupp1  15829  smumul  15842  pcelnn  16206  pockthg  16242  vdwlem12  16328  prmo1  16373  dec5nprm  16402  dec2nprm  16403  modxp1i  16406  2exp8  16423  2exp16  16424  2expltfac  16426  5prm  16442  11prm  16448  13prm  16449  17prm  16450  19prm  16451  23prm  16452  prmlem2  16453  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  ocndx  16673  ocid  16674  dsndx  16675  dsid  16676  unifndx  16677  unifid  16678  odrngstr  16679  ressds  16686  homndx  16687  homid  16688  ccondx  16689  ccoid  16690  resshom  16691  ressco  16692  slotsbhcdif  16693  imasvalstr  16725  prdsvalstr  16726  oppchomfval  16984  oppcbas  16988  rescbas  17099  rescco  17102  rescabs  17103  catstr  17227  ipostr  17763  smndex2dnrinv  18080  cycsubmcl  18344  psgnunilem2  18623  odcau  18729  lt6abl  19015  mgpds  19249  srads  19958  0ringnnzr  20042  mvrid  20203  mvrf1  20205  mplcoe3  20247  psrbagsn  20275  evlslem1  20295  cnfldstr  20547  cnfldfun  20557  nn0srg  20615  thlbas  20840  thlle  20841  pmatcollpw3fi1lem1  21394  chfacfscmulgsum  21468  chfacfpmmulfsupp  21471  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cpmadugsumlemB  21482  cpmadugsumlemF  21484  ressunif  22871  tuslem  22876  tmslem  23092  dscmet  23182  tnglem  23249  ehl1eudis  24023  dveflem  24576  c1lip2  24595  ply1remlem  24756  fta1glem1  24759  fta1blem  24762  plyid  24799  coeidp  24853  dgrid  24854  vieta1lem2  24900  vieta1  24901  aalioulem3  24923  aaliou2b  24930  dvtaylp  24958  taylthlem1  24961  taylthlem2  24962  radcnvlem2  25002  dvradcnv  25009  pserdvlem2  25016  logtayllem  25242  logtayl  25243  cxp1  25254  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  leibpilem2  25519  log2ublem3  25526  log2ub  25527  birthday  25532  lgamcvg2  25632  gamp1  25635  issqf  25713  ppi2  25747  mumullem2  25757  sqff1o  25759  1sgmprm  25775  ppiublem2  25779  chtublem  25787  logfacbnd3  25799  logexprlim  25801  logfacrlim2  25802  perfectlem1  25805  perfectlem2  25806  bclbnd  25856  bpos1  25859  bposlem6  25865  lgsval  25877  2lgslem3a  25972  2lgslem3c  25974  rpvmasumlem  26063  log2sumbnd  26120  itvndx  26226  lngndx  26227  itvid  26228  lngid  26229  trkgstr  26230  ttgval  26661  ttglem  26662  ttgbas  26663  ttgds  26667  eengstr  26766  edgfid  26776  edgfndxnn  26777  edgfndxid  26778  baseltedgf  26779  usgrexmplef  27041  cusgrsizeindb1  27232  wlk1ewlk  27421  usgr2pthlem  27544  uspgrn2crct  27586  crctcshwlkn0lem5  27592  rusgrnumwwlkl1  27747  rusgrnumwwlkb1  27751  clwwlkccatlem  27767  clwwlkinwwlk  27818  umgr2cwwkdifex  27844  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  konigsbergiedgw  28027  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  konigsberglem4  28034  1kp2ke3k  28225  ex-exp  28229  ex-fac  28230  9p10ne21  28249  prmdvdsbc  30532  dpmul4  30590  threehalves  30591  1mhdrd  30592  s2f1  30621  omndmul2  30713  cycpm2tr  30761  freshmansdream  30859  drngdimgt0  31016  lmat22e12  31084  lmat22e21  31085  lmat22e22  31086  madjusmdetlem4  31095  nexple  31268  oddpwdc  31612  eulerpartlemd  31624  eulerpartlemgs2  31638  eulerpartlemn  31639  iwrdsplit  31645  fib0  31657  fib1  31658  fibp1  31659  sgnmulsgn  31807  sgnmulsgp  31808  plymulx0  31817  signstfveq0  31847  signsvvf  31849  signsvfn  31852  signshlen  31860  prodfzo03  31874  reprsuc  31886  breprexplemc  31903  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  usgrgt2cycl  32377  subfac1  32425  kur14lem9  32461  bccolsum  32971  nn0prpw  33671  factwoffsmonot  39118  235t711  39197  ex-decpmul  39198  nn0rppwr  39202  fltnltalem  39294  3cubeslem3l  39303  3cubeslem3r  39304  pell1qr1  39488  rmspecfund  39526  jm2.23  39613  jm2.27c  39624  itgpowd  39841  areaquad  39843  brfvidRP  40053  brfvrcld  40056  corclrcl  40072  dftrcl3  40085  dfrtrcl3  40098  fvrtrcllb1d  40102  corcltrcl  40104  cotrclrcl  40107  inductionexd  40525  radcnvrat  40666  binomcxplemnn0  40701  binomcxplemfrat  40703  binomcxplemnotnn0  40708  wallispilem2  42371  wallispilem5  42374  wallispi2lem2  42377  stirlinglem5  42383  stirlinglem7  42385  stirlinglem10  42388  stirlinglem11  42389  fourierdlem48  42459  iccpartigtl  43603  iccpartlt  43604  iccpartgel  43609  fmtnosqrt  43721  fmtno1  43723  fmtno2  43732  fmtno5lem1  43735  fmtno5lem2  43736  fmtno5lem3  43737  fmtno5lem4  43738  fmtno5  43739  257prm  43743  fmtnofac1  43752  fmtno4prmfac  43754  fmtno4prmfac193  43755  fmtno4nprmfac193  43756  fmtno5faclem1  43761  fmtno5faclem2  43762  fmtno5faclem3  43763  fmtno5fac  43764  fmtno5nprm  43765  3ndvds4  43778  139prmALT  43779  31prm  43780  m5prm  43781  127prm  43783  m7prm  43784  2exp11  43785  m11nprm  43786  lighneallem2  43791  perfectALTVlem1  43906  perfectALTVlem2  43907  11t31e341  43917  2exp340mod341  43918  341fppr2  43919  8exp8mod9  43921  nfermltl8rev  43927  nfermltl2rev  43928  evengpoap3  43984  nnsum4primesevenALTV  43986  bgoldbtbndlem1  43990  bgoldbachlt  43998  tgblthelfgott  44000  nnpw2pmod  44663  dig1  44688  dignn0flhalflem2  44696