Theorem nncnd 9156

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 9147	. 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 8029   NNcn 9142

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

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 9143

This theorem is referenced by:  peano5uzti  9587  qapne  9872  qtri3or  10499  exbtwnzlemstep  10506  intfracq  10581  flqdiv  10582  modqmulnn  10603  addmodid  10633  modaddmodup  10648  modsumfzodifsn  10657  addmodlteq  10659  facdiv  10999  facndiv  11000  faclbnd  11002  faclbnd6  11005  facubnd  11006  facavg  11007  bccmpl  11015  bcn0  11016  bcn1  11019  bcm1k  11021  bcp1n  11022  bcp1nk  11023  bcval5  11024  bcpasc  11027  permnn  11032  cvg1nlemcxze  11542  cvg1nlemcau  11544  resqrexlemcalc3  11576  binom11  12046  binom1dif  12047  divcnv  12057  arisum2  12059  trireciplem  12060  trirecip  12061  expcnvap0  12062  geo2sum  12074  geo2lim  12076  cvgratnnlembern  12083  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratz  12092  eftcl  12214  eftabs  12216  efcllemp  12218  ege2le3  12231  efcj  12233  efaddlem  12234  eftlub  12250  eirraplem  12337  oexpneg  12437  divalglemnn  12478  bitsp1  12511  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitscmp  12518  bitsinv1lem  12521  bitsinv1  12522  dvdsgcdidd  12564  bezoutlemnewy  12566  mulgcd  12586  rplpwr  12597  sqgcd  12599  lcmgcdlem  12648  3lcm2e6woprm  12657  cncongr1  12674  cncongr2  12675  prmind2  12691  isprm5  12713  divgcdodd  12714  prmdvdsexpr  12721  sqrt2irrlem  12732  oddpwdclemxy  12740  oddpwdclemodd  12743  oddpwdclemdc  12744  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  sqrt2irraplemnn  12750  sqrt2irrap  12751  qmuldeneqnum  12766  divnumden  12767  qnumgt0  12769  numdensq  12773  hashdvds  12792  phiprmpw  12793  prmdiv  12806  prmdivdiv  12808  phisum  12812  modprm0  12826  pythagtriplem4  12840  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem19  12854  pythagtrip  12855  pcprendvds2  12863  pcpre1  12864  pcpremul  12865  pceulem  12866  pcdiv  12874  pcqmul  12875  pcelnn  12893  pcid  12896  pc2dvds  12902  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  pcaddlem  12911  pcadd  12912  pcfaclem  12921  qexpz  12924  expnprm  12925  oddprmdvds  12926  prmpwdvds  12927  pockthlem  12928  pockthg  12929  infpnlem1  12931  4sqlem6  12955  4sqlem7  12956  4sqlem10  12959  mul4sqlem  12965  4sqlem11  12973  4sqlem12  12974  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  oddennn  13012  evenennn  13013  mulgnndir  13737  mulgnnass  13743  znrrg  14673  logbgcd1irraplemap  15692  wilthlem1  15703  0sgm  15708  mpodvdsmulf1o  15713  1sgmprm  15717  1sgm2ppw  15718  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsval2lem  15738  gausslemma2dlem6  15795  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2  15811  m1lgs  15813  2sqlem3  15845  2sqlem4  15846  trilpolemeq1  16644  trilpolemlt1  16645  redcwlpolemeq1  16658  nconstwlpolemgt0  16668