Theorem nncn 8861

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

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7747   NNcn 8853

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099  ax-cnex 7840  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-v 2727  df-in 3121  df-ss 3128  df-int 3824  df-inn 8854

This theorem is referenced by:  nn1m1nn  8871  nn1suc  8872  nnaddcl  8873  nnmulcl  8874  nnsub  8892  nndiv  8894  nndivtr  8895  nnnn0addcl  9140  nn0nnaddcl  9141  elnnnn0  9153  nnnegz  9190  zaddcllempos  9224  zaddcllemneg  9226  nnaddm1cl  9248  elz2  9258  zdiv  9275  zdivadd  9276  zdivmul  9277  nneoor  9289  nneo  9290  divfnzn  9555  qmulz  9557  qaddcl  9569  qnegcl  9570  qmulcl  9571  qreccl  9576  nnledivrp  9698  nn0ledivnn  9699  fseq1m1p1  10026  nnsplit  10068  ubmelm1fzo  10157  subfzo0  10173  flqdiv  10252  addmodidr  10304  modfzo0difsn  10326  nn0ennn  10364  expnegap0  10459  expm1t  10479  nnsqcl  10520  nnlesq  10554  facdiv  10647  facndiv  10648  faclbnd  10650  bcn1  10667  bcn2m1  10678  arisum  11435  arisum2  11436  expcnvap0  11439  mertenslem2  11473  ef0lem  11597  efexp  11619  nndivides  11733  modmulconst  11759  dvdsflip  11785  nn0enne  11835  nno  11839  divalgmod  11860  ndvdsadd  11864  modgcd  11920  gcddiv  11948  gcdmultiple  11949  gcdmultiplez  11950  rpmulgcd  11955  rplpwr  11956  sqgcd  11958  lcmgcdlem  12005  qredeq  12024  qredeu  12025  divgcdcoprm0  12029  cncongrcoprm  12034  prmind2  12048  isprm6  12075  sqrt2irr  12090  oddpwdclemodd  12100  divnumden  12124  divdenle  12125  nn0gcdsq  12128  hashgcdlem  12166  pythagtriplem1  12193  pythagtriplem2  12194  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  pythagtriplem19  12210  pcqcl  12234  pcexp  12237  pcneg  12252  fldivp1  12274  oddprmdvds  12280  prmpwdvds  12281  infpnlem2  12286  dvexp  13275  rpcxproot  13434  logbgcd1irr  13485  lgssq2  13542  2sqlem6  13556  2sqlem10  13561