Theorem nncn 10617

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 10614	. 2 |- NN C_ CC
2	1	sseli 3460	1 |- ( A e. NN -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1868   CCcc 9537   NNcn 10609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-nn 10610

This theorem is referenced by:  nn1m1nn  10629  nn1suc  10630  nnaddcl  10631  nnmulcl  10632  nnsub  10648  nndiv  10650  nndivtr  10651  nnnn0addcl  10900  nn0nnaddcl  10901  elnnnn0  10913  nn0sub  10920  nnnegz  10940  elz2  10954  zaddcl  10977  nnaddm1cl  10993  zdiv  11006  zdivadd  11007  zdivmul  11008  nneo  11019  peano5uzi  11024  elq  11266  qmulz  11267  qaddcl  11280  qnegcl  11281  qmulcl  11282  qreccl  11284  rpnnen1lem5  11294  fseq1m1p1  11869  ubmelm1fzo  12006  quoremz  12081  quoremnn0ALT  12083  intfracq  12085  fldiv  12086  fldiv2  12087  modmulnn  12113  modidmul0OLD  12122  addmodid  12138  modaddmodup  12152  nn0ennn  12191  ser1const  12268  expneg  12279  expm1t  12299  nnsqcl  12343  nnlesq  12377  digit2  12404  digit1  12405  facdiv  12471  facndiv  12472  faclbnd  12474  faclbnd4lem1  12477  faclbnd4lem4  12480  bcn1  12497  bcm1k  12499  bcp1n  12500  bcval5  12502  bcn2m1  12508  swrdccatwrd  12812  cshwidxmod  12893  cshwidxm  12897  cshwidxn  12898  repswcshw  12899  isercoll2  13717  divcnv  13896  harmonic  13902  arisum  13903  arisum2  13904  expcnv  13907  geomulcvg  13917  mertenslem2  13926  ef0lem  14118  efexp  14140  ruclem12  14278  sqrt2irr  14286  divalgmod  14372  ndvdsadd  14374  modgcd  14485  gcddiv  14502  gcdmultiple  14503  gcdmultiplez  14504  rpmulgcd  14508  rplpwr  14509  sqgcd  14511  lcmgcdlem  14556  prmind2  14620  qredeq  14648  qredeu  14649  isprm6  14651  divnumden  14682  divdenle  14683  nn0gcdsq  14686  pythagtriplem1  14751  pythagtriplem2  14752  pythagtriplem6  14756  pythagtriplem7  14757  pythagtriplem12  14761  pythagtriplem14  14763  pythagtriplem15  14764  pythagtriplem16  14765  pythagtriplem17  14766  pythagtriplem19  14768  pcqcl  14791  pcexp  14794  pcneg  14808  fldivp1  14827  prmpwdvds  14833  infpnlem2  14840  prmreclem1  14845  prmreclem6  14850  4sqlem19  14898  vdwapun  14909  vdwapid1  14910  prmonn2  14982  prmgaplem7  15012  mulgnegnn  16753  mulgnnass  16771  odmod  17180  cply1mul  18872  cnfldmulg  18985  prmirredlem  19048  znidomb  19116  znrrg  19120  chfacfscmul0  19866  chfacfscmulfsupp  19867  chfacfscmulgsum  19868  chfacfpmmul0  19870  chfacfpmmulfsupp  19871  chfacfpmmulgsum  19872  cayhamlem1  19874  cpmadugsumlemF  19884  ovolunlem1  22434  uniioombllem3  22527  vitali  22555  mbfi1fseqlem3  22659  dvexp  22891  dvexp3  22914  plyeq0lem  23148  dgrcolem1  23211  aaliou3lem2  23283  aaliou3lem7  23289  pserdv2  23369  abelthlem6  23375  logtayl  23589  logtaylsum  23590  logtayl2  23591  cxpexp  23597  cxproot  23619  root1id  23678  root1eq1  23679  cxpeq  23681  atantayl  23847  atantayl2  23848  birthdaylem2  23862  dfef2  23880  emcllem2  23906  emcllem3  23907  zetacvg  23924  lgam1  23973  gamfac  23976  basellem2  23992  basellem3  23993  basellem5  23995  basellem8  23998  mumul  24092  dvdsdivcl  24094  dvdsflip  24095  fsumdvdscom  24098  muinv  24106  chtublem  24123  perfect  24143  pcbcctr  24188  bclbnd  24192  bposlem1  24196  bposlem6  24201  lgssq  24247  lgssq2  24248  2sqlem6  24281  2sqlem10  24286  rplogsumlem1  24306  dchrmusumlema  24315  dchrmusum2  24316  dchrvmasumiflem1  24323  dchrvmaeq0  24326  dchrisum0re  24335  logdivbnd  24378  cusgrasize2inds  25188  clwwlkel  25504  clwwlkf  25505  clwwlkf1  25507  wwlksubclwwlk  25515  rusgra0edg  25666  clwwlkextfrlem1  25787  numclwwlk2lem1  25813  numclwlk2lem2f  25814  numclwlk2lem2f1o  25816  gxnn0neg  25974  ipasslem4  26458  ipasslem5  26459  isarchi3  28496  oddpwdc  29180  eulerpartlemb  29194  fibp1  29227  subfacp1lem6  29901  subfaclim  29904  snmlff  30045  circum  30311  divcnvlin  30359  bcprod  30366  iprodgam  30370  faclim  30374  faclim2  30376  nn0prpwlem  30968  nndivsub  31107  poimirlem13  31864  poimirlem14  31865  poimirlem29  31880  poimirlem30  31881  poimirlem31  31882  poimirlem32  31883  mblfinlem2  31889  ovoliunnfl  31893  voliunnfl  31895  irrapxlem1  35583  pellexlem1  35590  pellqrex  35643  2nn0ind  35710  jm2.17c  35729  acongrep  35747  jm2.18  35760  jm2.20nn  35769  jm2.16nn0  35776  hashgcdlem  35991  proot1ex  35995  hashnzfzclim  36526  binomcxplemnotnn0  36560  clim1fr1  37496  sumnnodd  37527  wallispilem4  37747  wallispilem5  37748  wallispi  37749  wallispi2lem1  37750  wallispi2lem2  37751  wallispi2  37752  stirlinglem1  37753  stirlinglem3  37755  stirlinglem4  37756  stirlinglem5  37757  stirlinglem6  37758  stirlinglem7  37759  stirlinglem8  37760  stirlinglem10  37762  stirlinglem11  37763  stirlinglem12  37764  stirlinglem13  37765  stirlinglem14  37766  stirlinglem15  37767  dirkerper  37775  dirkertrigeqlem1  37777  fouriersw  37912  nnfoctbdjlem  38069  deccarry  38424  perfectALTV  38554  tgoldbachlt  38618  subsubelfzo0  38748  nnsgrp  39003  nnsgrpnmnd  39004  bcpascm1  39320  altgsumbcALT  39322  eluz2cnn0n1  39495  pw2m1lepw2m1  39506  mod0mul  39510  m1modmmod  39512  nn0enne  39514  nno  39516  logbpw2m1  39566  blenpw2m1  39578  nnpw2blen  39579  nnpw2pmod  39582  blennnt2  39588  blennn0em1  39590  nn0digval  39599  dignn0fr  39600  dignn0ldlem  39601  dig0  39605  nn0sumshdiglemA  39618  nn0sumshdiglemB  39619  nn0sumshdiglem1  39620