Theorem nncnd 8906

Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nncnd	|- ( ph -> A e. CC )

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 8897	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3151	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2146   CCcc 7784   NNcn 8892

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737  df-in 3133  df-ss 3140  df-int 3841  df-inn 8893

This theorem is referenced by:  peano5uzti  9334  qapne  9612  qtri3or  10213  exbtwnzlemstep  10218  intfracq  10290  flqdiv  10291  modqmulnn  10312  addmodid  10342  modaddmodup  10357  modsumfzodifsn  10366  addmodlteq  10368  facdiv  10686  facndiv  10687  faclbnd  10689  faclbnd6  10692  facubnd  10693  facavg  10694  bccmpl  10702  bcn0  10703  bcn1  10706  bcm1k  10708  bcp1n  10709  bcp1nk  10710  bcval5  10711  bcpasc  10714  permnn  10719  cvg1nlemcxze  10959  cvg1nlemcau  10961  resqrexlemcalc3  10993  binom11  11462  binom1dif  11463  divcnv  11473  arisum2  11475  trireciplem  11476  trirecip  11477  expcnvap0  11478  geo2sum  11490  geo2lim  11492  cvgratnnlembern  11499  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  cvgratnnlemsumlt  11504  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratz  11508  eftcl  11630  eftabs  11632  efcllemp  11634  ege2le3  11647  efcj  11649  efaddlem  11650  eftlub  11666  eirraplem  11752  oexpneg  11849  divalglemnn  11890  dvdsgcdidd  11962  bezoutlemnewy  11964  mulgcd  11984  rplpwr  11995  sqgcd  11997  lcmgcdlem  12044  3lcm2e6woprm  12053  cncongr1  12070  cncongr2  12071  prmind2  12087  isprm5  12109  divgcdodd  12110  prmdvdsexpr  12117  sqrt2irrlem  12128  oddpwdclemxy  12136  oddpwdclemodd  12139  oddpwdclemdc  12140  oddpwdc  12141  sqpweven  12142  2sqpwodd  12143  sqrt2irraplemnn  12146  sqrt2irrap  12147  qmuldeneqnum  12162  divnumden  12163  qnumgt0  12165  numdensq  12169  hashdvds  12188  phiprmpw  12189  prmdiv  12202  prmdivdiv  12204  phisum  12207  modprm0  12221  pythagtriplem4  12235  pythagtriplem6  12237  pythagtriplem7  12238  pythagtriplem14  12244  pythagtriplem15  12245  pythagtriplem16  12246  pythagtriplem19  12249  pythagtrip  12250  pcprendvds2  12258  pcpre1  12259  pcpremul  12260  pceulem  12261  pcdiv  12269  pcqmul  12270  pcelnn  12287  pcid  12290  pc2dvds  12296  dvdsprmpweqnn  12302  dvdsprmpweqle  12303  pcaddlem  12305  pcadd  12306  pcfaclem  12314  qexpz  12317  expnprm  12318  oddprmdvds  12319  prmpwdvds  12320  pockthlem  12321  pockthg  12322  infpnlem1  12324  4sqlem6  12348  4sqlem7  12349  4sqlem10  12352  mul4sqlem  12358  oddennn  12360  evenennn  12361  mulgnndir  12881  mulgnnass  12887  logbgcd1irraplemap  13967  lgsval2lem  13991  2sqlem3  14033  2sqlem4  14034  trilpolemeq1  14358  trilpolemlt1  14359  redcwlpolemeq1  14372  nconstwlpolemgt0  14381