Theorem 1nn0 12249

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

Syntax hints:   ∈ wcel 2110  1c1 10873  ℕ₀cn0 12233

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582  ax-1cn 10930

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-om 7707  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-nn 11974  df-n0 12234

This theorem is referenced by:  peano2nn0  12273  deccl  12451  10nn0  12454  numsucc  12476  numadd  12483  numaddc  12484  11multnc  12504  6p5lem  12506  6p6e12  12510  7p5e12  12513  8p4e12  12518  9p2e11  12523  9p3e12  12524  10p10e20  12531  4t4e16  12535  5t2e10  12536  5t4e20  12538  6t3e18  12541  6t4e24  12542  7t3e21  12546  7t4e28  12547  8t3e24  12552  9t3e27  12559  9t9e81  12565  xnn0n0n1ge2b  12866  fz0to3un2pr  13357  elfzom1elp1fzo  13452  fzo0sn0fzo1  13474  fldiv4lem1div2  13555  expn1  13790  nn0expcl  13794  sqval  13833  nn0opthlem1  13980  fac2  13991  faclbnd4lem2  14006  bccl  14034  hashsng  14082  hashen1  14083  hashrabrsn  14085  1elfz0hash  14103  hashgt23el  14137  hashprlei  14180  hashtplei  14196  wrdred1hash  14262  pfx1  14414  repsw1  14494  cshw1  14533  s3fv1  14603  s4fv1  14607  pfx2  14658  repsw2  14661  repsw3  14662  wwlktovf  14669  relexp1g  14735  relexpaddg  14762  rtrclreclem1  14766  bcxmas  15545  climcndslem2  15560  climcnds  15561  arisum  15570  geoisum1  15589  geoisum1c  15590  mertenslem2  15595  fprodnn0cl  15665  nn0risefaccl  15730  bpoly1  15759  bpoly4  15767  fsumcube  15768  ege2le3  15797  ef4p  15820  efgt1p2  15821  efgt1p  15822  sin01gt0  15897  rpnnen2lem3  15923  dvds1  16026  3dvds2dec  16040  bitsmod  16141  bitsinv1lem  16146  sadadd2lem  16164  sadadd  16172  sadass  16176  smupp1  16185  smumul  16198  pcelnn  16569  pockthg  16605  vdwlem12  16691  prmo1  16736  dec5nprm  16765  dec2nprm  16766  modxp1i  16769  2exp8  16788  2exp11  16789  2exp16  16790  2expltfac  16792  5prm  16808  11prm  16814  13prm  16815  17prm  16816  19prm  16817  23prm  16818  prmlem2  16819  37prm  16820  43prm  16821  83prm  16822  139prm  16823  163prm  16824  317prm  16825  631prm  16826  1259lem1  16830  1259lem2  16831  1259lem3  16832  1259lem4  16833  1259lem5  16834  1259prm  16835  2503lem1  16836  2503lem2  16837  2503lem3  16838  2503prm  16839  4001lem1  16840  4001lem2  16841  4001lem3  16842  4001lem4  16843  4001prm  16844  ocndx  17089  ocid  17090  basendxnocndx  17091  plendxnocndx  17092  dsndx  17093  dsid  17094  dsndxnn  17095  basendxltdsndx  17096  slotsdifdsndx  17102  unifndx  17103  unifid  17104  unifndxnn  17105  basendxltunifndx  17106  slotsdifunifndx  17109  odrngstr  17111  homndx  17119  homid  17120  ccondx  17121  ccoid  17122  slotsbhcdif  17123  slotsbhcdifOLD  17124  slotsdifplendx2  17125  slotsdifocndx  17126  imasvalstr  17160  prdsvalstr  17161  oppchomfvalOLD  17422  oppcbasOLD  17427  rescbasOLD  17540  resccoOLD  17544  rescabsOLD  17546  catstr  17672  ipostr  18245  smndex2dnrinv  18552  cycsubmcl  18818  psgnunilem2  19101  odcau  19207  lt6abl  19494  mgpdsOLD  19732  sradsOLD  20454  0ringnnzr  20538  cnfldstr  20597  cnfldfunOLD  20608  nn0srg  20666  thlbasOLD  20900  thlleOLD  20902  mvrid  21190  mvrf1  21192  mplcoe3  21237  psrbagsn  21269  evlslem1  21290  mhpvarcl  21336  pmatcollpw3fi1lem1  21933  chfacfscmulgsum  22007  chfacfpmmulfsupp  22010  chfacfpmmulgsum  22011  chfacfpmmulgsum2  22012  cpmadugsumlemB  22021  cpmadugsumlemF  22023  tuslemOLD  23417  tmslemOLD  23636  dscmet  23726  tnglemOLD  23795  ehl1eudis  24582  dveflem  25141  c1lip2  25160  itgpowd  25212  ply1remlem  25325  fta1glem1  25328  fta1blem  25331  plyid  25368  coeidp  25422  dgrid  25423  vieta1lem2  25469  vieta1  25470  aalioulem3  25492  aaliou2b  25499  dvtaylp  25527  taylthlem1  25530  taylthlem2  25531  radcnvlem2  25571  dvradcnv  25578  pserdvlem2  25585  logtayllem  25812  logtayl  25813  cxp1  25824  quart1cl  26002  quart1lem  26003  quart1  26004  quartlem1  26005  quartlem2  26006  leibpilem2  26089  log2ublem3  26096  log2ub  26097  birthday  26102  lgamcvg2  26202  gamp1  26205  issqf  26283  ppi2  26317  mumullem2  26327  sqff1o  26329  1sgmprm  26345  ppiublem2  26349  chtublem  26357  logfacbnd3  26369  logexprlim  26371  logfacrlim2  26372  perfectlem1  26375  perfectlem2  26376  bclbnd  26426  bpos1  26429  bposlem6  26435  lgsval  26447  2lgslem3a  26542  2lgslem3c  26544  rpvmasumlem  26633  log2sumbnd  26690  itvndx  26796  lngndx  26797  itvid  26798  lngid  26799  slotsinbpsd  26800  slotslnbpsd  26801  lngndxnitvndx  26802  trkgstr  26803  ttgvalOLD  27235  ttglemOLD  27237  ttgbasOLD  27239  ttgdsOLD  27246  eengstr  27346  edgfid  27356  edgfndx  27357  edgfndxnn  27358  edgfndxidOLD  27360  basendxltedgfndx  27361  baseltedgfOLD  27362  usgrexmplef  27624  cusgrsizeindb1  27815  wlk1ewlk  28004  usgr2pthlem  28127  uspgrn2crct  28169  crctcshwlkn0lem5  28175  rusgrnumwwlkl1  28329  rusgrnumwwlkb1  28333  clwwlkccatlem  28349  clwwlkinwwlk  28400  umgr2cwwkdifex  28425  upgr3v3e3cycl  28540  upgr4cycl4dv4e  28545  konigsbergiedgw  28608  konigsberglem1  28612  konigsberglem2  28613  konigsberglem3  28614  konigsberglem4  28615  1kp2ke3k  28806  ex-exp  28810  ex-fac  28811  9p10ne21  28830  prmdvdsbc  31126  dpmul4  31184  threehalves  31185  1mhdrd  31186  s2f1  31215  omndmul2  31334  cycpm2tr  31382  freshmansdream  31480  drngdimgt0  31697  lmat22e12  31765  lmat22e21  31766  lmat22e22  31767  madjusmdetlem4  31776  nexple  31973  oddpwdc  32317  eulerpartlemd  32329  eulerpartlemgs2  32343  eulerpartlemn  32344  iwrdsplit  32350  fib0  32362  fib1  32363  fibp1  32364  sgnmulsgn  32512  sgnmulsgp  32513  plymulx0  32522  signstfveq0  32552  signsvvf  32554  signsvfn  32557  signshlen  32565  prodfzo03  32579  reprsuc  32591  breprexplemc  32608  hgt750lemd  32624  hgt750lem  32627  hgt750lem2  32628  hgt750leme  32634  usgrgt2cycl  33088  subfac1  33136  kur14lem9  33172  bccolsum  33701  nn0prpw  34508  12gcd5e1  40008  60gcd6e6  40009  60gcd7e1  40010  420gcd8e4  40011  12lcm5e60  40013  lcmineqlem11  40044  lcmineqlem18  40051  lcmineqlem22  40055  lcmineqlem  40057  3exp7  40058  3lexlogpow5ineq1  40059  3lexlogpow5ineq2  40060  3lexlogpow5ineq4  40061  3lexlogpow5ineq5  40065  dvrelogpow2b  40073  aks4d1p1p2  40075  aks4d1p1p4  40076  aks4d1p1p6  40078  aks4d1p1p7  40079  aks4d1p1p5  40080  aks4d1p1  40081  aks4d1p3  40083  2np3bcnp1  40097  2ap1caineq  40098  sticksstones22  40121  factwoffsmonot  40160  235t711  40316  ex-decpmul  40317  nn0rppwr  40330  fltnltalem  40496  3cubeslem3l  40505  3cubeslem3r  40506  pell1qr1  40690  rmspecfund  40728  jm2.23  40815  jm2.27c  40826  areaquad  41044  resqrtvalex  41223  imsqrtvalex  41224  brfvidRP  41266  brfvrcld  41269  corclrcl  41285  dftrcl3  41298  dfrtrcl3  41311  fvrtrcllb1d  41315  corcltrcl  41317  cotrclrcl  41320  inductionexd  41735  radcnvrat  41902  binomcxplemnn0  41937  binomcxplemfrat  41939  binomcxplemnotnn0  41944  wallispilem2  43578  wallispilem5  43581  wallispi2lem2  43584  stirlinglem5  43590  stirlinglem7  43592  stirlinglem10  43595  stirlinglem11  43596  fourierdlem48  43666  iccpartigtl  44844  iccpartlt  44845  iccpartgel  44850  fmtnosqrt  44960  fmtno1  44962  fmtno2  44971  fmtno5lem1  44974  fmtno5lem2  44975  fmtno5lem3  44976  fmtno5lem4  44977  fmtno5  44978  257prm  44982  fmtnofac1  44991  fmtno4prmfac  44993  fmtno4prmfac193  44994  fmtno4nprmfac193  44995  fmtno5faclem1  45000  fmtno5faclem2  45001  fmtno5faclem3  45002  fmtno5fac  45003  fmtno5nprm  45004  3ndvds4  45016  139prmALT  45017  31prm  45018  m5prm  45019  127prm  45020  m7prm  45021  m11nprm  45022  lighneallem2  45027  perfectALTVlem1  45142  perfectALTVlem2  45143  11t31e341  45153  2exp340mod341  45154  341fppr2  45155  8exp8mod9  45157  nfermltl8rev  45163  nfermltl2rev  45164  evengpoap3  45220  nnsum4primesevenALTV  45222  bgoldbtbndlem1  45226  bgoldbachlt  45234  tgblthelfgott  45236  nnpw2pmod  45898  dig1  45923  dignn0flhalflem2  45931  1aryfvalel  45951  itcoval1  45978  itcoval2  45979  ackval1  45996  ackval2  45997  ackval3  45998  ackendofnn0  45999  ackvalsucsucval  46003  ackval0012  46004  ackval1012  46005  ackval2012  46006  ackval3012  46007  ackval41a  46009  ackval42  46011  prstclevalOLD  46319  prstcocvalOLD  46322