Theorem 1nn0 12569

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

Syntax hints:   ∈ wcel 2108  1c1 11185  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-n0 12554

This theorem is referenced by:  peano2nn0  12593  deccl  12773  10nn0  12776  numsucc  12798  numadd  12805  numaddc  12806  11multnc  12826  6p5lem  12828  6p6e12  12832  7p5e12  12835  8p4e12  12840  9p2e11  12845  9p3e12  12846  10p10e20  12853  4t4e16  12857  5t2e10  12858  5t4e20  12860  6t3e18  12863  6t4e24  12864  7t3e21  12868  7t4e28  12869  8t3e24  12874  9t3e27  12881  9t9e81  12887  xnn0n0n1ge2b  13194  fz0to3un2pr  13686  elfzom1elp1fzo  13783  fzo0sn0fzo1  13805  fvf1tp  13840  fldiv4lem1div2  13888  expn1  14122  nn0expcl  14126  sqval  14165  nn0opthlem1  14317  fac2  14328  faclbnd4lem2  14343  bccl  14371  hashsng  14418  hashen1  14419  hashrabrsn  14421  1elfz0hash  14439  hashgt23el  14473  hashprlei  14517  hashtplei  14533  tpf1ofv1  14546  tpfo  14549  wrdred1hash  14609  pfx1  14751  repsw1  14831  cshw1  14870  s3fv1  14941  s4fv1  14945  pfx2  14996  repsw2  14999  repsw3  15000  wwlktovf  15005  relexp1g  15075  relexpaddg  15102  rtrclreclem1  15106  bcxmas  15883  climcndslem2  15898  climcnds  15899  arisum  15908  geoisum1  15927  geoisum1c  15928  mertenslem2  15933  fprodnn0cl  16005  nn0risefaccl  16070  bpoly1  16099  bpoly4  16107  fsumcube  16108  ege2le3  16138  ef4p  16161  efgt1p2  16162  efgt1p  16163  sin01gt0  16238  rpnnen2lem3  16264  dvds1  16367  3dvds2dec  16381  bitsmod  16482  bitsinv1lem  16487  sadadd2lem  16505  sadadd  16513  sadass  16517  smupp1  16526  smumul  16539  nn0rppwr  16608  prmdvdsbc  16773  pcelnn  16917  pockthg  16953  vdwlem12  17039  prmo1  17084  dec5nprm  17113  dec2nprm  17114  modxp1i  17117  2exp8  17136  2exp11  17137  2exp16  17138  2expltfac  17140  5prm  17156  11prm  17162  13prm  17163  17prm  17164  19prm  17165  23prm  17166  prmlem2  17167  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  ocndx  17440  ocid  17441  basendxnocndx  17442  plendxnocndx  17443  dsndx  17444  dsid  17445  dsndxnn  17446  basendxltdsndx  17447  slotsdifdsndx  17453  unifndx  17454  unifid  17455  unifndxnn  17456  basendxltunifndx  17457  slotsdifunifndx  17460  odrngstr  17462  homndx  17470  homid  17471  ccondx  17472  ccoid  17473  slotsbhcdif  17474  slotsbhcdifOLD  17475  slotsdifplendx2  17476  slotsdifocndx  17477  imasvalstr  17511  prdsvalstr  17512  oppchomfvalOLD  17773  oppcbasOLD  17778  rescbasOLD  17891  resccoOLD  17895  rescabsOLD  17897  catstr  18026  ipostr  18599  smndex2dnrinv  18950  cycsubmcl  19241  psgnunilem2  19537  odcau  19646  lt6abl  19937  mgpdsOLD  20175  0ringnnzr  20551  sradsOLD  21215  cnfldstr  21389  cnfldstrOLD  21404  cnfldfunALTOLDOLD  21416  nn0srg  21478  freshmansdream  21616  thlbasOLD  21738  thlleOLD  21740  mvrid  22027  mvrf1  22029  mplcoe3  22079  psrbagsn  22110  evlslem1  22129  mhpvarcl  22175  psdcl  22188  psdmul  22193  pmatcollpw3fi1lem1  22813  chfacfscmulgsum  22887  chfacfpmmulfsupp  22890  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cpmadugsumlemB  22901  cpmadugsumlemF  22903  tuslemOLD  24297  tmslemOLD  24516  dscmet  24606  tnglemOLD  24675  ehl1eudis  25473  dveflem  26037  c1lip2  26057  itgpowd  26111  ply1remlem  26224  fta1glem1  26227  fta1blem  26230  plyid  26268  coeidp  26323  dgrid  26324  vieta1lem2  26371  vieta1  26372  aalioulem3  26394  aaliou2b  26401  dvtaylp  26430  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  radcnvlem2  26475  dvradcnv  26482  pserdvlem2  26490  logtayllem  26719  logtayl  26720  cxp1  26731  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  leibpilem2  27002  log2ublem3  27009  log2ub  27010  birthday  27015  lgamcvg2  27116  gamp1  27119  issqf  27197  ppi2  27231  mumullem2  27241  sqff1o  27243  1sgmprm  27261  ppiublem2  27265  chtublem  27273  logfacbnd3  27285  logexprlim  27287  logfacrlim2  27288  perfectlem1  27291  perfectlem2  27292  bclbnd  27342  bpos1  27345  bposlem6  27351  lgsval  27363  2lgslem3a  27458  2lgslem3c  27460  rpvmasumlem  27549  log2sumbnd  27606  itvndx  28463  lngndx  28464  itvid  28465  lngid  28466  slotsinbpsd  28467  slotslnbpsd  28468  lngndxnitvndx  28469  trkgstr  28470  ttgvalOLD  28902  ttglemOLD  28904  ttgbasOLD  28906  ttgdsOLD  28913  eengstr  29013  edgfid  29023  edgfndx  29024  edgfndxnn  29025  edgfndxidOLD  29027  basendxltedgfndx  29028  baseltedgfOLD  29029  usgrexmplef  29294  cusgrsizeindb1  29486  wlk1ewlk  29676  usgr2pthlem  29799  uspgrn2crct  29841  crctcshwlkn0lem5  29847  rusgrnumwwlkl1  30001  rusgrnumwwlkb1  30005  clwwlkccatlem  30021  clwwlkinwwlk  30072  umgr2cwwkdifex  30097  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsbergiedgw  30280  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberglem4  30287  1kp2ke3k  30478  ex-exp  30482  ex-fac  30483  9p10ne21  30502  dpmul4  32878  threehalves  32879  1mhdrd  32880  s2f1  32911  omndmul2  33062  cycpm2tr  33112  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1dg1rt  33569  coe1vr1  33578  deg1vr  33579  drngdimgt0  33631  rtelextdg2lem  33717  fldext2chn  33719  2sqr3minply  33738  lmat22e12  33765  lmat22e21  33766  lmat22e22  33767  madjusmdetlem4  33776  nexple  33973  oddpwdc  34319  eulerpartlemd  34331  eulerpartlemgs2  34345  eulerpartlemn  34346  iwrdsplit  34352  fib0  34364  fib1  34365  fibp1  34366  sgnmulsgn  34514  sgnmulsgp  34515  plymulx0  34524  signstfveq0  34554  signsvvf  34556  signsvfn  34559  signshlen  34567  prodfzo03  34580  reprsuc  34592  breprexplemc  34609  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  usgrgt2cycl  35098  subfac1  35146  kur14lem9  35182  bccolsum  35701  nn0prpw  36289  12gcd5e1  41960  60gcd6e6  41961  60gcd7e1  41962  420gcd8e4  41963  12lcm5e60  41965  lcmineqlem11  41996  lcmineqlem18  42003  lcmineqlem22  42007  lcmineqlem  42009  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq5  42017  dvrelogpow2b  42025  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p3  42035  aks6d1c1p8  42072  aks6d1c5lem3  42094  2np3bcnp1  42101  2ap1caineq  42102  sticksstones22  42125  aks6d1c6lem1  42127  aks6d1c7lem1  42137  aks6d1c7  42141  factwoffsmonot  42199  235t711  42293  ex-decpmul  42294  fltnltalem  42617  sum9cubes  42627  3cubeslem3l  42642  3cubeslem3r  42643  pell1qr1  42827  rmspecfund  42865  jm2.23  42953  jm2.27c  42964  areaquad  43177  resqrtvalex  43607  imsqrtvalex  43608  brfvidRP  43650  brfvrcld  43653  corclrcl  43669  dftrcl3  43682  dfrtrcl3  43695  fvrtrcllb1d  43699  corcltrcl  43701  cotrclrcl  43704  inductionexd  44117  radcnvrat  44283  binomcxplemnn0  44318  binomcxplemfrat  44320  binomcxplemnotnn0  44325  rexanuz2nf  45408  wallispilem2  45987  wallispilem5  45990  wallispi2lem2  45993  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  fourierdlem48  46075  iccpartigtl  47297  iccpartlt  47298  iccpartgel  47303  fmtnosqrt  47413  fmtno1  47415  fmtno2  47424  fmtno5lem1  47427  fmtno5lem2  47428  fmtno5lem3  47429  fmtno5lem4  47430  fmtno5  47431  257prm  47435  fmtnofac1  47444  fmtno4prmfac  47446  fmtno4prmfac193  47447  fmtno4nprmfac193  47448  fmtno5faclem1  47453  fmtno5faclem2  47454  fmtno5faclem3  47455  fmtno5fac  47456  fmtno5nprm  47457  3ndvds4  47469  139prmALT  47470  31prm  47471  m5prm  47472  127prm  47473  m7prm  47474  m11nprm  47475  lighneallem2  47480  perfectALTVlem1  47595  perfectALTVlem2  47596  11t31e341  47606  2exp340mod341  47607  341fppr2  47608  8exp8mod9  47610  nfermltl8rev  47616  nfermltl2rev  47617  evengpoap3  47673  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  bgoldbachlt  47687  tgblthelfgott  47689  usgrexmpl1lem  47836  usgrexmpl2lem  47841  nnpw2pmod  48317  dig1  48342  dignn0flhalflem2  48350  1aryfvalel  48370  itcoval1  48397  itcoval2  48398  ackval1  48415  ackval2  48416  ackval3  48417  ackendofnn0  48418  ackvalsucsucval  48422  ackval0012  48423  ackval1012  48424  ackval2012  48425  ackval3012  48426  ackval41a  48428  ackval42  48430  prstclevalOLD  48736  prstcocvalOLD  48739