Theorem nncn 8879

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

Syntax hints:   -> wi 4   e. wcel 2141   CCcc 7765   NNcn 8871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105  ax-cnex 7858  ax-resscn 7859  ax-1re 7861  ax-addrcl 7864

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3830  df-inn 8872

This theorem is referenced by:  nn1m1nn  8889  nn1suc  8890  nnaddcl  8891  nnmulcl  8892  nnsub  8910  nndiv  8912  nndivtr  8913  nnnn0addcl  9158  nn0nnaddcl  9159  elnnnn0  9171  nnnegz  9208  zaddcllempos  9242  zaddcllemneg  9244  nnaddm1cl  9266  elz2  9276  zdiv  9293  zdivadd  9294  zdivmul  9295  nneoor  9307  nneo  9308  divfnzn  9573  qmulz  9575  qaddcl  9587  qnegcl  9588  qmulcl  9589  qreccl  9594  nnledivrp  9716  nn0ledivnn  9717  fseq1m1p1  10044  nnsplit  10086  ubmelm1fzo  10175  subfzo0  10191  flqdiv  10270  addmodidr  10322  modfzo0difsn  10344  nn0ennn  10382  expnegap0  10477  expm1t  10497  nnsqcl  10538  nnlesq  10572  facdiv  10665  facndiv  10666  faclbnd  10668  bcn1  10685  bcn2m1  10696  arisum  11454  arisum2  11455  expcnvap0  11458  mertenslem2  11492  ef0lem  11616  efexp  11638  nndivides  11752  modmulconst  11778  dvdsflip  11804  nn0enne  11854  nno  11858  divalgmod  11879  ndvdsadd  11883  modgcd  11939  gcddiv  11967  gcdmultiple  11968  gcdmultiplez  11969  rpmulgcd  11974  rplpwr  11975  sqgcd  11977  lcmgcdlem  12024  qredeq  12043  qredeu  12044  divgcdcoprm0  12048  cncongrcoprm  12053  prmind2  12067  isprm6  12094  sqrt2irr  12109  oddpwdclemodd  12119  divnumden  12143  divdenle  12144  nn0gcdsq  12147  hashgcdlem  12185  pythagtriplem1  12212  pythagtriplem2  12213  pythagtriplem6  12217  pythagtriplem7  12218  pythagtriplem12  12222  pythagtriplem14  12224  pythagtriplem15  12225  pythagtriplem16  12226  pythagtriplem17  12227  pythagtriplem19  12229  pcqcl  12253  pcexp  12256  pcneg  12271  fldivp1  12293  oddprmdvds  12299  prmpwdvds  12300  infpnlem2  12305  dvexp  13434  rpcxproot  13593  logbgcd1irr  13644  lgssq2  13701  2sqlem6  13715  2sqlem10  13720