Theorem nncn 9114

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7993   NNcn 9106

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 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

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 2801  df-in 3203  df-ss 3210  df-int 3923  df-inn 9107

This theorem is referenced by:  nn1m1nn  9124  nn1suc  9125  nnaddcl  9126  nnmulcl  9127  nnsub  9145  nndiv  9147  nndivtr  9148  nnnn0addcl  9395  nn0nnaddcl  9396  elnnnn0  9408  nnnegz  9445  zaddcllempos  9479  zaddcllemneg  9481  nnaddm1cl  9504  elz2  9514  zdiv  9531  zdivadd  9532  zdivmul  9533  nneoor  9545  nneo  9546  divfnzn  9812  qmulz  9814  qaddcl  9826  qnegcl  9827  qmulcl  9828  qreccl  9833  nnledivrp  9958  nn0ledivnn  9959  fseq1m1p1  10287  nnsplit  10329  ubmelm1fzo  10427  subfzo0  10443  flqdiv  10538  addmodidr  10590  modfzo0difsn  10612  nn0ennn  10650  expnegap0  10764  expm1t  10784  nnsqcl  10826  nnlesq  10860  facdiv  10955  facndiv  10956  faclbnd  10958  bcn1  10975  bcn2m1  10986  arisum  12004  arisum2  12005  expcnvap0  12008  mertenslem2  12042  ef0lem  12166  efexp  12188  nndivides  12303  modmulconst  12329  dvdsflip  12357  nn0enne  12408  nno  12412  divalgmod  12433  ndvdsadd  12437  modgcd  12507  gcddiv  12535  gcdmultiple  12536  gcdmultiplez  12537  rpmulgcd  12542  rplpwr  12543  sqgcd  12545  lcmgcdlem  12594  qredeq  12613  qredeu  12614  divgcdcoprm0  12618  cncongrcoprm  12623  prmind2  12637  isprm6  12664  sqrt2irr  12679  oddpwdclemodd  12689  divnumden  12713  divdenle  12714  nn0gcdsq  12717  hashgcdlem  12755  pythagtriplem1  12783  pythagtriplem2  12784  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  pythagtriplem19  12800  pcqcl  12824  pcexp  12827  pcneg  12843  fldivp1  12866  oddprmdvds  12872  prmpwdvds  12873  infpnlem2  12878  4sqlem19  12927  mulgnegnn  13664  mulgnnass  13689  mulgmodid  13693  cnfldmulg  14534  znidomb  14616  znrrg  14618  dvexp  15379  rpcxproot  15582  logbgcd1irr  15635  perfect  15669  lgssq2  15714  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  2lgslem1a1  15759  2sqlem6  15793  2sqlem10  15798