Theorem 1nn0 11725

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

Syntax hints:   ∈ wcel 2050  1c1 10336  ℕ₀cn0 11707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-1cn 10393

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-nn 11440  df-n0 11708

This theorem is referenced by:  peano2nn0  11749  deccl  11926  10nn0  11929  numsucc  11952  numadd  11959  numaddc  11960  11multnc  11981  6p5lem  11983  6p6e12  11987  7p5e12  11990  8p4e12  11995  9p2e11  12000  9p3e12  12001  10p10e20  12008  4t4e16  12012  5t2e10  12013  5t4e20  12015  6t3e18  12018  6t4e24  12019  7t3e21  12023  7t4e28  12024  8t3e24  12029  9t3e27  12036  9t9e81  12042  xnn0n0n1ge2b  12343  fz0to3un2pr  12825  elfzom1elp1fzo  12919  fzo0sn0fzo1  12941  fldiv4lem1div2  13022  expn1  13254  nn0expcl  13258  sqval  13296  nn0opthlem1  13443  fac2  13454  faclbnd4lem2  13469  bccl  13497  hashsng  13544  hashen1  13545  hashrabrsn  13546  1elfz0hash  13564  hashgt23el  13598  hashprlei  13637  hashtplei  13653  wrdred1hash  13724  swrd0len0OLD  13828  swrdtrcfvOLD  13833  pfx1  13885  swrdccatwrdOLD  13903  wrdeqs1catOLD  13913  repsw1  14002  cshw1  14046  s3fv1  14116  s4fv1  14120  pfx2  14171  repsw2  14174  repsw3  14175  wwlktovf  14181  relexp1g  14246  relexpaddg  14273  rtrclreclem2  14279  bcxmas  15050  climcndslem2  15065  climcnds  15066  arisum  15075  geoisum1  15095  geoisum1c  15096  mertenslem2  15101  fprodnn0cl  15171  nn0risefaccl  15236  bpoly1  15265  bpoly4  15273  fsumcube  15274  ege2le3  15303  ef4p  15326  efgt1p2  15327  efgt1p  15328  sin01gt0  15403  rpnnen2lem3  15429  dvds1  15529  3dvds2dec  15542  bitsmod  15645  bitsinv1lem  15650  sadadd2lem  15668  sadadd  15676  sadass  15680  smupp1  15689  smumul  15702  pcelnn  16062  pockthg  16098  vdwlem12  16184  prmo1  16229  dec5nprm  16258  dec2nprm  16259  modxp1i  16262  2exp8  16279  2exp16  16280  2expltfac  16282  5prm  16298  11prm  16304  13prm  16305  17prm  16306  19prm  16307  23prm  16308  prmlem2  16309  37prm  16310  43prm  16311  83prm  16312  139prm  16313  163prm  16314  317prm  16315  631prm  16316  1259lem1  16320  1259lem2  16321  1259lem3  16322  1259lem4  16323  1259lem5  16324  1259prm  16325  2503lem1  16326  2503lem2  16327  2503lem3  16328  2503prm  16329  4001lem1  16330  4001lem2  16331  4001lem3  16332  4001lem4  16333  4001prm  16334  ocndx  16529  ocid  16530  dsndx  16531  dsid  16532  unifndx  16533  unifid  16534  odrngstr  16535  ressds  16542  homndx  16543  homid  16544  ccondx  16545  ccoid  16546  resshom  16547  ressco  16548  slotsbhcdif  16549  imasvalstr  16581  prdsvalstr  16582  oppchomfval  16842  oppcbas  16846  rescbas  16957  rescco  16960  rescabs  16961  catstr  17085  ipostr  17621  psgnunilem2  18385  odcau  18490  lt6abl  18769  mgpds  18972  srads  19680  0ringnnzr  19763  mvrid  19917  mvrf1  19919  mplcoe3  19960  psrbagsn  19988  evlslem1  20008  cnfldstr  20249  cnfldfun  20259  nn0srg  20317  thlbas  20542  thlle  20543  pmatcollpw3fi1lem1  21098  chfacfscmulgsum  21172  chfacfpmmulfsupp  21175  chfacfpmmulgsum  21176  chfacfpmmulgsum2  21177  cpmadugsumlemB  21186  cpmadugsumlemF  21188  ressunif  22574  tuslem  22579  tmslem  22795  dscmet  22885  tnglem  22952  ehl1eudis  23726  dveflem  24279  c1lip2  24298  ply1remlem  24459  fta1glem1  24462  fta1blem  24465  plyid  24502  coeidp  24556  dgrid  24557  vieta1lem2  24603  vieta1  24604  aalioulem3  24626  aaliou2b  24633  dvtaylp  24661  taylthlem1  24664  taylthlem2  24665  radcnvlem2  24705  dvradcnv  24712  pserdvlem2  24719  logtayllem  24943  logtayl  24944  cxp1  24955  quart1cl  25133  quart1lem  25134  quart1  25135  quartlem1  25136  quartlem2  25137  leibpilem2  25221  log2ublem3  25228  log2ub  25229  birthday  25234  lgamcvg2  25334  gamp1  25337  issqf  25415  ppi2  25449  mumullem2  25459  sqff1o  25461  1sgmprm  25477  ppiublem2  25481  chtublem  25489  logfacbnd3  25501  logexprlim  25503  logfacrlim2  25504  perfectlem1  25507  perfectlem2  25508  bclbnd  25558  bpos1  25561  bposlem6  25567  lgsval  25579  2lgslem3a  25674  2lgslem3c  25676  rpvmasumlem  25765  log2sumbnd  25822  itvndx  25928  lngndx  25929  itvid  25930  lngid  25931  trkgstr  25932  ttgval  26364  ttglem  26365  ttgbas  26366  ttgds  26370  eengstr  26469  edgfid  26479  edgfndxnn  26480  edgfndxid  26481  baseltedgf  26482  usgrexmplef  26744  cusgrsizeindb1  26935  wlk1ewlk  27124  usgr2pthlem  27252  uspgrn2crct  27294  crctcshwlkn0lem5  27300  rusgrnumwwlkl1  27474  rusgrnumwwlkb1  27478  clwwlkccatlem  27495  clwwlkinwwlk  27555  clwwlkinwwlkOLD  27556  umgr2cwwkdifex  27589  upgr3v3e3cycl  27709  upgr4cycl4dv4e  27714  konigsbergiedgw  27780  konigsberglem1  27784  konigsberglem2  27785  konigsberglem3  27786  konigsberglem4  27787  1kp2ke3k  28003  ex-exp  28007  ex-fac  28008  9p10ne21  28026  prmdvdsbc  30278  dpmul4  30336  threehalves  30337  1mhdrd  30338  s2f1  30363  omndmul2  30428  cycpm2tr  30448  freshmansdream  30535  drngdimgt0  30642  lmat22e12  30723  lmat22e21  30724  lmat22e22  30725  madjusmdetlem4  30734  nexple  30909  oddpwdc  31254  eulerpartlemd  31266  eulerpartlemgs2  31280  eulerpartlemn  31281  iwrdsplit  31287  iwrdsplitOLD  31288  fib0  31300  fib1  31301  fibp1  31302  sgnmulsgn  31450  sgnmulsgp  31451  plymulx0  31460  signstfveq0  31491  signstfveq0OLD  31492  signsvvf  31494  signsvfn  31497  signshlen  31505  prodfzo03  31519  reprsuc  31531  breprexplemc  31548  hgt750lemd  31564  hgt750lem  31567  hgt750lem2  31568  hgt750leme  31574  subfac1  32007  kur14lem9  32043  bccolsum  32488  nn0prpw  33189  235t711  38606  ex-decpmul  38607  nn0rppwr  38611  fltnltalem  38678  pell1qr1  38861  rmspecfund  38899  jm2.23  38986  jm2.27c  38997  itgpowd  39214  areaquad  39216  brfvidRP  39393  brfvrcld  39396  corclrcl  39412  dftrcl3  39425  dfrtrcl3  39438  fvrtrcllb1d  39442  corcltrcl  39444  cotrclrcl  39447  inductionexd  39865  radcnvrat  40059  binomcxplemnn0  40094  binomcxplemfrat  40096  binomcxplemnotnn0  40101  wallispilem2  41780  wallispilem5  41783  wallispi2lem2  41786  stirlinglem5  41792  stirlinglem7  41794  stirlinglem10  41797  stirlinglem11  41798  fourierdlem48  41868  iccpartigtl  42953  iccpartlt  42954  iccpartgel  42959  fmtnosqrt  43067  fmtno1  43069  fmtno2  43078  fmtno5lem1  43081  fmtno5lem2  43082  fmtno5lem3  43083  fmtno5lem4  43084  fmtno5  43085  257prm  43089  fmtnofac1  43098  fmtno4prmfac  43100  fmtno4prmfac193  43101  fmtno4nprmfac193  43102  fmtno5faclem1  43107  fmtno5faclem2  43108  fmtno5faclem3  43109  fmtno5fac  43110  fmtno5nprm  43111  3ndvds4  43124  139prmALT  43125  31prm  43126  m5prm  43127  127prm  43129  m7prm  43130  2exp11  43131  m11nprm  43132  lighneallem2  43137  perfectALTVlem1  43252  perfectALTVlem2  43253  11t31e341  43263  2exp340mod341  43264  341fppr2  43265  8exp8mod9  43267  nfermltl8rev  43273  nfermltl2rev  43274  evengpoap3  43330  nnsum4primesevenALTV  43332  bgoldbtbndlem1  43336  bgoldbachlt  43344  tgblthelfgott  43346  nnpw2pmod  44009  dig1  44034  dignn0flhalflem2  44042