Theorem nncn 9154

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8033   NNcn 9146

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8126  ax-resscn 8127  ax-1re 8129  ax-addrcl 8132

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9147

This theorem is referenced by:  nn1m1nn  9164  nn1suc  9165  nnaddcl  9166  nnmulcl  9167  nnsub  9185  nndiv  9187  nndivtr  9188  nnnn0addcl  9435  nn0nnaddcl  9436  elnnnn0  9448  nnnegz  9485  zaddcllempos  9519  zaddcllemneg  9521  nnaddm1cl  9544  elz2  9554  zdiv  9571  zdivadd  9572  zdivmul  9573  nneoor  9585  nneo  9586  divfnzn  9858  qmulz  9860  qaddcl  9872  qnegcl  9873  qmulcl  9874  qreccl  9879  nnledivrp  10004  nn0ledivnn  10005  fseq1m1p1  10333  nnsplit  10375  ubmelm1fzo  10475  subfzo0  10492  flqdiv  10587  addmodidr  10639  modfzo0difsn  10661  nn0ennn  10699  expnegap0  10813  expm1t  10833  nnsqcl  10875  nnlesq  10909  facdiv  11004  facndiv  11005  faclbnd  11007  bcn1  11024  bcn2m1  11035  arisum  12080  arisum2  12081  expcnvap0  12084  mertenslem2  12118  ef0lem  12242  efexp  12264  nndivides  12379  modmulconst  12405  dvdsflip  12433  nn0enne  12484  nno  12488  divalgmod  12509  ndvdsadd  12513  modgcd  12583  gcddiv  12611  gcdmultiple  12612  gcdmultiplez  12613  rpmulgcd  12618  rplpwr  12619  sqgcd  12621  lcmgcdlem  12670  qredeq  12689  qredeu  12690  divgcdcoprm0  12694  cncongrcoprm  12699  prmind2  12713  isprm6  12740  sqrt2irr  12755  oddpwdclemodd  12765  divnumden  12789  divdenle  12790  nn0gcdsq  12793  hashgcdlem  12831  pythagtriplem1  12859  pythagtriplem2  12860  pythagtriplem6  12864  pythagtriplem7  12865  pythagtriplem12  12869  pythagtriplem14  12871  pythagtriplem15  12872  pythagtriplem16  12873  pythagtriplem17  12874  pythagtriplem19  12876  pcqcl  12900  pcexp  12903  pcneg  12919  fldivp1  12942  oddprmdvds  12948  prmpwdvds  12949  infpnlem2  12954  4sqlem19  13003  mulgnegnn  13740  mulgnnass  13765  mulgmodid  13769  cnfldmulg  14612  znidomb  14694  znrrg  14696  dvexp  15462  rpcxproot  15665  logbgcd1irr  15718  perfect  15752  lgssq2  15797  gausslemma2dlem1a  15814  gausslemma2dlem3  15819  2lgslem1a1  15842  2sqlem6  15876  2sqlem10  15881