Theorem nncn 10569

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nncn

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 10566	. 2
2	1	sseli 3499	1

Syntax hints:  ->wi 4  e.wcel 1818  cc 9511  cn 10561

This theorem is referenced by:  nn1m1nn  10581  nn1suc  10582  nnaddcl  10583  nnmulcl  10584  nnsub  10599  nndiv  10601  nndivtr  10602  nnnn0addcl  10851  nn0nnaddcl  10852  elnnnn0  10864  nn0sub  10871  nnnegz  10892  elz2  10906  zaddcl  10929  nnaddm1cl  10945  zdiv  10958  zdivadd  10959  zdivmul  10960  nneo  10971  peano5uzi  10976  uzindOLD  10982  elq  11213  qmulz  11214  qaddcl  11227  qnegcl  11228  qmulcl  11229  qreccl  11231  rpnnen1lem5  11241  fseq1m1p1  11782  ubmelm1fzo  11908  quoremz  11982  quoremnn0ALT  11984  intfracq  11986  fldiv  11987  fldiv2  11988  modmulnn  12013  modidmul0  12022  modaddmodup  12050  nn0ennn  12089  ser1const  12163  expneg  12174  expm1t  12194  nnsqcl  12237  nnlesq  12271  digit2  12299  digit1  12300  facdiv  12365  facndiv  12366  faclbnd  12368  faclbnd4lem1  12371  faclbnd4lem4  12374  bcn1  12391  bcm1k  12393  bcp1n  12394  bcval5  12396  bcn2m1  12402  swrdccatwrd  12693  cshwidxmod  12774  cshwidxm  12778  cshwidxn  12779  repswcshw  12780  isercoll2  13491  divcnv  13665  harmonic  13670  arisum  13671  arisum2  13672  expcnv  13675  geomulcvg  13685  mertenslem2  13694  ef0lem  13814  efexp  13836  ruclem12  13974  sqrt2irr  13982  divalgmod  14064  ndvdsadd  14066  modgcd  14174  gcddiv  14187  gcdmultiple  14188  gcdmultiplez  14189  rpmulgcd  14193  rplpwr  14194  sqgcd  14196  prmind2  14228  qredeq  14247  qredeu  14248  isprm6  14250  divnumden  14281  divdenle  14282  nn0gcdsq  14285  pythagtriplem1  14340  pythagtriplem2  14341  pythagtriplem6  14345  pythagtriplem7  14346  pythagtriplem12  14350  pythagtriplem14  14352  pythagtriplem15  14353  pythagtriplem16  14354  pythagtriplem17  14355  pythagtriplem19  14357  pcqcl  14380  pcexp  14383  pcneg  14397  fldivp1  14416  prmpwdvds  14422  infpnlem2  14429  prmreclem1  14434  prmreclem6  14439  4sqlem19  14481  vdwapun  14492  vdwapid1  14493  mulgnegnn  16152  mulgnnass  16170  odmod  16570  cply1mul  18335  cnfldmulg  18450  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  znrrg  18604  chfacfscmul0  19359  chfacfscmulfsupp  19360  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulfsupp  19364  chfacfpmmulgsum  19365  cayhamlem1  19367  cpmadugsumlemF  19377  ovolunlem1  21908  uniioombllem3  21994  vitali  22022  mbfi1fseqlem3  22124  dvexp  22356  dvexp3  22379  plyeq0lem  22607  dgrcolem1  22670  aaliou3lem2  22739  aaliou3lem7  22745  pserdv2  22825  abelthlem6  22831  logtayl  23041  logtaylsum  23042  logtayl2  23043  cxpexp  23049  cxproot  23071  root1id  23128  root1eq1  23129  cxpeq  23131  atantayl  23268  atantayl2  23269  birthdaylem2  23282  dfef2  23300  emcllem2  23326  emcllem3  23327  basellem2  23355  basellem3  23356  basellem5  23358  basellem8  23361  mumul  23455  dvdsdivcl  23457  dvdsflip  23458  fsumdvdscom  23461  muinv  23469  chtublem  23486  perfect  23506  pcbcctr  23551  bclbnd  23555  bposlem1  23559  bposlem6  23564  lgssq  23610  lgssq2  23611  2sqlem6  23644  2sqlem10  23649  rplogsumlem1  23669  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumiflem1  23686  dchrvmaeq0  23689  dchrisum0re  23698  logdivbnd  23741  cusgrasize2inds  24477  clwwlkel  24793  clwwlkf  24794  clwwlkf1  24796  wwlksubclwwlk  24804  rusgra0edg  24955  clwwlkextfrlem1  25076  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  gxnn0neg  25265  ipasslem4  25749  ipasslem5  25750  isarchi3  27731  oddpwdc  28293  eulerpartlemb  28307  fibp1  28340  zetacvg  28557  lgam1  28606  gamfac  28609  subfacp1lem6  28629  subfaclim  28632  snmlff  28774  circum  29040  divcnvlin  29118  iprodgam  29125  faclim  29171  faclim2  29173  nndivsub  29922  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  nn0prpwlem  30140  irrapxlem1  30758  pellexlem1  30765  pellqrex  30815  2nn0ind  30881  jm2.17c  30900  acongrep  30918  jm2.18  30930  jm2.20nn  30939  jm2.16nn0  30946  hashgcdlem  31157  proot1ex  31161  lcmgcdlem  31212  hashnzfzclim  31227  binomcxplemnotnn0  31261  clim1fr1  31607  sumnnodd  31636  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem4  31859  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  dirkerper  31878  dirkertrigeqlem1  31880  fouriersw  32014  subsubelfzo0  32338  nnsgrp  32505  nnsgrpnmnd  32506  bcpascm1  32940  altgsumbcALT  32942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562