Theorem nncnd 9320

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 9311	. 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 9306

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 9307

This theorem is used by:  peano5uzti  9758  qapne  10048  ltesubnnd  10180  qtri3or  10685  exbtwnzlemstep  10692  intfracq  10770  flqdiv  10771  modqmulnn  10792  addmodid  10822  modaddmodup  10837  modsumfzodifsn  10846  addmodlteq  10848  facdiv  11190  facndiv  11191  faclbnd  11193  faclbnd6  11196  facubnd  11197  facavg  11198  bccmpl  11206  bcn0  11207  bcn1  11210  bcm1k  11212  bcp1n  11213  bcp1nk  11214  bcval5  11215  bcpasc  11218  permnn  11224  hashf1  11301  hashfac  11302  cvg1nlemcxze  11762  cvg1nlemcau  11764  resqrexlemcalc3  11796  binom11  12269  binom1dif  12270  divcnv  12280  arisum2  12282  trireciplem  12283  trirecip  12284  expcnvap0  12285  geo2sum  12297  geo2lim  12299  cvgratnnlembern  12306  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratz  12315  eftcl  12437  eftabs  12439  efcllemp  12441  ege2le3  12454  efcj  12456  efaddlem  12457  eftlub  12473  eirraplem  12560  oexpneg  12660  divalglemnn  12701  bitsp1  12734  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  bitsinv1  12745  dvdsgcdidd  12787  bezoutlemnewy  12789  mulgcd  12809  rplpwr  12820  sqgcd  12822  lcmgcdlem  12871  3lcm2e6woprm  12880  cncongr1  12897  cncongr2  12898  prmind2  12914  isprm5  12937  divgcdodd  12938  prmdvdsexpr  12945  sqrt2irrlem  12956  pwbdvdslemn  12960  pwbdvdseulemle  12962  nnmaxpwlemxy  12964  nnmaxpwlemnfac  12967  nnmaxpwlemparts  12968  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  sqrt2irraplemnn  12975  sqrt2irrap  12976  qmuldeneqnum  12991  divnumden  12992  qnumgt0  12994  numdensq  12998  hashdvds  13019  phiprmpw  13020  prmdiv  13033  prmdivdiv  13035  phisum  13039  modprm0  13053  pythagtriplem4  13067  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem19  13081  pythagtrip  13082  pcprendvds2  13090  pcpre1  13091  pcpremul  13092  pceulem  13093  pcdiv  13101  pcqmul  13102  pcelnn  13120  pcid  13123  pc2dvds  13129  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  pcaddlem  13138  pcadd  13139  pcfaclem  13148  qexpz  13151  expnprm  13152  oddprmdvds  13153  prmpwdvds  13154  pockthlem  13155  pockthg  13156  infpnlem1  13158  4sqlem6  13182  4sqlem7  13183  4sqlem10  13186  mul4sqlem  13192  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  ballotfilemfc0  13281  ballotfilemfcc  13282  oddennn  13332  evenennn  13333  mulgnndir  14003  mulgnnass  14009  znrrg  15044  logbgcd1irraplemap  16124  log2tlbndlog2  16139  birthdaylem2  16145  birthdaylem3  16146  pellexlem2  16149  wilthlem1  16151  0sgm  16166  mpodvdsmulf1o  16185  1sgmprm  16189  1sgm2ppw  16190  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcmono  16202  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem5  16213  lgsval2lem  16227  gausslemma2dlem6  16284  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2  16300  m1lgs  16302  2sqlem3  16334  2sqlem4  16335  trilpolemeq1  17187  trilpolemlt1  17188  redcwlpolemeq1  17202  nconstwlpolemgt0  17212