Theorem nncn 10544

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

Syntax hints:   -> wi 4   e. wcel 1767   CCcc 9490   NNcn 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-i2m1 9560  ax-1ne0 9561  ax-rrecex 9564  ax-cnre 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537

This theorem is referenced by:  nn1m1nn  10556  nn1suc  10557  nnaddcl  10558  nnmulcl  10559  nnsub  10574  nndiv  10576  nndivtr  10577  nnnn0addcl  10826  nn0nnaddcl  10827  elnnnn0  10839  nn0sub  10846  nnnegz  10867  elz2  10881  zaddcl  10903  nnaddm1cl  10919  zdiv  10931  zdivadd  10932  zdivmul  10933  nneo  10944  peano5uzi  10949  uzindOLD  10955  elq  11184  qmulz  11185  qaddcl  11198  qnegcl  11199  qmulcl  11200  qreccl  11202  rpnnen1lem5  11212  fseq1m1p1  11753  ubmelm1fzo  11876  quoremz  11950  quoremnn0ALT  11952  intfracq  11954  fldiv  11955  fldiv2  11956  modmulnn  11981  modidmul0  11990  modaddmodup  12018  nn0ennn  12057  ser1const  12131  expneg  12142  expm1t  12162  nnsqcl  12205  nnlesq  12239  digit2  12267  digit1  12268  facdiv  12333  facndiv  12334  faclbnd  12336  faclbnd4lem1  12339  faclbnd4lem4  12342  bcn1  12359  bcm1k  12361  bcp1n  12362  bcval5  12364  bcn2m1  12370  swrdccatwrd  12656  cshwidxmod  12737  cshwidxm  12741  cshwidxn  12742  repswcshw  12743  isercoll2  13454  divcnv  13628  harmonic  13633  arisum  13634  arisum2  13635  expcnv  13638  geomulcvg  13648  mertenslem2  13657  ef0lem  13676  efexp  13697  ruclem12  13835  sqrt2irr  13843  divalgmod  13923  ndvdsadd  13925  modgcd  14033  gcddiv  14046  gcdmultiple  14047  gcdmultiplez  14048  rpmulgcd  14052  rplpwr  14053  sqgcd  14055  prmind2  14087  qredeq  14106  qredeu  14107  isprm6  14109  divnumden  14140  divdenle  14141  nn0gcdsq  14144  pythagtriplem1  14199  pythagtriplem2  14200  pythagtriplem6  14204  pythagtriplem7  14205  pythagtriplem12  14209  pythagtriplem14  14211  pythagtriplem15  14212  pythagtriplem16  14213  pythagtriplem17  14214  pythagtriplem19  14216  pcqcl  14239  pcexp  14242  pcneg  14256  fldivp1  14275  prmpwdvds  14281  infpnlem2  14288  prmreclem1  14293  prmreclem6  14298  4sqlem19  14340  vdwapun  14351  vdwapid1  14352  mulgnegnn  15962  mulgnnass  15980  odmod  16376  cply1mul  18134  cnfldmulg  18249  prmirredlem  18318  prmirredlemOLD  18321  znidomb  18395  znrrg  18399  chfacfscmul0  19154  chfacfscmulfsupp  19155  chfacfscmulgsum  19156  chfacfpmmul0  19158  chfacfpmmulfsupp  19159  chfacfpmmulgsum  19160  cayhamlem1  19162  cpmadugsumlemF  19172  ovolunlem1  21671  uniioombllem3  21757  vitali  21785  mbfi1fseqlem3  21887  dvexp  22119  dvexp3  22142  plyeq0lem  22370  dgrcolem1  22432  aaliou3lem2  22501  aaliou3lem7  22507  pserdv2  22587  abelthlem6  22593  logtayl  22797  logtaylsum  22798  logtayl2  22799  cxpexp  22805  cxproot  22827  root1id  22884  root1eq1  22885  cxpeq  22887  atantayl  23024  atantayl2  23025  birthdaylem2  23038  dfef2  23056  emcllem2  23082  emcllem3  23083  basellem2  23111  basellem3  23112  basellem5  23114  basellem8  23117  mumul  23211  dvdsdivcl  23213  dvdsflip  23214  fsumdvdscom  23217  muinv  23225  chtublem  23242  perfect  23262  pcbcctr  23307  bclbnd  23311  bposlem1  23315  bposlem6  23320  lgssq  23366  lgssq2  23367  2sqlem6  23400  2sqlem10  23405  rplogsumlem1  23425  dchrmusumlema  23434  dchrmusum2  23435  dchrvmasumiflem1  23442  dchrvmaeq0  23445  dchrisum0re  23454  logdivbnd  23497  cusgrasize2inds  24181  clwwlkel  24497  clwwlkf  24498  clwwlkf1  24500  wwlksubclwwlk  24508  rusgra0edg  24659  clwwlkextfrlem1  24781  numclwwlk2lem1  24807  numclwlk2lem2f  24808  numclwlk2lem2f1o  24810  gxnn0neg  24969  ipasslem4  25453  ipasslem5  25454  isarchi3  27421  oddpwdc  27961  eulerpartlemb  27975  fibp1  28008  zetacvg  28225  lgam1  28274  gamfac  28277  subfacp1lem6  28297  subfaclim  28300  snmlff  28442  circum  28543  divcnvlin  28623  iprodgam  28730  faclim  28776  faclim2  28778  nndivsub  29527  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  nn0prpwlem  29745  irrapxlem1  30390  pellexlem1  30397  pellqrex  30447  2nn0ind  30513  jm2.17c  30532  acongrep  30550  jm2.18  30562  jm2.20nn  30571  jm2.16nn0  30578  hashgcdlem  30790  proot1ex  30794  lcmgcdlem  30840  hashnzfzclim  30855  clim1fr1  31171  sumnnodd  31200  wallispilem4  31396  wallispilem5  31397  wallispi  31398  wallispi2lem1  31399  wallispi2lem2  31400  wallispi2  31401  stirlinglem1  31402  stirlinglem3  31404  stirlinglem4  31405  stirlinglem5  31406  stirlinglem6  31407  stirlinglem7  31408  stirlinglem8  31409  stirlinglem10  31411  stirlinglem11  31412  stirlinglem12  31413  stirlinglem13  31414  stirlinglem14  31415  stirlinglem15  31416  dirkerper  31424  dirkertrigeqlem1  31426  sqwvfourb  31558  fouriersw  31560  subsubelfzo0  31833  bcpascm1  32036  altgsumbcALT  32038