Theorem 1nn0 12491

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

Syntax hints:   ∈ wcel 2141  1c1 11068  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205  df-n0 12476

This theorem is referenced by:  peano2nn0  12515  deccl  12697  11nn0  12698  12nn0  12699  16nn0  12700  10nn0  12704  11nn  12707  numsucc  12727  numadd  12734  numaddc  12735  11multnc  12755  6p5lem  12757  6p6e12  12761  7p5e12  12764  8p4e12  12769  9p2e11  12774  9p3e12  12775  10p10e20  12782  4t4e16  12786  5t2e10  12787  5t4e20  12789  6t3e18  12792  6t4e24  12793  7t3e21  12797  7t4e28  12798  8t3e24  12803  9t3e27  12810  9t9e81  12816  1lt10  12827  xnn0n0n1ge2b  13128  fz0to3un2pr  13628  elfzom1elp1fzo  13732  fzo0sn0fzo1  13755  fvf1tp  13793  fldiv4lem1div2  13841  expn1  14078  nn0expcl  14082  sqval  14121  nn0opthlem1  14275  fac2  14286  faclbnd4lem2  14301  bccl  14329  hashsng  14376  hashen1  14377  hashrabrsn  14379  1elfz0hash  14397  hashgt23el  14431  hashprlei  14475  hashtplei  14491  tpf1ofv1  14504  tpfo  14507  wrdred1hash  14568  pfx1  14710  repsw1  14790  cshw1  14829  s3fv1  14899  s4fv1  14903  pfx2  14954  repsw2  14957  repsw3  14958  wwlktovf  14963  relexp1g  15033  relexpaddg  15060  rtrclreclem1  15064  sgnmulsgn  15113  bcxmas  15856  climcndslem2  15871  climcnds  15872  arisum  15881  geoisum1  15900  geoisum1c  15901  mertenslem2  15906  fprodnn0cl  15978  nn0risefaccl  16043  bpoly1  16072  bpoly4  16080  fsumcube  16081  ege2le3  16111  ef4p  16136  efgt1p2  16137  efgt1p  16138  sin01gt0  16213  rpnnen2lem3  16239  dvds1  16344  3dvds2dec  16358  5ndvds6  16439  bitsmod  16461  bitsinv1lem  16466  sadadd2lem  16484  sadadd  16492  sadass  16496  smupp1  16505  smumul  16518  nn0rppwr  16586  prmdvdsbc  16752  pcelnn  16897  pockthg  16933  vdwlem12  17019  prmo1  17064  dec5nprm  17093  dec2nprm  17094  modxp1i  17097  2exp8  17115  2exp11  17116  2exp16  17117  2expltfac  17119  5prm  17135  11prm  17142  13prm  17143  17prm  17144  19prm  17145  23prm  17146  prmlem2  17147  37prm  17148  43prm  17149  83prm  17150  139prm  17151  163prm  17152  317prm  17153  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  1259prm  17163  2503lem1  17164  2503lem2  17165  2503lem3  17166  2503prm  17167  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  4001prm  17172  ocndx  17401  ocid  17402  basendxnocndx  17403  plendxnocndx  17404  dsndx  17405  dsid  17406  dsndxnn  17407  basendxltdsndx  17408  slotsdifdsndx  17414  unifndx  17415  unifid  17416  unifndxnn  17417  basendxltunifndx  17418  slotsdifunifndx  17421  odrngstr  17423  homndx  17431  homid  17432  ccondx  17433  ccoid  17434  slotsbhcdif  17435  slotsdifplendx2  17436  slotsdifocndx  17437  imasvalstr  17471  prdsvalstr  17472  catstr  17984  ipostr  18552  smndex2dnrinv  18943  cycsubmcl  19233  psgnunilem2  19526  odcau  19635  lt6abl  19926  omndmul2  20164  0ringnnzr  20562  cnfldstr  21414  nn0srg  21477  freshmansdream  21614  mvrid  22023  mvrf1  22025  mplcoe3  22079  psrbagsn  22104  evlslem1  22123  mhpvarcl  22201  psdcl  22214  psdmul  22219  psdmvr  22222  pmatcollpw3fi1lem1  22834  chfacfscmulgsum  22908  chfacfpmmulfsupp  22911  chfacfpmmulgsum  22912  chfacfpmmulgsum2  22913  cpmadugsumlemB  22922  cpmadugsumlemF  22924  dscmet  24620  ehl1eudis  25470  dveflem  26029  c1lip2  26048  itgpowd  26100  ply1remlem  26213  fta1glem1  26216  fta1blem  26219  plyid  26257  coeidp  26311  dgrid  26312  plyn0mulidp  26333  vieta1lem2  26363  vieta1  26364  aalioulem3  26386  aaliou2b  26393  dvtaylp  26421  taylthlem1  26424  taylthlem2  26425  radcnvlem2  26465  dvradcnv  26472  pserdvlem2  26479  logtayllem  26712  logtayl  26713  cxp1  26724  quart1cl  26907  quart1lem  26908  quart1  26909  quartlem1  26910  quartlem2  26911  leibpilem2  26994  log2ublem3  27001  log2ub  27002  birthday  27007  lgamcvg2  27107  gamp1  27110  issqf  27188  ppi2  27222  mumullem2  27232  sqff1o  27234  1sgmprm  27251  ppiublem2  27255  chtublem  27263  logfacbnd3  27275  logexprlim  27277  logfacrlim2  27278  perfectlem1  27281  perfectlem2  27282  bclbnd  27332  bpos1  27335  bposlem6  27341  lgsval  27353  2lgslem3a  27448  2lgslem3c  27450  rpvmasumlem  27539  log2sumbnd  27596  itvndx  28594  lngndx  28595  itvid  28596  lngid  28597  slotsinbpsd  28598  slotslnbpsd  28599  lngndxnitvndx  28600  trkgstr  28601  eengstr  29138  edgfid  29148  edgfndx  29149  edgfndxnn  29150  basendxltedgfndx  29152  usgrexmplef  29417  cusgrsizeindb1  29608  wlk1ewlk  29797  usgr2pthlem  29920  uspgrn2crct  29965  crctcshwlkn0lem5  29971  rusgrnumwwlkl1  30128  rusgrnumwwlkb1  30132  clwwlkccatlem  30148  clwwlkinwwlk  30199  umgr2cwwkdifex  30224  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  konigsbergiedgw  30407  konigsberglem1  30411  konigsberglem2  30412  konigsberglem3  30413  konigsberglem4  30414  1kp2ke3k  30605  ex-exp  30609  ex-fac  30610  9p10ne21  30629  sgnmulsgp  32995  nexple  32996  dpmul4  33052  threehalves  33053  1mhdrd  33054  s2f1  33084  cycpm2tr  33260  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  ply1dg1rt  33737  coe1vr1  33748  deg1vr  33749  mplmulmvr  33797  esplylem  33824  esplyfv1  33827  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  drngdimgt0  33876  rtelextdg2lem  33984  fldext2chn  33986  constrdircl  34023  iconstr  34024  2sqr3minply  34038  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminply  34046  lmat22e12  34077  lmat22e21  34078  lmat22e22  34079  madjusmdetlem4  34088  oddpwdc  34612  eulerpartlemd  34624  eulerpartlemgs2  34638  eulerpartlemn  34639  iwrdsplit  34645  fib0  34657  fib1  34658  fibp1  34659  signstfveq0  34832  signsvvf  34834  signsvfn  34837  signshlen  34845  prodfzo03  34858  reprsuc  34870  breprexplemc  34887  hgt750lemd  34903  hgt750lem  34906  hgt750lem2  34907  hgt750leme  34913  usgrgt2cycl  35441  subfac1  35489  kur14lem9  35525  bccolsum  36050  nn0prpw  36644  12gcd5e1  42581  60gcd6e6  42582  60gcd7e1  42583  420gcd8e4  42584  12lcm5e60  42586  lcmineqlem11  42617  lcmineqlem18  42624  lcmineqlem22  42628  lcmineqlem  42630  3exp7  42631  3lexlogpow5ineq1  42632  3lexlogpow5ineq2  42633  3lexlogpow5ineq5  42638  dvrelogpow2b  42646  aks4d1p1p2  42648  aks4d1p1p4  42649  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  aks4d1p1  42654  aks4d1p3  42656  aks6d1c1p8  42693  aks6d1c5lem3  42715  2np3bcnp1  42722  2ap1caineq  42723  sticksstones22  42746  aks6d1c6lem1  42748  aks6d1c7lem1  42758  aks6d1c7  42762  235t711  42875  ex-decpmul  42876  fltnltalem  43205  sum9cubes  43215  3cubeslem3l  43228  3cubeslem3r  43229  pell1qr1  43409  rmspecfund  43447  jm2.23  43534  jm2.27c  43545  areaquad  43754  resqrtvalex  44182  imsqrtvalex  44183  brfvidRP  44225  brfvrcld  44228  corclrcl  44244  dftrcl3  44257  dfrtrcl3  44270  fvrtrcllb1d  44274  corcltrcl  44276  cotrclrcl  44279  inductionexd  44692  radcnvrat  44851  binomcxplemnn0  44886  binomcxplemfrat  44888  binomcxplemnotnn0  44893  rexanuz2nf  46027  wallispilem2  46601  wallispilem5  46604  wallispi2lem2  46607  stirlinglem5  46613  stirlinglem7  46615  stirlinglem10  46618  stirlinglem11  46619  fourierdlem48  46689  ormkglobd  47412  sin5tlem4  47431  goldratmolem2  47441  iccpartigtl  47990  iccpartlt  47991  iccpartgel  47996  fmtnosqrt  48109  fmtno1  48111  fmtno2  48120  fmtno5lem1  48123  fmtno5lem2  48124  fmtno5lem3  48125  fmtno5lem4  48126  fmtno5  48127  257prm  48131  fmtnofac1  48140  fmtno4prmfac  48142  fmtno4prmfac193  48143  fmtno4nprmfac193  48144  fmtno5faclem1  48149  fmtno5faclem2  48150  fmtno5faclem3  48151  fmtno5fac  48152  fmtno5nprm  48153  3ndvds4  48165  139prmALT  48166  31prm  48167  m5prm  48168  127prm  48169  m7prm  48170  m11nprm  48171  lighneallem2  48176  perfectALTVlem1  48304  perfectALTVlem2  48305  11t31e341  48315  2exp340mod341  48316  341fppr2  48317  8exp8mod9  48319  nfermltl8rev  48325  nfermltl2rev  48326  evengpoap3  48382  nnsum4primesevenALTV  48384  bgoldbtbndlem1  48388  bgoldbachlt  48396  tgblthelfgott  48398  cycl3grtri  48530  stgr1  48544  usgrexmpl1lem  48604  usgrexmpl2lem  48609  gpgprismgriedgdmss  48635  gpgprismgr4cycllem3  48680  gpgprismgr4cycllem7  48684  gpgprismgr4cycllem9  48686  gpgprismgr4cycllem10  48687  grlimedgnedg  48714  nnpw2pmod  49166  dig1  49191  dignn0flhalflem2  49199  1aryfvalel  49219  itcoval1  49246  itcoval2  49247  ackval1  49264  ackval2  49265  ackval3  49266  ackendofnn0  49267  ackvalsucsucval  49271  ackval0012  49272  ackval1012  49273  ackval2012  49274  ackval3012  49275  ackval41a  49277  ackval42  49279