Theorem 1nn0 12434

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

Syntax hints:   ∈ wcel 2109  1c1 11045  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  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 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  peano2nn0  12458  deccl  12640  10nn0  12643  numsucc  12665  numadd  12672  numaddc  12673  11multnc  12693  6p5lem  12695  6p6e12  12699  7p5e12  12702  8p4e12  12707  9p2e11  12712  9p3e12  12713  10p10e20  12720  4t4e16  12724  5t2e10  12725  5t4e20  12727  6t3e18  12730  6t4e24  12731  7t3e21  12735  7t4e28  12736  8t3e24  12741  9t3e27  12748  9t9e81  12754  xnn0n0n1ge2b  13068  fz0to3un2pr  13566  elfzom1elp1fzo  13669  fzo0sn0fzo1  13692  fvf1tp  13727  fldiv4lem1div2  13775  expn1  14012  nn0expcl  14016  sqval  14055  nn0opthlem1  14209  fac2  14220  faclbnd4lem2  14235  bccl  14263  hashsng  14310  hashen1  14311  hashrabrsn  14313  1elfz0hash  14331  hashgt23el  14365  hashprlei  14409  hashtplei  14425  tpf1ofv1  14438  tpfo  14441  wrdred1hash  14502  pfx1  14644  repsw1  14724  cshw1  14763  s3fv1  14834  s4fv1  14838  pfx2  14889  repsw2  14892  repsw3  14893  wwlktovf  14898  relexp1g  14968  relexpaddg  14995  rtrclreclem1  14999  bcxmas  15777  climcndslem2  15792  climcnds  15793  arisum  15802  geoisum1  15821  geoisum1c  15822  mertenslem2  15827  fprodnn0cl  15899  nn0risefaccl  15964  bpoly1  15993  bpoly4  16001  fsumcube  16002  ege2le3  16032  ef4p  16057  efgt1p2  16058  efgt1p  16059  sin01gt0  16134  rpnnen2lem3  16160  dvds1  16265  3dvds2dec  16279  5ndvds6  16360  bitsmod  16382  bitsinv1lem  16387  sadadd2lem  16405  sadadd  16413  sadass  16417  smupp1  16426  smumul  16439  nn0rppwr  16507  prmdvdsbc  16672  pcelnn  16817  pockthg  16853  vdwlem12  16939  prmo1  16984  dec5nprm  17013  dec2nprm  17014  modxp1i  17017  2exp8  17035  2exp11  17036  2exp16  17037  2expltfac  17039  5prm  17055  11prm  17061  13prm  17062  17prm  17063  19prm  17064  23prm  17065  prmlem2  17066  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  ocndx  17320  ocid  17321  basendxnocndx  17322  plendxnocndx  17323  dsndx  17324  dsid  17325  dsndxnn  17326  basendxltdsndx  17327  slotsdifdsndx  17333  unifndx  17334  unifid  17335  unifndxnn  17336  basendxltunifndx  17337  slotsdifunifndx  17340  odrngstr  17342  homndx  17350  homid  17351  ccondx  17352  ccoid  17353  slotsbhcdif  17354  slotsdifplendx2  17355  slotsdifocndx  17356  imasvalstr  17390  prdsvalstr  17391  catstr  17898  ipostr  18464  smndex2dnrinv  18818  cycsubmcl  19109  psgnunilem2  19401  odcau  19510  lt6abl  19801  0ringnnzr  20410  cnfldstr  21242  cnfldstrOLD  21257  nn0srg  21330  freshmansdream  21460  mvrid  21869  mvrf1  21871  mplcoe3  21921  psrbagsn  21946  evlslem1  21965  mhpvarcl  22011  psdcl  22024  psdmul  22029  psdmvr  22032  pmatcollpw3fi1lem1  22649  chfacfscmulgsum  22723  chfacfpmmulfsupp  22726  chfacfpmmulgsum  22727  chfacfpmmulgsum2  22728  cpmadugsumlemB  22737  cpmadugsumlemF  22739  dscmet  24436  ehl1eudis  25296  dveflem  25859  c1lip2  25879  itgpowd  25933  ply1remlem  26046  fta1glem1  26049  fta1blem  26052  plyid  26090  coeidp  26145  dgrid  26146  vieta1lem2  26195  vieta1  26196  aalioulem3  26218  aaliou2b  26225  dvtaylp  26254  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  radcnvlem2  26299  dvradcnv  26306  pserdvlem2  26314  logtayllem  26544  logtayl  26545  cxp1  26556  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem1  26743  quartlem2  26744  leibpilem2  26827  log2ublem3  26834  log2ub  26835  birthday  26840  lgamcvg2  26941  gamp1  26944  issqf  27022  ppi2  27056  mumullem2  27066  sqff1o  27068  1sgmprm  27086  ppiublem2  27090  chtublem  27098  logfacbnd3  27110  logexprlim  27112  logfacrlim2  27113  perfectlem1  27116  perfectlem2  27117  bclbnd  27167  bpos1  27170  bposlem6  27176  lgsval  27188  2lgslem3a  27283  2lgslem3c  27285  rpvmasumlem  27374  log2sumbnd  27431  itvndx  28340  lngndx  28341  itvid  28342  lngid  28343  slotsinbpsd  28344  slotslnbpsd  28345  lngndxnitvndx  28346  trkgstr  28347  eengstr  28883  edgfid  28893  edgfndx  28894  edgfndxnn  28895  basendxltedgfndx  28897  usgrexmplef  29162  cusgrsizeindb1  29354  wlk1ewlk  29543  usgr2pthlem  29666  uspgrn2crct  29711  crctcshwlkn0lem5  29717  rusgrnumwwlkl1  29871  rusgrnumwwlkb1  29875  clwwlkccatlem  29891  clwwlkinwwlk  29942  umgr2cwwkdifex  29967  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsbergiedgw  30150  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  konigsberglem4  30157  1kp2ke3k  30348  ex-exp  30352  ex-fac  30353  9p10ne21  30372  sgnmulsgn  32740  sgnmulsgp  32741  nexple  32742  dpmul4  32807  threehalves  32808  1mhdrd  32809  s2f1  32839  omndmul2  32999  cycpm2tr  33049  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1dg1rt  33521  coe1vr1  33530  deg1vr  33531  drngdimgt0  33587  rtelextdg2lem  33689  fldext2chn  33691  constrdircl  33728  iconstr  33729  2sqr3minply  33743  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminply  33751  lmat22e12  33782  lmat22e21  33783  lmat22e22  33784  madjusmdetlem4  33793  oddpwdc  34318  eulerpartlemd  34330  eulerpartlemgs2  34344  eulerpartlemn  34345  iwrdsplit  34351  fib0  34363  fib1  34364  fibp1  34365  plymulx0  34511  signstfveq0  34541  signsvvf  34543  signsvfn  34546  signshlen  34554  prodfzo03  34567  reprsuc  34579  breprexplemc  34596  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  usgrgt2cycl  35090  subfac1  35138  kur14lem9  35174  bccolsum  35699  nn0prpw  36284  12gcd5e1  41964  60gcd6e6  41965  60gcd7e1  41966  420gcd8e4  41967  12lcm5e60  41969  lcmineqlem11  42000  lcmineqlem18  42007  lcmineqlem22  42011  lcmineqlem  42013  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow5ineq2  42016  3lexlogpow5ineq4  42017  3lexlogpow5ineq5  42021  dvrelogpow2b  42029  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p3  42039  aks6d1c1p8  42076  aks6d1c5lem3  42098  2np3bcnp1  42105  2ap1caineq  42106  sticksstones22  42129  aks6d1c6lem1  42131  aks6d1c7lem1  42141  aks6d1c7  42145  235t711  42266  ex-decpmul  42267  fltnltalem  42623  sum9cubes  42633  3cubeslem3l  42647  3cubeslem3r  42648  pell1qr1  42832  rmspecfund  42870  jm2.23  42958  jm2.27c  42969  areaquad  43178  resqrtvalex  43607  imsqrtvalex  43608  brfvidRP  43650  brfvrcld  43653  corclrcl  43669  dftrcl3  43682  dfrtrcl3  43695  fvrtrcllb1d  43699  corcltrcl  43701  cotrclrcl  43704  inductionexd  44117  radcnvrat  44276  binomcxplemnn0  44311  binomcxplemfrat  44313  binomcxplemnotnn0  44318  rexanuz2nf  45461  wallispilem2  46037  wallispilem5  46040  wallispi2lem2  46043  stirlinglem5  46049  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  fourierdlem48  46125  ormkglobd  46846  iccpartigtl  47397  iccpartlt  47398  iccpartgel  47403  fmtnosqrt  47513  fmtno1  47515  fmtno2  47524  fmtno5lem1  47527  fmtno5lem2  47528  fmtno5lem3  47529  fmtno5lem4  47530  fmtno5  47531  257prm  47535  fmtnofac1  47544  fmtno4prmfac  47546  fmtno4prmfac193  47547  fmtno4nprmfac193  47548  fmtno5faclem1  47553  fmtno5faclem2  47554  fmtno5faclem3  47555  fmtno5fac  47556  fmtno5nprm  47557  3ndvds4  47569  139prmALT  47570  31prm  47571  m5prm  47572  127prm  47573  m7prm  47574  m11nprm  47575  lighneallem2  47580  perfectALTVlem1  47695  perfectALTVlem2  47696  11t31e341  47706  2exp340mod341  47707  341fppr2  47708  8exp8mod9  47710  nfermltl8rev  47716  nfermltl2rev  47717  evengpoap3  47773  nnsum4primesevenALTV  47775  bgoldbtbndlem1  47779  bgoldbachlt  47787  tgblthelfgott  47789  cycl3grtri  47919  stgr1  47933  usgrexmpl1lem  47985  usgrexmpl2lem  47990  gpgprismgriedgdmss  48016  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem9  48066  gpgprismgr4cycllem10  48067  nnpw2pmod  48545  dig1  48570  dignn0flhalflem2  48578  1aryfvalel  48598  itcoval1  48625  itcoval2  48626  ackval1  48643  ackval2  48644  ackval3  48645  ackendofnn0  48646  ackvalsucsucval  48650  ackval0012  48651  ackval1012  48652  ackval2012  48653  ackval3012  48654  ackval41a  48656  ackval42  48658