Theorem nncn 9141

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8020   NNcn 9133

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9134

This theorem is referenced by:  nn1m1nn  9151  nn1suc  9152  nnaddcl  9153  nnmulcl  9154  nnsub  9172  nndiv  9174  nndivtr  9175  nnnn0addcl  9422  nn0nnaddcl  9423  elnnnn0  9435  nnnegz  9472  zaddcllempos  9506  zaddcllemneg  9508  nnaddm1cl  9531  elz2  9541  zdiv  9558  zdivadd  9559  zdivmul  9560  nneoor  9572  nneo  9573  divfnzn  9845  qmulz  9847  qaddcl  9859  qnegcl  9860  qmulcl  9861  qreccl  9866  nnledivrp  9991  nn0ledivnn  9992  fseq1m1p1  10320  nnsplit  10362  ubmelm1fzo  10461  subfzo0  10478  flqdiv  10573  addmodidr  10625  modfzo0difsn  10647  nn0ennn  10685  expnegap0  10799  expm1t  10819  nnsqcl  10861  nnlesq  10895  facdiv  10990  facndiv  10991  faclbnd  10993  bcn1  11010  bcn2m1  11021  arisum  12049  arisum2  12050  expcnvap0  12053  mertenslem2  12087  ef0lem  12211  efexp  12233  nndivides  12348  modmulconst  12374  dvdsflip  12402  nn0enne  12453  nno  12457  divalgmod  12478  ndvdsadd  12482  modgcd  12552  gcddiv  12580  gcdmultiple  12581  gcdmultiplez  12582  rpmulgcd  12587  rplpwr  12588  sqgcd  12590  lcmgcdlem  12639  qredeq  12658  qredeu  12659  divgcdcoprm0  12663  cncongrcoprm  12668  prmind2  12682  isprm6  12709  sqrt2irr  12724  oddpwdclemodd  12734  divnumden  12758  divdenle  12759  nn0gcdsq  12762  hashgcdlem  12800  pythagtriplem1  12828  pythagtriplem2  12829  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  pythagtriplem19  12845  pcqcl  12869  pcexp  12872  pcneg  12888  fldivp1  12911  oddprmdvds  12917  prmpwdvds  12918  infpnlem2  12923  4sqlem19  12972  mulgnegnn  13709  mulgnnass  13734  mulgmodid  13738  cnfldmulg  14580  znidomb  14662  znrrg  14664  dvexp  15425  rpcxproot  15628  logbgcd1irr  15681  perfect  15715  lgssq2  15760  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  2lgslem1a1  15805  2sqlem6  15839  2sqlem10  15844