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  9764  qapne  10054  ltesubnnd  10186  qtri3or  10691  exbtwnzlemstep  10698  intfracq  10777  flqdiv  10778  modqmulnn  10799  addmodid  10829  modaddmodup  10844  modsumfzodifsn  10853  addmodlteq  10855  facdiv  11197  facndiv  11198  faclbnd  11200  faclbnd6  11203  facubnd  11204  facavg  11205  bccmpl  11213  bcn0  11214  bcn1  11217  bcm1k  11219  bcp1n  11220  bcp1nk  11221  bcval5  11222  bcpasc  11225  permnn  11231  hashf1  11308  hashfac  11309  cvg1nlemcxze  11769  cvg1nlemcau  11771  resqrexlemcalc3  11803  binom11  12277  binom1dif  12278  divcnv  12288  arisum2  12290  trireciplem  12291  trirecip  12292  expcnvap0  12293  geo2sum  12305  geo2lim  12307  cvgratnnlembern  12314  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratz  12323  eftcl  12445  eftabs  12447  efcllemp  12449  ege2le3  12462  efcj  12464  efaddlem  12465  eftlub  12481  eirraplem  12568  oexpneg  12668  divalglemnn  12709  bitsp1  12742  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitscmp  12749  bitsinv1lem  12752  bitsinv1  12753  dvdsgcdidd  12795  bezoutlemnewy  12797  mulgcd  12817  rplpwr  12828  sqgcd  12830  lcmgcdlem  12879  3lcm2e6woprm  12888  cncongr1  12905  cncongr2  12906  prmind2  12922  isprm5  12945  divgcdodd  12946  prmdvdsexpr  12953  sqrt2irrlem  12964  pwbdvdslemn  12968  pwbdvdseulemle  12970  nnmaxpwlemxy  12972  nnmaxpwlemnfac  12975  nnmaxpwlemparts  12976  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  sqrt2irraplemnn  12983  sqrt2irrap  12984  qmuldeneqnum  12999  divnumden  13000  qnumgt0  13002  numdensq  13006  hashdvds  13027  phiprmpw  13028  prmdiv  13041  prmdivdiv  13043  phisum  13047  modprm0  13061  pythagtriplem4  13075  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem19  13089  pythagtrip  13090  pcprendvds2  13098  pcpre1  13099  pcpremul  13100  pceulem  13101  pcdiv  13109  pcqmul  13110  pcelnn  13128  pcid  13131  pc2dvds  13137  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  pcaddlem  13146  pcadd  13147  pcfaclem  13156  qexpz  13159  expnprm  13160  oddprmdvds  13161  prmpwdvds  13162  pockthlem  13163  pockthg  13164  infpnlem1  13166  4sqlem6  13190  4sqlem7  13191  4sqlem10  13194  mul4sqlem  13200  4sqlem11  13208  4sqlem12  13209  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  ballotfilemfc0  13289  ballotfilemfcc  13290  oddennn  13340  evenennn  13341  mulgnndir  14012  mulgnnass  14018  znrrg  15103  efnthr  16193  logbgcd1irraplemap  16222  log2tlbndlog2  16237  birthdaylem2  16243  birthdaylem3  16244  pellexlem2  16247  wilthlem1  16249  0sgm  16271  mpodvdsmulf1o  16301  1sgmprm  16305  1sgm2ppw  16306  chtublem  16312  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcmono  16321  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgsval2lem  16351  gausslemma2dlem6  16408  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2  16424  m1lgs  16426  2sqlem3  16458  2sqlem4  16459  trilpolemeq1  17313  trilpolemlt1  17314  redcwlpolemeq1  17328  nconstwlpolemgt0  17338