Theorem nncn 9314

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 9311	. 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 9306

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 9307

This theorem is used by:  nn1m1nn  9324  nn1suc  9325  nnaddcl  9326  nnmulcl  9327  nnsub  9345  nndiv  9347  nndivtr  9348  nnnn0addcl  9597  nn0nnaddcl  9598  elnnnn0  9610  nnnegz  9651  zaddcllempos  9685  zaddcllemneg  9687  nnaddm1cl  9710  elz2  9720  zdiv  9738  zdivadd  9739  zdivmul  9740  nneoor  9752  nneo  9753  divfnzn  10030  qmulz  10032  qaddcl  10044  qnegcl  10045  qmulcl  10046  qreccl  10051  nnledivrp  10177  nn0ledivnn  10178  fseq1m1p1  10512  nnsplit  10554  ubmelm1fzo  10654  subfzo0  10671  flqdiv  10771  addmodidr  10823  modfzo0difsn  10845  nn0ennn  10883  expnegap0  10997  expm1t  11017  nnsqcl  11059  nnlesq  11093  facdiv  11190  facndiv  11191  faclbnd  11193  bcn1  11210  bcn2m1  11222  arisum  12281  arisum2  12282  expcnvap0  12285  mertenslem2  12319  ef0lem  12443  efexp  12465  nndivides  12580  modmulconst  12606  dvdsflip  12634  nn0enne  12685  nno  12689  divalgmod  12710  ndvdsadd  12714  modgcd  12784  gcddiv  12812  gcdmultiple  12813  gcdmultiplez  12814  rpmulgcd  12819  rplpwr  12820  sqgcd  12822  lcmgcdlem  12871  qredeq  12890  qredeu  12891  divgcdcoprm0  12895  cncongrcoprm  12900  prmind2  12914  isprm6  12942  sqrt2irr  12957  divnumden  12992  divdenle  12993  nn0gcdsq  12996  hashgcdlem  13036  pythagtriplem1  13064  pythagtriplem2  13065  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  pythagtriplem19  13081  pcqcl  13105  pcexp  13108  pcneg  13124  fldivp1  13147  oddprmdvds  13153  prmpwdvds  13154  infpnlem2  13159  4sqlem19  13208  mulgnegnn  13984  mulgnnass  14009  mulgmodid  14013  cnfldmulg  14962  znidomb  15042  znrrg  15044  dvexp  15861  rpcxproot  16069  logbgcd1irr  16122  birthdaylem2  16145  pellexlem1  16148  perfect  16199  pcbcctr  16201  bclbnd  16205  bposlem1  16209  lgssq2  16258  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  2lgslem1a1  16303  2sqlem6  16337  2sqlem10  16342