Theorem nncn 9262

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   NNcn 9254

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9255

This theorem is referenced by:  nn1m1nn  9272  nn1suc  9273  nnaddcl  9274  nnmulcl  9275  nnsub  9293  nndiv  9295  nndivtr  9296  nnnn0addcl  9543  nn0nnaddcl  9544  elnnnn0  9556  nnnegz  9597  zaddcllempos  9631  zaddcllemneg  9633  nnaddm1cl  9656  elz2  9666  zdiv  9684  zdivadd  9685  zdivmul  9686  nneoor  9698  nneo  9699  divfnzn  9971  qmulz  9973  qaddcl  9985  qnegcl  9986  qmulcl  9987  qreccl  9992  nnledivrp  10117  nn0ledivnn  10118  fseq1m1p1  10451  nnsplit  10493  ubmelm1fzo  10593  subfzo0  10610  flqdiv  10707  addmodidr  10759  modfzo0difsn  10781  nn0ennn  10819  expnegap0  10933  expm1t  10953  nnsqcl  10995  nnlesq  11029  facdiv  11125  facndiv  11126  faclbnd  11128  bcn1  11145  bcn2m1  11157  arisum  12209  arisum2  12210  expcnvap0  12213  mertenslem2  12247  ef0lem  12371  efexp  12393  nndivides  12508  modmulconst  12534  dvdsflip  12562  nn0enne  12613  nno  12617  divalgmod  12638  ndvdsadd  12642  modgcd  12712  gcddiv  12740  gcdmultiple  12741  gcdmultiplez  12742  rpmulgcd  12747  rplpwr  12748  sqgcd  12750  lcmgcdlem  12799  qredeq  12818  qredeu  12819  divgcdcoprm0  12823  cncongrcoprm  12828  prmind2  12842  isprm6  12869  sqrt2irr  12884  oddpwdclemodd  12894  divnumden  12918  divdenle  12919  nn0gcdsq  12922  hashgcdlem  12960  pythagtriplem1  12988  pythagtriplem2  12989  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  pythagtriplem19  13005  pcqcl  13029  pcexp  13032  pcneg  13048  fldivp1  13071  oddprmdvds  13077  prmpwdvds  13078  infpnlem2  13083  4sqlem19  13132  mulgnegnn  13885  mulgnnass  13910  mulgmodid  13914  cnfldmulg  14850  znidomb  14932  znrrg  14934  dvexp  15702  rpcxproot  15905  logbgcd1irr  15958  pellexlem1  15971  perfect  15995  lgssq2  16040  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  2lgslem1a1  16085  2sqlem6  16119  2sqlem10  16124