Theorem nncn 9321

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 9318	. 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 8183   NNcn 9313

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

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 9314

This theorem is used by:  nn1m1nn  9331  nn1suc  9332  nnaddcl  9333  nnmulcl  9334  nnsub  9352  nndiv  9354  nndivtr  9355  nnnn0addcl  9604  nn0nnaddcl  9605  elnnnn0  9617  nnnegz  9656  zaddcllempos  9690  zaddcllemneg  9692  nnaddm1cl  9715  elz2  9725  zdiv  9744  zdivadd  9745  zdivmul  9746  nneoor  9758  nneo  9759  divfnzn  10036  qmulz  10038  qaddcl  10050  qnegcl  10051  qmulcl  10052  qreccl  10057  nnledivrp  10183  nn0ledivnn  10184  fseq1m1p1  10518  nnsplit  10560  ubmelm1fzo  10660  subfzo0  10677  flqdiv  10778  addmodidr  10830  modfzo0difsn  10852  nn0ennn  10890  expnegap0  11004  expm1t  11024  nnsqcl  11066  nnlesq  11100  facdiv  11197  facndiv  11198  faclbnd  11200  bcn1  11217  bcn2m1  11229  arisum  12289  arisum2  12290  expcnvap0  12293  mertenslem2  12327  ef0lem  12451  efexp  12473  nndivides  12588  modmulconst  12614  dvdsflip  12642  nn0enne  12693  nno  12697  divalgmod  12718  ndvdsadd  12722  modgcd  12792  gcddiv  12820  gcdmultiple  12821  gcdmultiplez  12822  rpmulgcd  12827  rplpwr  12828  sqgcd  12830  lcmgcdlem  12879  qredeq  12898  qredeu  12899  divgcdcoprm0  12903  cncongrcoprm  12908  prmind2  12922  isprm6  12950  sqrt2irr  12965  divnumden  13000  divdenle  13001  nn0gcdsq  13004  hashgcdlem  13044  pythagtriplem1  13072  pythagtriplem2  13073  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  pythagtriplem19  13089  pcqcl  13113  pcexp  13116  pcneg  13132  fldivp1  13155  oddprmdvds  13161  prmpwdvds  13162  infpnlem2  13167  4sqlem19  13216  mulgnegnn  13993  mulgnnass  14018  mulgmodid  14022  cnfldmulg  15021  znidomb  15101  znrrg  15103  dvexp  15954  root1idef  16101  rpcxproot  16164  efnthr  16193  logbgcd1irr  16220  birthdaylem2  16243  pellexlem1  16246  chtublem  16312  perfect  16318  pcbcctr  16320  bclbnd  16324  bposlem1  16328  bposlem6  16333  lgssq2  16382  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  2lgslem1a1  16427  2sqlem6  16461  2sqlem10  16466