Theorem nncnd 9327

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 9318	. 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 8183   NNcn 9313

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

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 9314

This theorem is used by:  peano5uzti  9765  qapne  10055  ltesubnnd  10187  qtri3or  10692  exbtwnzlemstep  10699  intfracq  10778  flqdiv  10779  modqmulnn  10800  addmodid  10830  modaddmodup  10845  modsumfzodifsn  10854  addmodlteq  10856  facdiv  11198  facndiv  11199  faclbnd  11201  faclbnd6  11204  facubnd  11205  facavg  11206  bccmpl  11214  bcn0  11215  bcn1  11218  bcm1k  11220  bcp1n  11221  bcp1nk  11222  bcval5  11223  bcpasc  11226  permnn  11232  hashf1  11309  hashfac  11310  cvg1nlemcxze  11770  cvg1nlemcau  11772  resqrexlemcalc3  11804  binom11  12278  binom1dif  12279  divcnv  12289  arisum2  12291  trireciplem  12292  trirecip  12293  expcnvap0  12294  geo2sum  12306  geo2lim  12308  cvgratnnlembern  12315  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratz  12324  eftcl  12446  eftabs  12448  efcllemp  12450  ege2le3  12463  efcj  12465  efaddlem  12466  eftlub  12482  eirraplem  12569  oexpneg  12669  divalglemnn  12710  bitsp1  12743  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  bitsinv1  12754  dvdsgcdidd  12796  bezoutlemnewy  12798  mulgcd  12818  rplpwr  12829  sqgcd  12831  lcmgcdlem  12880  3lcm2e6woprm  12889  cncongr1  12906  cncongr2  12907  prmind2  12923  isprm5  12946  divgcdodd  12947  prmdvdsexpr  12954  sqrt2irrlem  12965  pwbdvdslemn  12969  pwbdvdseulemle  12971  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  nnmaxpwlemparts  12977  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  sqrt2irraplemnn  12984  sqrt2irrap  12985  qmuldeneqnum  13000  divnumden  13001  qnumgt0  13003  numdensq  13007  hashdvds  13028  phiprmpw  13029  prmdiv  13042  prmdivdiv  13044  phisum  13048  modprm0  13062  pythagtriplem4  13076  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem19  13090  pythagtrip  13091  pcprendvds2  13099  pcpre1  13100  pcpremul  13101  pceulem  13102  pcdiv  13110  pcqmul  13111  pcelnn  13129  pcid  13132  pc2dvds  13138  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  pcaddlem  13147  pcadd  13148  pcfaclem  13157  qexpz  13160  expnprm  13161  oddprmdvds  13162  prmpwdvds  13163  pockthlem  13164  pockthg  13165  infpnlem1  13167  4sqlem6  13191  4sqlem7  13192  4sqlem10  13195  mul4sqlem  13201  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  ballotfilemfc0  13290  ballotfilemfcc  13291  oddennn  13341  evenennn  13342  mulgnndir  14013  mulgnnass  14019  znrrg  15104  efnthr  16176  logbgcd1irraplemap  16205  log2tlbndlog2  16220  birthdaylem2  16226  birthdaylem3  16227  pellexlem2  16230  wilthlem1  16232  0sgm  16254  mpodvdsmulf1o  16284  1sgmprm  16288  1sgm2ppw  16289  chtublem  16295  mersenne  16297  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcmono  16304  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgsval2lem  16334  gausslemma2dlem6  16391  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2  16407  m1lgs  16409  2sqlem3  16441  2sqlem4  16442  trilpolemeq1  17296  trilpolemlt1  17297  redcwlpolemeq1  17311  nconstwlpolemgt0  17321