Theorem nncn 9312

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   NNcn 9304

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9305

This theorem is used by:  nn1m1nn  9322  nn1suc  9323  nnaddcl  9324  nnmulcl  9325  nnsub  9343  nndiv  9345  nndivtr  9346  nnnn0addcl  9593  nn0nnaddcl  9594  elnnnn0  9606  nnnegz  9647  zaddcllempos  9681  zaddcllemneg  9683  nnaddm1cl  9706  elz2  9716  zdiv  9734  zdivadd  9735  zdivmul  9736  nneoor  9748  nneo  9749  divfnzn  10021  qmulz  10023  qaddcl  10035  qnegcl  10036  qmulcl  10037  qreccl  10042  nnledivrp  10167  nn0ledivnn  10168  fseq1m1p1  10502  nnsplit  10544  ubmelm1fzo  10644  subfzo0  10661  flqdiv  10758  addmodidr  10810  modfzo0difsn  10832  nn0ennn  10870  expnegap0  10984  expm1t  11004  nnsqcl  11046  nnlesq  11080  facdiv  11176  facndiv  11177  faclbnd  11179  bcn1  11196  bcn2m1  11208  arisum  12265  arisum2  12266  expcnvap0  12269  mertenslem2  12303  ef0lem  12427  efexp  12449  nndivides  12564  modmulconst  12590  dvdsflip  12618  nn0enne  12669  nno  12673  divalgmod  12694  ndvdsadd  12698  modgcd  12768  gcddiv  12796  gcdmultiple  12797  gcdmultiplez  12798  rpmulgcd  12803  rplpwr  12804  sqgcd  12806  lcmgcdlem  12855  qredeq  12874  qredeu  12875  divgcdcoprm0  12879  cncongrcoprm  12884  prmind2  12898  isprm6  12925  sqrt2irr  12940  oddpwdclemodd  12950  divnumden  12974  divdenle  12975  nn0gcdsq  12978  hashgcdlem  13016  pythagtriplem1  13044  pythagtriplem2  13045  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  pythagtriplem19  13061  pcqcl  13085  pcexp  13088  pcneg  13104  fldivp1  13127  oddprmdvds  13133  prmpwdvds  13134  infpnlem2  13139  4sqlem19  13188  mulgnegnn  13935  mulgnnass  13960  mulgmodid  13964  cnfldmulg  14913  znidomb  14993  znrrg  14995  dvexp  15812  rpcxproot  16016  logbgcd1irr  16069  birthdaylem2  16088  pellexlem1  16091  perfect  16115  lgssq2  16160  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  2lgslem1a1  16205  2sqlem6  16239  2sqlem10  16244