Theorem 1nn0 11308

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	|- 1 e. NN0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 11031	. 2 |- 1 e. NN
2	1	nnnn0i 11300	1 |- 1 e. NN0

Syntax hints:   e. wcel 1990   1c1 9937   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-1cn 9994

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021  df-n0 11293

This theorem is referenced by:  peano2nn0  11333  deccl  11512  10nn0  11516  numsucc  11549  numadd  11560  numaddc  11561  11multnc  11592  6p5lem  11595  6p6e12  11602  7p5e12  11607  8p4e12  11614  9p2e11  11619  9p2e11OLD  11620  9p3e12  11621  10p10e20  11628  10p10e20OLD  11629  4t4e16  11633  5t2e10  11634  5t4e20  11637  5t4e20OLD  11638  6t3e18  11642  6t4e24  11643  7t3e21  11649  7t4e28  11650  8t3e24  11655  9t3e27  11664  9t9e81  11670  xnn0n0n1ge2b  11965  fz0to3un2pr  12441  elfzom1elp1fzo  12534  fzo0sn0fzo1  12557  fldiv4lem1div2  12638  expn1  12870  nn0expcl  12874  sqval  12922  sq10  13048  nn0opthlem1  13055  fac2  13066  faclbnd4lem2  13081  bccl  13109  hashsng  13159  hashen1  13160  hashrabrsn  13161  1elfz0hash  13179  hashprlei  13250  hashtplei  13266  wrdred1hash  13350  swrd0len0  13436  swrdtrcfv  13441  swrdccatwrd  13468  wrdeqs1cat  13474  repsw1  13530  cshw1  13568  s3fv1  13637  s4fv1  13641  repsw2  13693  repsw3  13694  wwlktovf  13699  relexp1g  13766  relexpaddg  13793  rtrclreclem2  13799  bcxmas  14567  climcndslem2  14582  climcnds  14583  arisum  14592  geoisum1  14610  geoisum1c  14611  mertenslem2  14617  fprodnn0cl  14687  nn0risefaccl  14753  bpoly1  14782  bpoly4  14790  fsumcube  14791  ege2le3  14820  ef4p  14843  efgt1p2  14844  efgt1p  14845  sin01gt0  14920  rpnnen2lem3  14945  dvds1  15041  3dvds2dec  15056  3dvds2decOLD  15057  bitsmod  15158  bitsinv1lem  15163  sadadd2lem  15181  sadadd  15189  sadass  15193  smupp1  15202  smumul  15215  pcelnn  15574  pockthg  15610  vdwlem12  15696  prmo1  15741  dec5nprm  15770  dec2nprm  15771  modxp1i  15774  2exp8  15796  2exp16  15797  2expltfac  15799  5prm  15815  11prm  15822  13prm  15823  17prm  15824  19prm  15825  23prm  15826  prmlem2  15827  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  ocndx  16060  ocid  16061  dsndx  16062  dsid  16063  unifndx  16064  unifid  16065  odrngstr  16066  ressds  16073  homndx  16074  homid  16075  ccondx  16076  ccoid  16077  resshom  16078  ressco  16079  slotsbhcdif  16080  imasvalstr  16112  prdsvalstr  16113  oppchomfval  16374  oppcbas  16378  rescbas  16489  rescco  16492  rescabs  16493  catstr  16617  ipostr  17153  psgnunilem2  17915  odcau  18019  lt6abl  18296  mgpds  18499  srads  19186  0ringnnzr  19269  mvrid  19423  mvrf1  19425  mplcoe3  19466  psrbagsn  19495  evlslem1  19515  cnfldstr  19748  cnfldfun  19758  nn0srg  19816  thlbas  20040  thlle  20041  pmatcollpw3fi1lem1  20591  chfacfscmulgsum  20665  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cpmadugsumlemB  20679  cpmadugsumlemF  20681  ressunif  22066  tuslem  22071  tmslem  22287  dscmet  22377  tnglem  22444  dveflem  23742  c1lip2  23761  ply1remlem  23922  fta1glem1  23925  fta1blem  23928  plyid  23965  coeidp  24019  dgrid  24020  vieta1lem2  24066  vieta1  24067  aalioulem3  24089  aaliou2b  24096  dvtaylp  24124  taylthlem1  24127  taylthlem2  24128  radcnvlem2  24168  dvradcnv  24175  pserdvlem2  24182  logtayllem  24405  logtayl  24406  cxp1  24417  dcubic1lem  24570  dcubic2  24571  mcubic  24574  quart1cl  24581  quart1lem  24582  quart1  24583  quartlem1  24584  quartlem2  24585  leibpilem2  24668  log2ublem3  24675  log2ub  24676  birthday  24681  lgamcvg2  24781  gamp1  24784  issqf  24862  ppi2  24896  mumullem2  24906  sqff1o  24908  1sgmprm  24924  ppiublem2  24928  chtublem  24936  logfacbnd3  24948  logexprlim  24950  logfacrlim2  24951  perfectlem1  24954  perfectlem2  24955  bclbnd  25005  bpos1  25008  bposlem6  25014  lgsval  25026  2lgslem3a  25121  2lgslem3c  25123  rpvmasumlem  25176  log2sumbnd  25233  itvndx  25339  lngndx  25340  itvid  25341  lngid  25342  trkgstr  25343  ttgval  25755  ttglem  25756  ttgbas  25757  ttgds  25761  eengstr  25860  edgfid  25869  edgfndxnn  25870  edgfndxid  25871  baseltedgf  25872  usgrexmplef  26151  cusgrsizeindb1  26346  wlk1ewlk  26536  usgr2pthlem  26659  uspgrn2crct  26700  crctcshwlkn0lem5  26706  rusgrnumwwlkl1  26863  rusgrnumwwlkb1  26867  clwwlkinwwlk  26905  umgr2cwwkdifex  26942  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  konigsberglem4  27117  extwwlkfablem2  27210  1kp2ke3k  27303  ex-exp  27307  ex-fac  27308  dpmul4  29622  threehalves  29623  1mhdrd  29624  omndmul2  29712  lmat22e12  29885  lmat22e21  29886  lmat22e22  29887  madjusmdetlem4  29896  nexple  30071  oddpwdc  30416  eulerpartlemd  30428  eulerpartlemgs2  30442  eulerpartlemn  30443  iwrdsplit  30449  fib0  30461  fib1  30462  fibp1  30463  sgnmulsgn  30611  sgnmulsgp  30612  plymulx0  30624  signstfveq0  30654  signsvvf  30656  signsvfn  30659  signshlen  30667  prodfzo03  30681  reprsuc  30693  breprexplemc  30710  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  subfac1  31160  kur14lem9  31196  bccolsum  31625  nn0prpw  32318  pell1qr1  37435  rmspecfund  37474  jm2.23  37563  jm2.27c  37574  itgpowd  37800  areaquad  37802  brfvidRP  37980  brfvrcld  37983  corclrcl  37999  dftrcl3  38012  dfrtrcl3  38025  fvrtrcllb1d  38029  corcltrcl  38031  cotrclrcl  38034  inductionexd  38453  radcnvrat  38513  binomcxplemnn0  38548  binomcxplemfrat  38550  binomcxplemnotnn0  38555  wallispilem2  40283  wallispilem5  40286  wallispi2lem2  40289  stirlinglem5  40295  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  fourierdlem48  40371  iccpartigtl  41359  iccpartlt  41360  iccpartgel  41365  pfx1  41411  pfx2  41412  fmtnosqrt  41451  fmtno1  41453  fmtno2  41462  fmtno5lem1  41465  fmtno5lem2  41466  fmtno5lem3  41467  fmtno5lem4  41468  fmtno5  41469  257prm  41473  fmtnofac1  41482  fmtno4prmfac  41484  fmtno4prmfac193  41485  fmtno4nprmfac193  41486  fmtno5faclem1  41491  fmtno5faclem2  41492  fmtno5faclem3  41493  fmtno5fac  41494  fmtno5nprm  41495  3ndvds4  41510  139prmALT  41511  31prm  41512  m5prm  41513  127prm  41515  m7prm  41516  2exp11  41517  m11nprm  41518  lighneallem2  41523  perfectALTVlem1  41630  perfectALTVlem2  41631  evengpoap3  41687  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  bgoldbachlt  41701  tgblthelfgott  41703  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  nnpw2pmod  42377  dig1  42402  dignn0flhalflem2  42410