Theorem nncnd 9321

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 9312	. 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 8178   NNcn 9307

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

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 9308

This theorem is used by:  peano5uzti  9759  qapne  10049  ltesubnnd  10181  qtri3or  10686  exbtwnzlemstep  10693  intfracq  10772  flqdiv  10773  modqmulnn  10794  addmodid  10824  modaddmodup  10839  modsumfzodifsn  10848  addmodlteq  10850  facdiv  11192  facndiv  11193  faclbnd  11195  faclbnd6  11198  facubnd  11199  facavg  11200  bccmpl  11208  bcn0  11209  bcn1  11212  bcm1k  11214  bcp1n  11215  bcp1nk  11216  bcval5  11217  bcpasc  11220  permnn  11226  hashf1  11303  hashfac  11304  cvg1nlemcxze  11764  cvg1nlemcau  11766  resqrexlemcalc3  11798  binom11  12272  binom1dif  12273  divcnv  12283  arisum2  12285  trireciplem  12286  trirecip  12287  expcnvap0  12288  geo2sum  12300  geo2lim  12302  cvgratnnlembern  12309  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratz  12318  eftcl  12440  eftabs  12442  efcllemp  12444  ege2le3  12457  efcj  12459  efaddlem  12460  eftlub  12476  eirraplem  12563  oexpneg  12663  divalglemnn  12704  bitsp1  12737  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  bitsinv1  12748  dvdsgcdidd  12790  bezoutlemnewy  12792  mulgcd  12812  rplpwr  12823  sqgcd  12825  lcmgcdlem  12874  3lcm2e6woprm  12883  cncongr1  12900  cncongr2  12901  prmind2  12917  isprm5  12940  divgcdodd  12941  prmdvdsexpr  12948  sqrt2irrlem  12959  pwbdvdslemn  12963  pwbdvdseulemle  12965  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  nnmaxpwlemparts  12971  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  sqrt2irraplemnn  12978  sqrt2irrap  12979  qmuldeneqnum  12994  divnumden  12995  qnumgt0  12997  numdensq  13001  hashdvds  13022  phiprmpw  13023  prmdiv  13036  prmdivdiv  13038  phisum  13042  modprm0  13056  pythagtriplem4  13070  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem19  13084  pythagtrip  13085  pcprendvds2  13093  pcpre1  13094  pcpremul  13095  pceulem  13096  pcdiv  13104  pcqmul  13105  pcelnn  13123  pcid  13126  pc2dvds  13132  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  pcaddlem  13141  pcadd  13142  pcfaclem  13151  qexpz  13154  expnprm  13155  oddprmdvds  13156  prmpwdvds  13157  pockthlem  13158  pockthg  13159  infpnlem1  13161  4sqlem6  13185  4sqlem7  13186  4sqlem10  13189  mul4sqlem  13195  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  ballotfilemfc0  13284  ballotfilemfcc  13285  oddennn  13335  evenennn  13336  mulgnndir  14007  mulgnnass  14013  znrrg  15086  efnthr  16150  logbgcd1irraplemap  16179  log2tlbndlog2  16194  birthdaylem2  16200  birthdaylem3  16201  pellexlem2  16204  wilthlem1  16206  0sgm  16228  mpodvdsmulf1o  16258  1sgmprm  16262  1sgm2ppw  16263  chtublem  16269  mersenne  16271  perfect1  16272  perfectlem1  16273  perfectlem2  16274  perfect  16275  bcmono  16278  bcp1ctr  16280  bclbnd  16281  bposlem1  16285  bposlem2  16286  bposlem3  16287  bposlem5  16289  bposlem6  16290  lgsval2lem  16308  gausslemma2dlem6  16365  gausslemma2dlem7  16366  gausslemma2d  16367  lgseisenlem1  16368  lgseisenlem4  16371  lgsquadlem1  16375  lgsquadlem2  16376  lgsquadlem3  16377  lgsquad2  16381  m1lgs  16383  2sqlem3  16415  2sqlem4  16416  trilpolemeq1  17269  trilpolemlt1  17270  redcwlpolemeq1  17284  nconstwlpolemgt0  17294