Theorem nncn 10650

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

Assertion

Ref	Expression
nncn	|- ( A e. NN -> A e. CC )

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 10647	. 2 |- NN C_ CC
2	1	sseli 3440	1 |- ( A e. NN -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1898   CCcc 9568   NNcn 10642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-i2m1 9638  ax-1ne0 9639  ax-rrecex 9642  ax-cnre 9643

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-nn 10643

This theorem is referenced by:  nn1m1nn  10662  nn1suc  10663  nnaddcl  10664  nnmulcl  10665  nnsub  10681  nndiv  10683  nndivtr  10684  nnnn0addcl  10934  nn0nnaddcl  10935  elnnnn0  10947  nn0sub  10954  nnnegz  10974  elz2  10988  zaddcl  11011  nnaddm1cl  11027  zdiv  11040  zdivadd  11041  zdivmul  11042  nneo  11053  peano5uzi  11058  elq  11300  qmulz  11301  qaddcl  11314  qnegcl  11315  qmulcl  11316  qreccl  11318  rpnnen1lem5  11328  fseq1m1p1  11904  ubmelm1fzo  12044  quoremz  12120  quoremnn0ALT  12122  intfracq  12124  fldiv  12125  fldiv2  12126  modmulnn  12152  modidmul0OLD  12161  addmodid  12177  modaddmodup  12191  nn0ennn  12230  ser1const  12307  expneg  12318  expm1t  12338  nnsqcl  12382  nnlesq  12416  digit2  12443  digit1  12444  facdiv  12510  facndiv  12511  faclbnd  12513  faclbnd4lem1  12516  faclbnd4lem4  12519  bcn1  12536  bcm1k  12538  bcp1n  12539  bcval5  12541  bcn2m1  12547  swrdccatwrd  12867  cshwidxmod  12948  cshwidxm  12952  cshwidxn  12953  repswcshw  12954  isercoll2  13787  divcnv  13966  harmonic  13972  arisum  13973  arisum2  13974  expcnv  13977  geomulcvg  13987  mertenslem2  13996  ef0lem  14188  efexp  14210  ruclem12  14348  sqrt2irr  14356  divalgmod  14442  ndvdsadd  14444  modgcd  14555  gcddiv  14572  gcdmultiple  14573  gcdmultiplez  14574  rpmulgcd  14578  rplpwr  14579  sqgcd  14581  lcmgcdlem  14626  prmind2  14690  qredeq  14718  qredeu  14719  isprm6  14721  divnumden  14752  divdenle  14753  nn0gcdsq  14756  pythagtriplem1  14821  pythagtriplem2  14822  pythagtriplem6  14826  pythagtriplem7  14827  pythagtriplem12  14831  pythagtriplem14  14833  pythagtriplem15  14834  pythagtriplem16  14835  pythagtriplem17  14836  pythagtriplem19  14838  pcqcl  14861  pcexp  14864  pcneg  14878  fldivp1  14897  prmpwdvds  14903  infpnlem2  14910  prmreclem1  14915  prmreclem6  14920  4sqlem19  14968  vdwapun  14979  vdwapid1  14980  prmonn2  15052  prmgaplem7  15082  mulgnegnn  16823  mulgnnass  16841  odmod  17250  cply1mul  18942  cnfldmulg  19055  prmirredlem  19119  znidomb  19187  znrrg  19191  chfacfscmul0  19937  chfacfscmulfsupp  19938  chfacfscmulgsum  19939  chfacfpmmul0  19941  chfacfpmmulfsupp  19942  chfacfpmmulgsum  19943  cayhamlem1  19945  cpmadugsumlemF  19955  ovolunlem1  22505  uniioombllem3  22599  vitali  22627  mbfi1fseqlem3  22731  dvexp  22963  dvexp3  22986  plyeq0lem  23220  dgrcolem1  23283  aaliou3lem2  23355  aaliou3lem7  23361  pserdv2  23441  abelthlem6  23447  logtayl  23661  logtaylsum  23662  logtayl2  23663  cxpexp  23669  cxproot  23691  root1id  23750  root1eq1  23751  cxpeq  23753  atantayl  23919  atantayl2  23920  birthdaylem2  23934  dfef2  23952  emcllem2  23978  emcllem3  23979  zetacvg  23996  lgam1  24045  gamfac  24048  basellem2  24064  basellem3  24065  basellem5  24067  basellem8  24070  mumul  24164  dvdsdivcl  24166  dvdsflip  24167  fsumdvdscom  24170  muinv  24178  chtublem  24195  perfect  24215  pcbcctr  24260  bclbnd  24264  bposlem1  24268  bposlem6  24273  lgssq  24319  lgssq2  24320  2sqlem6  24353  2sqlem10  24358  rplogsumlem1  24378  dchrmusumlema  24387  dchrmusum2  24388  dchrvmasumiflem1  24395  dchrvmaeq0  24398  dchrisum0re  24407  logdivbnd  24450  cusgrasize2inds  25261  clwwlkel  25577  clwwlkf  25578  clwwlkf1  25580  wwlksubclwwlk  25588  rusgra0edg  25739  clwwlkextfrlem1  25860  numclwwlk2lem1  25886  numclwlk2lem2f  25887  numclwlk2lem2f1o  25889  gxnn0neg  26047  ipasslem4  26531  ipasslem5  26532  isarchi3  28555  oddpwdc  29237  eulerpartlemb  29251  fibp1  29284  subfacp1lem6  29958  subfaclim  29961  snmlff  30102  circum  30368  divcnvlin  30417  bcprod  30424  iprodgam  30428  faclim  30432  faclim2  30434  nn0prpwlem  31028  nndivsub  31167  poimirlem13  31999  poimirlem14  32000  poimirlem29  32015  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  ovoliunnfl  32028  voliunnfl  32030  irrapxlem1  35712  pellexlem1  35719  pellqrex  35772  2nn0ind  35839  jm2.17c  35858  acongrep  35876  jm2.18  35889  jm2.20nn  35898  jm2.16nn0  35905  hashgcdlem  36120  proot1ex  36124  hashnzfzclim  36716  binomcxplemnotnn0  36750  nnsplit  37656  clim1fr1  37765  sumnnodd  37796  wallispilem4  38031  wallispilem5  38032  wallispi  38033  wallispi2lem1  38034  wallispi2lem2  38035  wallispi2  38036  stirlinglem1  38037  stirlinglem3  38039  stirlinglem4  38040  stirlinglem5  38041  stirlinglem6  38042  stirlinglem7  38043  stirlinglem8  38044  stirlinglem10  38046  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  stirlinglem14  38050  stirlinglem15  38051  dirkerper  38059  dirkertrigeqlem1  38061  fouriersw  38196  nnfoctbdjlem  38398  deccarry  38850  perfectALTV  38980  tgoldbachlt  39044  subsubelfzo0  39200  cusgrsize2inds  39660  1wlkdlem2  39822  nnsgrp  40186  nnsgrpnmnd  40187  bcpascm1  40501  altgsumbcALT  40503  eluz2cnn0n1  40676  pw2m1lepw2m1  40687  mod0mul  40691  m1modmmod  40693  nn0enne  40695  nno  40697  logbpw2m1  40747  blenpw2m1  40759  nnpw2blen  40760  nnpw2pmod  40763  blennnt2  40769  blennn0em1  40771  nn0digval  40780  dignn0fr  40781  dignn0ldlem  40782  dig0  40786  nn0sumshdiglemA  40799  nn0sumshdiglemB  40800  nn0sumshdiglem1  40801