Theorem nncn 9043

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

Syntax hints:   -> wi 4   e. wcel 2175   CCcc 7922   NNcn 9035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 8015  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-in 3171  df-ss 3178  df-int 3885  df-inn 9036

This theorem is referenced by:  nn1m1nn  9053  nn1suc  9054  nnaddcl  9055  nnmulcl  9056  nnsub  9074  nndiv  9076  nndivtr  9077  nnnn0addcl  9324  nn0nnaddcl  9325  elnnnn0  9337  nnnegz  9374  zaddcllempos  9408  zaddcllemneg  9410  nnaddm1cl  9433  elz2  9443  zdiv  9460  zdivadd  9461  zdivmul  9462  nneoor  9474  nneo  9475  divfnzn  9741  qmulz  9743  qaddcl  9755  qnegcl  9756  qmulcl  9757  qreccl  9762  nnledivrp  9887  nn0ledivnn  9888  fseq1m1p1  10216  nnsplit  10258  ubmelm1fzo  10353  subfzo0  10369  flqdiv  10464  addmodidr  10516  modfzo0difsn  10538  nn0ennn  10576  expnegap0  10690  expm1t  10710  nnsqcl  10752  nnlesq  10786  facdiv  10881  facndiv  10882  faclbnd  10884  bcn1  10901  bcn2m1  10912  arisum  11780  arisum2  11781  expcnvap0  11784  mertenslem2  11818  ef0lem  11942  efexp  11964  nndivides  12079  modmulconst  12105  dvdsflip  12133  nn0enne  12184  nno  12188  divalgmod  12209  ndvdsadd  12213  modgcd  12283  gcddiv  12311  gcdmultiple  12312  gcdmultiplez  12313  rpmulgcd  12318  rplpwr  12319  sqgcd  12321  lcmgcdlem  12370  qredeq  12389  qredeu  12390  divgcdcoprm0  12394  cncongrcoprm  12399  prmind2  12413  isprm6  12440  sqrt2irr  12455  oddpwdclemodd  12465  divnumden  12489  divdenle  12490  nn0gcdsq  12493  hashgcdlem  12531  pythagtriplem1  12559  pythagtriplem2  12560  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem15  12572  pythagtriplem16  12573  pythagtriplem17  12574  pythagtriplem19  12576  pcqcl  12600  pcexp  12603  pcneg  12619  fldivp1  12642  oddprmdvds  12648  prmpwdvds  12649  infpnlem2  12654  4sqlem19  12703  mulgnegnn  13439  mulgnnass  13464  mulgmodid  13468  cnfldmulg  14309  znidomb  14391  znrrg  14393  dvexp  15154  rpcxproot  15357  logbgcd1irr  15410  perfect  15444  lgssq2  15489  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  2lgslem1a1  15534  2sqlem6  15568  2sqlem10  15573