Theorem nncnd 9318

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   NNcn 9304

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9305

This theorem is used by:  peano5uzti  9754  qapne  10039  ltesubnnd  10170  qtri3or  10675  exbtwnzlemstep  10682  intfracq  10757  flqdiv  10758  modqmulnn  10779  addmodid  10809  modaddmodup  10824  modsumfzodifsn  10833  addmodlteq  10835  facdiv  11176  facndiv  11177  faclbnd  11179  faclbnd6  11182  facubnd  11183  facavg  11184  bccmpl  11192  bcn0  11193  bcn1  11196  bcm1k  11198  bcp1n  11199  bcp1nk  11200  bcval5  11201  bcpasc  11204  permnn  11210  hashf1  11287  hashfac  11288  cvg1nlemcxze  11748  cvg1nlemcau  11750  resqrexlemcalc3  11782  binom11  12253  binom1dif  12254  divcnv  12264  arisum2  12266  trireciplem  12267  trirecip  12268  expcnvap0  12269  geo2sum  12281  geo2lim  12283  cvgratnnlembern  12290  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratz  12299  eftcl  12421  eftabs  12423  efcllemp  12425  ege2le3  12438  efcj  12440  efaddlem  12441  eftlub  12457  eirraplem  12544  oexpneg  12644  divalglemnn  12685  bitsp1  12718  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitscmp  12725  bitsinv1lem  12728  bitsinv1  12729  dvdsgcdidd  12771  bezoutlemnewy  12773  mulgcd  12793  rplpwr  12804  sqgcd  12806  lcmgcdlem  12855  3lcm2e6woprm  12864  cncongr1  12881  cncongr2  12882  prmind2  12898  isprm5  12920  divgcdodd  12921  prmdvdsexpr  12928  sqrt2irrlem  12939  oddpwdclemxy  12947  oddpwdclemodd  12950  oddpwdclemdc  12951  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  sqrt2irraplemnn  12957  sqrt2irrap  12958  qmuldeneqnum  12973  divnumden  12974  qnumgt0  12976  numdensq  12980  hashdvds  12999  phiprmpw  13000  prmdiv  13013  prmdivdiv  13015  phisum  13019  modprm0  13033  pythagtriplem4  13047  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem19  13061  pythagtrip  13062  pcprendvds2  13070  pcpre1  13071  pcpremul  13072  pceulem  13073  pcdiv  13081  pcqmul  13082  pcelnn  13100  pcid  13103  pc2dvds  13109  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  pcaddlem  13118  pcadd  13119  pcfaclem  13128  qexpz  13131  expnprm  13132  oddprmdvds  13133  prmpwdvds  13134  pockthlem  13135  pockthg  13136  infpnlem1  13138  4sqlem6  13162  4sqlem7  13163  4sqlem10  13166  mul4sqlem  13172  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  ballotfilemfc0  13232  ballotfilemfcc  13233  oddennn  13283  evenennn  13284  mulgnndir  13954  mulgnnass  13960  znrrg  14995  logbgcd1irraplemap  16071  log2tlbndlog2  16082  birthdaylem2  16088  birthdaylem3  16089  pellexlem2  16092  wilthlem1  16094  0sgm  16099  mpodvdsmulf1o  16104  1sgmprm  16108  1sgm2ppw  16109  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsval2lem  16129  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2  16202  m1lgs  16204  2sqlem3  16236  2sqlem4  16237  trilpolemeq1  17089  trilpolemlt1  17090  redcwlpolemeq1  17104  nconstwlpolemgt0  17114