Theorem nncn 8721

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

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7611   NNcn 8713

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-cnex 7704  ax-resscn 7705  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-v 2683  df-in 3072  df-ss 3079  df-int 3767  df-inn 8714

This theorem is referenced by:  nn1m1nn  8731  nn1suc  8732  nnaddcl  8733  nnmulcl  8734  nnsub  8752  nndiv  8754  nndivtr  8755  nnnn0addcl  9000  nn0nnaddcl  9001  elnnnn0  9013  nnnegz  9050  zaddcllempos  9084  zaddcllemneg  9086  nnaddm1cl  9108  elz2  9115  zdiv  9132  zdivadd  9133  zdivmul  9134  nneoor  9146  nneo  9147  divfnzn  9406  qmulz  9408  qaddcl  9420  qnegcl  9421  qmulcl  9422  qreccl  9427  nnledivrp  9546  nn0ledivnn  9547  fseq1m1p1  9868  nnsplit  9907  ubmelm1fzo  9996  subfzo0  10012  flqdiv  10087  addmodidr  10139  modfzo0difsn  10161  nn0ennn  10199  expnegap0  10294  expm1t  10314  nnsqcl  10355  nnlesq  10389  facdiv  10477  facndiv  10478  faclbnd  10480  bcn1  10497  bcn2m1  10508  arisum  11260  arisum2  11261  expcnvap0  11264  mertenslem2  11298  ef0lem  11355  efexp  11377  nndivides  11489  modmulconst  11514  dvdsflip  11538  nn0enne  11588  nno  11592  divalgmod  11613  ndvdsadd  11617  modgcd  11668  gcddiv  11696  gcdmultiple  11697  gcdmultiplez  11698  rpmulgcd  11703  rplpwr  11704  sqgcd  11706  lcmgcdlem  11747  qredeq  11766  qredeu  11767  divgcdcoprm0  11771  cncongrcoprm  11776  prmind2  11790  isprm6  11814  sqrt2irr  11829  oddpwdclemodd  11839  divnumden  11863  divdenle  11864  nn0gcdsq  11867  hashgcdlem  11892  dvexp  12833