Theorem nncnd 9199

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8073   NNcn 9185

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-in 3207  df-ss 3214  df-int 3934  df-inn 9186

This theorem is referenced by:  peano5uzti  9632  qapne  9917  qtri3or  10546  exbtwnzlemstep  10553  intfracq  10628  flqdiv  10629  modqmulnn  10650  addmodid  10680  modaddmodup  10695  modsumfzodifsn  10704  addmodlteq  10706  facdiv  11046  facndiv  11047  faclbnd  11049  faclbnd6  11052  facubnd  11053  facavg  11054  bccmpl  11062  bcn0  11063  bcn1  11066  bcm1k  11068  bcp1n  11069  bcp1nk  11070  bcval5  11071  bcpasc  11074  permnn  11079  cvg1nlemcxze  11605  cvg1nlemcau  11607  resqrexlemcalc3  11639  binom11  12110  binom1dif  12111  divcnv  12121  arisum2  12123  trireciplem  12124  trirecip  12125  expcnvap0  12126  geo2sum  12138  geo2lim  12140  cvgratnnlembern  12147  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratz  12156  eftcl  12278  eftabs  12280  efcllemp  12282  ege2le3  12295  efcj  12297  efaddlem  12298  eftlub  12314  eirraplem  12401  oexpneg  12501  divalglemnn  12542  bitsp1  12575  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitscmp  12582  bitsinv1lem  12585  bitsinv1  12586  dvdsgcdidd  12628  bezoutlemnewy  12630  mulgcd  12650  rplpwr  12661  sqgcd  12663  lcmgcdlem  12712  3lcm2e6woprm  12721  cncongr1  12738  cncongr2  12739  prmind2  12755  isprm5  12777  divgcdodd  12778  prmdvdsexpr  12785  sqrt2irrlem  12796  oddpwdclemxy  12804  oddpwdclemodd  12807  oddpwdclemdc  12808  oddpwdc  12809  sqpweven  12810  2sqpwodd  12811  sqrt2irraplemnn  12814  sqrt2irrap  12815  qmuldeneqnum  12830  divnumden  12831  qnumgt0  12833  numdensq  12837  hashdvds  12856  phiprmpw  12857  prmdiv  12870  prmdivdiv  12872  phisum  12876  modprm0  12890  pythagtriplem4  12904  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem19  12918  pythagtrip  12919  pcprendvds2  12927  pcpre1  12928  pcpremul  12929  pceulem  12930  pcdiv  12938  pcqmul  12939  pcelnn  12957  pcid  12960  pc2dvds  12966  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  pcaddlem  12975  pcadd  12976  pcfaclem  12985  qexpz  12988  expnprm  12989  oddprmdvds  12990  prmpwdvds  12991  pockthlem  12992  pockthg  12993  infpnlem1  12995  4sqlem6  13019  4sqlem7  13020  4sqlem10  13023  mul4sqlem  13029  4sqlem11  13037  4sqlem12  13038  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  oddennn  13076  evenennn  13077  mulgnndir  13801  mulgnnass  13807  znrrg  14739  logbgcd1irraplemap  15763  pellexlem2  15775  wilthlem1  15777  0sgm  15782  mpodvdsmulf1o  15787  1sgmprm  15791  1sgm2ppw  15792  mersenne  15794  perfect1  15795  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsval2lem  15812  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2  15885  m1lgs  15887  2sqlem3  15919  2sqlem4  15920  trilpolemeq1  16755  trilpolemlt1  16756  redcwlpolemeq1  16770  nconstwlpolemgt0  16780