Theorem nncn 9245

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

Syntax hints:   -> wi 4   e. wcel 2203   CCcc 8125   NNcn 9237

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 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-in 3217  df-ss 3224  df-int 3950  df-inn 9238

This theorem is referenced by:  nn1m1nn  9255  nn1suc  9256  nnaddcl  9257  nnmulcl  9258  nnsub  9276  nndiv  9278  nndivtr  9279  nnnn0addcl  9526  nn0nnaddcl  9527  elnnnn0  9539  nnnegz  9580  zaddcllempos  9614  zaddcllemneg  9616  nnaddm1cl  9639  elz2  9649  zdiv  9666  zdivadd  9667  zdivmul  9668  nneoor  9680  nneo  9681  divfnzn  9953  qmulz  9955  qaddcl  9967  qnegcl  9968  qmulcl  9969  qreccl  9974  nnledivrp  10099  nn0ledivnn  10100  fseq1m1p1  10429  nnsplit  10471  ubmelm1fzo  10571  subfzo0  10588  flqdiv  10683  addmodidr  10735  modfzo0difsn  10757  nn0ennn  10795  expnegap0  10909  expm1t  10929  nnsqcl  10971  nnlesq  11005  facdiv  11100  facndiv  11101  faclbnd  11103  bcn1  11120  bcn2m1  11132  arisum  12184  arisum2  12185  expcnvap0  12188  mertenslem2  12222  ef0lem  12346  efexp  12368  nndivides  12483  modmulconst  12509  dvdsflip  12537  nn0enne  12588  nno  12592  divalgmod  12613  ndvdsadd  12617  modgcd  12687  gcddiv  12715  gcdmultiple  12716  gcdmultiplez  12717  rpmulgcd  12722  rplpwr  12723  sqgcd  12725  lcmgcdlem  12774  qredeq  12793  qredeu  12794  divgcdcoprm0  12798  cncongrcoprm  12803  prmind2  12817  isprm6  12844  sqrt2irr  12859  oddpwdclemodd  12869  divnumden  12893  divdenle  12894  nn0gcdsq  12897  hashgcdlem  12935  pythagtriplem1  12963  pythagtriplem2  12964  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  pythagtriplem19  12980  pcqcl  13004  pcexp  13007  pcneg  13023  fldivp1  13046  oddprmdvds  13052  prmpwdvds  13053  infpnlem2  13058  4sqlem19  13107  mulgnegnn  13849  mulgnnass  13874  mulgmodid  13878  cnfldmulg  14724  znidomb  14806  znrrg  14808  dvexp  15576  rpcxproot  15779  logbgcd1irr  15832  pellexlem1  15845  perfect  15869  lgssq2  15914  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  2lgslem1a1  15959  2sqlem6  15993  2sqlem10  15998