Theorem 1nn0 12444

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

Syntax hints:   ∈ wcel 2119  1c1 11030  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-n0 12429

This theorem is referenced by:  peano2nn0  12468  deccl  12650  10nn0  12653  numsucc  12675  numadd  12682  numaddc  12683  11multnc  12703  6p5lem  12705  6p6e12  12709  7p5e12  12712  8p4e12  12717  9p2e11  12722  9p3e12  12723  10p10e20  12730  4t4e16  12734  5t2e10  12735  5t4e20  12737  6t3e18  12740  6t4e24  12741  7t3e21  12745  7t4e28  12746  8t3e24  12751  9t3e27  12758  9t9e81  12764  xnn0n0n1ge2b  13074  fz0to3un2pr  13574  elfzom1elp1fzo  13678  fzo0sn0fzo1  13701  fvf1tp  13739  fldiv4lem1div2  13787  expn1  14024  nn0expcl  14028  sqval  14067  nn0opthlem1  14221  fac2  14232  faclbnd4lem2  14247  bccl  14275  hashsng  14322  hashen1  14323  hashrabrsn  14325  1elfz0hash  14343  hashgt23el  14377  hashprlei  14421  hashtplei  14437  tpf1ofv1  14450  tpfo  14453  wrdred1hash  14514  pfx1  14656  repsw1  14736  cshw1  14775  s3fv1  14845  s4fv1  14849  pfx2  14900  repsw2  14903  repsw3  14904  wwlktovf  14909  relexp1g  14979  relexpaddg  15006  rtrclreclem1  15010  bcxmas  15791  climcndslem2  15806  climcnds  15807  arisum  15816  geoisum1  15835  geoisum1c  15836  mertenslem2  15841  fprodnn0cl  15913  nn0risefaccl  15978  bpoly1  16007  bpoly4  16015  fsumcube  16016  ege2le3  16046  ef4p  16071  efgt1p2  16072  efgt1p  16073  sin01gt0  16148  rpnnen2lem3  16174  dvds1  16279  3dvds2dec  16293  5ndvds6  16374  bitsmod  16396  bitsinv1lem  16401  sadadd2lem  16419  sadadd  16427  sadass  16431  smupp1  16440  smumul  16453  nn0rppwr  16521  prmdvdsbc  16687  pcelnn  16832  pockthg  16868  vdwlem12  16954  prmo1  16999  dec5nprm  17028  dec2nprm  17029  modxp1i  17032  2exp8  17050  2exp11  17051  2exp16  17052  2expltfac  17054  5prm  17070  11prm  17076  13prm  17077  17prm  17078  19prm  17079  23prm  17080  prmlem2  17081  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  ocndx  17335  ocid  17336  basendxnocndx  17337  plendxnocndx  17338  dsndx  17339  dsid  17340  dsndxnn  17341  basendxltdsndx  17342  slotsdifdsndx  17348  unifndx  17349  unifid  17350  unifndxnn  17351  basendxltunifndx  17352  slotsdifunifndx  17355  odrngstr  17357  homndx  17365  homid  17366  ccondx  17367  ccoid  17368  slotsbhcdif  17369  slotsdifplendx2  17370  slotsdifocndx  17371  imasvalstr  17405  prdsvalstr  17406  catstr  17918  ipostr  18486  smndex2dnrinv  18877  cycsubmcl  19167  psgnunilem2  19461  odcau  19570  lt6abl  19861  omndmul2  20099  0ringnnzr  20497  cnfldstr  21349  nn0srg  21412  freshmansdream  21549  mvrid  21958  mvrf1  21960  mplcoe3  22014  psrbagsn  22039  evlslem1  22058  mhpvarcl  22136  psdcl  22149  psdmul  22154  psdmvr  22157  pmatcollpw3fi1lem1  22769  chfacfscmulgsum  22843  chfacfpmmulfsupp  22846  chfacfpmmulgsum  22847  chfacfpmmulgsum2  22848  cpmadugsumlemB  22857  cpmadugsumlemF  22859  dscmet  24555  ehl1eudis  25405  dveflem  25964  c1lip2  25983  itgpowd  26035  ply1remlem  26148  fta1glem1  26151  fta1blem  26154  plyid  26192  coeidp  26246  dgrid  26247  vieta1lem2  26295  vieta1  26296  aalioulem3  26318  aaliou2b  26325  dvtaylp  26353  taylthlem1  26356  taylthlem2  26357  radcnvlem2  26397  dvradcnv  26404  pserdvlem2  26411  logtayllem  26641  logtayl  26642  cxp1  26653  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  quartlem2  26840  leibpilem2  26923  log2ublem3  26930  log2ub  26931  birthday  26936  lgamcvg2  27036  gamp1  27039  issqf  27117  ppi2  27151  mumullem2  27161  sqff1o  27163  1sgmprm  27180  ppiublem2  27184  chtublem  27192  logfacbnd3  27204  logexprlim  27206  logfacrlim2  27207  perfectlem1  27210  perfectlem2  27211  bclbnd  27261  bpos1  27264  bposlem6  27270  lgsval  27282  2lgslem3a  27377  2lgslem3c  27379  rpvmasumlem  27468  log2sumbnd  27525  itvndx  28523  lngndx  28524  itvid  28525  lngid  28526  slotsinbpsd  28527  slotslnbpsd  28528  lngndxnitvndx  28529  trkgstr  28530  eengstr  29067  edgfid  29077  edgfndx  29078  edgfndxnn  29079  basendxltedgfndx  29081  usgrexmplef  29346  cusgrsizeindb1  29537  wlk1ewlk  29726  usgr2pthlem  29849  uspgrn2crct  29894  crctcshwlkn0lem5  29900  rusgrnumwwlkl1  30057  rusgrnumwwlkb1  30061  clwwlkccatlem  30077  clwwlkinwwlk  30128  umgr2cwwkdifex  30153  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  konigsbergiedgw  30336  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  konigsberglem4  30343  1kp2ke3k  30534  ex-exp  30538  ex-fac  30539  9p10ne21  30558  sgnmulsgn  32934  sgnmulsgp  32935  nexple  32936  dpmul4  32992  threehalves  32993  1mhdrd  32994  s2f1  33024  cycpm2tr  33200  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1dg1rt  33663  coe1vr1  33674  deg1vr  33675  mplmulmvr  33723  esplylem  33750  esplyfv1  33753  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  drngdimgt0  33802  rtelextdg2lem  33910  fldext2chn  33912  constrdircl  33949  iconstr  33950  2sqr3minply  33964  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminply  33972  lmat22e12  34003  lmat22e21  34004  lmat22e22  34005  madjusmdetlem4  34014  oddpwdc  34538  eulerpartlemd  34550  eulerpartlemgs2  34564  eulerpartlemn  34565  iwrdsplit  34571  fib0  34583  fib1  34584  fibp1  34585  plymulx0  34731  signstfveq0  34761  signsvvf  34763  signsvfn  34766  signshlen  34774  prodfzo03  34787  reprsuc  34799  breprexplemc  34816  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  usgrgt2cycl  35358  subfac1  35406  kur14lem9  35442  bccolsum  35967  nn0prpw  36551  12gcd5e1  42488  60gcd6e6  42489  60gcd7e1  42490  420gcd8e4  42491  12lcm5e60  42493  lcmineqlem11  42524  lcmineqlem18  42531  lcmineqlem22  42535  lcmineqlem  42537  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow5ineq2  42540  3lexlogpow5ineq4  42541  3lexlogpow5ineq5  42545  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p3  42563  aks6d1c1p8  42600  aks6d1c5lem3  42622  2np3bcnp1  42629  2ap1caineq  42630  sticksstones22  42653  aks6d1c6lem1  42655  aks6d1c7lem1  42665  aks6d1c7  42669  235t711  42782  ex-decpmul  42783  fltnltalem  43112  sum9cubes  43122  3cubeslem3l  43135  3cubeslem3r  43136  pell1qr1  43316  rmspecfund  43354  jm2.23  43441  jm2.27c  43452  areaquad  43661  resqrtvalex  44089  imsqrtvalex  44090  brfvidRP  44132  brfvrcld  44135  corclrcl  44151  dftrcl3  44164  dfrtrcl3  44177  fvrtrcllb1d  44181  corcltrcl  44183  cotrclrcl  44186  inductionexd  44599  radcnvrat  44758  binomcxplemnn0  44793  binomcxplemfrat  44795  binomcxplemnotnn0  44800  rexanuz2nf  45935  wallispilem2  46509  wallispilem5  46512  wallispi2lem2  46515  stirlinglem5  46521  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  fourierdlem48  46597  ormkglobd  47320  sin5tlem4  47339  sin5tlem5  47340  goldratmolem2  47349  iccpartigtl  47898  iccpartlt  47899  iccpartgel  47904  fmtnosqrt  48017  fmtno1  48019  fmtno2  48028  fmtno5lem1  48031  fmtno5lem2  48032  fmtno5lem3  48033  fmtno5lem4  48034  fmtno5  48035  257prm  48039  fmtnofac1  48048  fmtno4prmfac  48050  fmtno4prmfac193  48051  fmtno4nprmfac193  48052  fmtno5faclem1  48057  fmtno5faclem2  48058  fmtno5faclem3  48059  fmtno5fac  48060  fmtno5nprm  48061  3ndvds4  48073  139prmALT  48074  31prm  48075  m5prm  48076  127prm  48077  m7prm  48078  m11nprm  48079  lighneallem2  48084  perfectALTVlem1  48212  perfectALTVlem2  48213  11t31e341  48223  2exp340mod341  48224  341fppr2  48225  8exp8mod9  48227  nfermltl8rev  48233  nfermltl2rev  48234  evengpoap3  48290  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  bgoldbachlt  48304  tgblthelfgott  48306  cycl3grtri  48438  stgr1  48452  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgprismgriedgdmss  48543  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem9  48594  gpgprismgr4cycllem10  48595  grlimedgnedg  48622  nnpw2pmod  49074  dig1  49099  dignn0flhalflem2  49107  1aryfvalel  49127  itcoval1  49154  itcoval2  49155  ackval1  49172  ackval2  49173  ackval3  49174  ackendofnn0  49175  ackvalsucsucval  49179  ackval0012  49180  ackval1012  49181  ackval2012  49182  ackval3012  49183  ackval41a  49185  ackval42  49187