Theorem nncnd 9157

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 9148	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3225	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   NNcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  peano5uzti  9588  qapne  9873  qtri3or  10501  exbtwnzlemstep  10508  intfracq  10583  flqdiv  10584  modqmulnn  10605  addmodid  10635  modaddmodup  10650  modsumfzodifsn  10659  addmodlteq  10661  facdiv  11001  facndiv  11002  faclbnd  11004  faclbnd6  11007  facubnd  11008  facavg  11009  bccmpl  11017  bcn0  11018  bcn1  11021  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcpasc  11029  permnn  11034  cvg1nlemcxze  11547  cvg1nlemcau  11549  resqrexlemcalc3  11581  binom11  12052  binom1dif  12053  divcnv  12063  arisum2  12065  trireciplem  12066  trirecip  12067  expcnvap0  12068  geo2sum  12080  geo2lim  12082  cvgratnnlembern  12089  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemsumlt  12094  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratz  12098  eftcl  12220  eftabs  12222  efcllemp  12224  ege2le3  12237  efcj  12239  efaddlem  12240  eftlub  12256  eirraplem  12343  oexpneg  12443  divalglemnn  12484  bitsp1  12517  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitscmp  12524  bitsinv1lem  12527  bitsinv1  12528  dvdsgcdidd  12570  bezoutlemnewy  12572  mulgcd  12592  rplpwr  12603  sqgcd  12605  lcmgcdlem  12654  3lcm2e6woprm  12663  cncongr1  12680  cncongr2  12681  prmind2  12697  isprm5  12719  divgcdodd  12720  prmdvdsexpr  12727  sqrt2irrlem  12738  oddpwdclemxy  12746  oddpwdclemodd  12749  oddpwdclemdc  12750  oddpwdc  12751  sqpweven  12752  2sqpwodd  12753  sqrt2irraplemnn  12756  sqrt2irrap  12757  qmuldeneqnum  12772  divnumden  12773  qnumgt0  12775  numdensq  12779  hashdvds  12798  phiprmpw  12799  prmdiv  12812  prmdivdiv  12814  phisum  12818  modprm0  12832  pythagtriplem4  12846  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem14  12855  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem19  12860  pythagtrip  12861  pcprendvds2  12869  pcpre1  12870  pcpremul  12871  pceulem  12872  pcdiv  12880  pcqmul  12881  pcelnn  12899  pcid  12902  pc2dvds  12908  dvdsprmpweqnn  12914  dvdsprmpweqle  12915  pcaddlem  12917  pcadd  12918  pcfaclem  12927  qexpz  12930  expnprm  12931  oddprmdvds  12932  prmpwdvds  12933  pockthlem  12934  pockthg  12935  infpnlem1  12937  4sqlem6  12961  4sqlem7  12962  4sqlem10  12965  mul4sqlem  12971  4sqlem11  12979  4sqlem12  12980  4sqlem14  12982  4sqlem17  12985  4sqlem18  12986  oddennn  13018  evenennn  13019  mulgnndir  13743  mulgnnass  13749  znrrg  14680  logbgcd1irraplemap  15699  wilthlem1  15710  0sgm  15715  mpodvdsmulf1o  15720  1sgmprm  15724  1sgm2ppw  15725  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsval2lem  15745  gausslemma2dlem6  15802  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2  15818  m1lgs  15820  2sqlem3  15852  2sqlem4  15853  trilpolemeq1  16670  trilpolemlt1  16671  redcwlpolemeq1  16685  nconstwlpolemgt0  16695