Theorem nncn 8927

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7809   NNcn 8919

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740  df-in 3136  df-ss 3143  df-int 3846  df-inn 8920

This theorem is referenced by:  nn1m1nn  8937  nn1suc  8938  nnaddcl  8939  nnmulcl  8940  nnsub  8958  nndiv  8960  nndivtr  8961  nnnn0addcl  9206  nn0nnaddcl  9207  elnnnn0  9219  nnnegz  9256  zaddcllempos  9290  zaddcllemneg  9292  nnaddm1cl  9314  elz2  9324  zdiv  9341  zdivadd  9342  zdivmul  9343  nneoor  9355  nneo  9356  divfnzn  9621  qmulz  9623  qaddcl  9635  qnegcl  9636  qmulcl  9637  qreccl  9642  nnledivrp  9766  nn0ledivnn  9767  fseq1m1p1  10095  nnsplit  10137  ubmelm1fzo  10226  subfzo0  10242  flqdiv  10321  addmodidr  10373  modfzo0difsn  10395  nn0ennn  10433  expnegap0  10528  expm1t  10548  nnsqcl  10590  nnlesq  10624  facdiv  10718  facndiv  10719  faclbnd  10721  bcn1  10738  bcn2m1  10749  arisum  11506  arisum2  11507  expcnvap0  11510  mertenslem2  11544  ef0lem  11668  efexp  11690  nndivides  11804  modmulconst  11830  dvdsflip  11857  nn0enne  11907  nno  11911  divalgmod  11932  ndvdsadd  11936  modgcd  11992  gcddiv  12020  gcdmultiple  12021  gcdmultiplez  12022  rpmulgcd  12027  rplpwr  12028  sqgcd  12030  lcmgcdlem  12077  qredeq  12096  qredeu  12097  divgcdcoprm0  12101  cncongrcoprm  12106  prmind2  12120  isprm6  12147  sqrt2irr  12162  oddpwdclemodd  12172  divnumden  12196  divdenle  12197  nn0gcdsq  12200  hashgcdlem  12238  pythagtriplem1  12265  pythagtriplem2  12266  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  pythagtriplem19  12282  pcqcl  12306  pcexp  12309  pcneg  12324  fldivp1  12346  oddprmdvds  12352  prmpwdvds  12353  infpnlem2  12358  mulgnegnn  12993  mulgnnass  13018  mulgmodid  13022  cnfldmulg  13473  dvexp  14178  rpcxproot  14337  logbgcd1irr  14388  lgssq2  14445  2sqlem6  14470  2sqlem10  14475