Theorem nncn 9193

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8073   NNcn 9185

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-in 3207  df-ss 3214  df-int 3934  df-inn 9186

This theorem is referenced by:  nn1m1nn  9203  nn1suc  9204  nnaddcl  9205  nnmulcl  9206  nnsub  9224  nndiv  9226  nndivtr  9227  nnnn0addcl  9474  nn0nnaddcl  9475  elnnnn0  9487  nnnegz  9526  zaddcllempos  9560  zaddcllemneg  9562  nnaddm1cl  9585  elz2  9595  zdiv  9612  zdivadd  9613  zdivmul  9614  nneoor  9626  nneo  9627  divfnzn  9899  qmulz  9901  qaddcl  9913  qnegcl  9914  qmulcl  9915  qreccl  9920  nnledivrp  10045  nn0ledivnn  10046  fseq1m1p1  10375  nnsplit  10417  ubmelm1fzo  10517  subfzo0  10534  flqdiv  10629  addmodidr  10681  modfzo0difsn  10703  nn0ennn  10741  expnegap0  10855  expm1t  10875  nnsqcl  10917  nnlesq  10951  facdiv  11046  facndiv  11047  faclbnd  11049  bcn1  11066  bcn2m1  11077  arisum  12122  arisum2  12123  expcnvap0  12126  mertenslem2  12160  ef0lem  12284  efexp  12306  nndivides  12421  modmulconst  12447  dvdsflip  12475  nn0enne  12526  nno  12530  divalgmod  12551  ndvdsadd  12555  modgcd  12625  gcddiv  12653  gcdmultiple  12654  gcdmultiplez  12655  rpmulgcd  12660  rplpwr  12661  sqgcd  12663  lcmgcdlem  12712  qredeq  12731  qredeu  12732  divgcdcoprm0  12736  cncongrcoprm  12741  prmind2  12755  isprm6  12782  sqrt2irr  12797  oddpwdclemodd  12807  divnumden  12831  divdenle  12832  nn0gcdsq  12835  hashgcdlem  12873  pythagtriplem1  12901  pythagtriplem2  12902  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  pythagtriplem19  12918  pcqcl  12942  pcexp  12945  pcneg  12961  fldivp1  12984  oddprmdvds  12990  prmpwdvds  12991  infpnlem2  12996  4sqlem19  13045  mulgnegnn  13782  mulgnnass  13807  mulgmodid  13811  cnfldmulg  14655  znidomb  14737  znrrg  14739  dvexp  15505  rpcxproot  15708  logbgcd1irr  15761  pellexlem1  15774  perfect  15798  lgssq2  15843  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  2lgslem1a1  15888  2sqlem6  15922  2sqlem10  15927