Theorem nncnd 8968

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

Syntax hints:   -> wi 4   e. wcel 2160   CCcc 7844   NNcn 8954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4139  ax-cnex 7937  ax-resscn 7938  ax-1re 7940  ax-addrcl 7943

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-in 3150  df-ss 3157  df-int 3863  df-inn 8955

This theorem is referenced by:  peano5uzti  9396  qapne  9675  qtri3or  10279  exbtwnzlemstep  10284  intfracq  10357  flqdiv  10358  modqmulnn  10379  addmodid  10409  modaddmodup  10424  modsumfzodifsn  10433  addmodlteq  10435  facdiv  10759  facndiv  10760  faclbnd  10762  faclbnd6  10765  facubnd  10766  facavg  10767  bccmpl  10775  bcn0  10776  bcn1  10779  bcm1k  10781  bcp1n  10782  bcp1nk  10783  bcval5  10784  bcpasc  10787  permnn  10792  cvg1nlemcxze  11032  cvg1nlemcau  11034  resqrexlemcalc3  11066  binom11  11535  binom1dif  11536  divcnv  11546  arisum2  11548  trireciplem  11549  trirecip  11550  expcnvap0  11551  geo2sum  11563  geo2lim  11565  cvgratnnlembern  11572  cvgratnnlemnexp  11573  cvgratnnlemmn  11574  cvgratnnlemsumlt  11577  cvgratnnlemfm  11578  cvgratnnlemrate  11579  cvgratz  11581  eftcl  11703  eftabs  11705  efcllemp  11707  ege2le3  11720  efcj  11722  efaddlem  11723  eftlub  11739  eirraplem  11825  oexpneg  11923  divalglemnn  11964  dvdsgcdidd  12036  bezoutlemnewy  12038  mulgcd  12058  rplpwr  12069  sqgcd  12071  lcmgcdlem  12120  3lcm2e6woprm  12129  cncongr1  12146  cncongr2  12147  prmind2  12163  isprm5  12185  divgcdodd  12186  prmdvdsexpr  12193  sqrt2irrlem  12204  oddpwdclemxy  12212  oddpwdclemodd  12215  oddpwdclemdc  12216  oddpwdc  12217  sqpweven  12218  2sqpwodd  12219  sqrt2irraplemnn  12222  sqrt2irrap  12223  qmuldeneqnum  12238  divnumden  12239  qnumgt0  12241  numdensq  12245  hashdvds  12264  phiprmpw  12265  prmdiv  12278  prmdivdiv  12280  phisum  12283  modprm0  12297  pythagtriplem4  12311  pythagtriplem6  12313  pythagtriplem7  12314  pythagtriplem14  12320  pythagtriplem15  12321  pythagtriplem16  12322  pythagtriplem19  12325  pythagtrip  12326  pcprendvds2  12334  pcpre1  12335  pcpremul  12336  pceulem  12337  pcdiv  12345  pcqmul  12346  pcelnn  12364  pcid  12367  pc2dvds  12373  dvdsprmpweqnn  12379  dvdsprmpweqle  12380  pcaddlem  12382  pcadd  12383  pcfaclem  12392  qexpz  12395  expnprm  12396  oddprmdvds  12397  prmpwdvds  12398  pockthlem  12399  pockthg  12400  infpnlem1  12402  4sqlem6  12426  4sqlem7  12427  4sqlem10  12430  mul4sqlem  12436  4sqlem11  12444  4sqlem12  12445  4sqlem14  12447  4sqlem17  12450  4sqlem18  12451  oddennn  12454  evenennn  12455  mulgnndir  13116  mulgnnass  13122  logbgcd1irraplemap  14872  wilthlem1  14883  lgsval2lem  14897  lgseisenlem1  14936  m1lgs  14938  2sqlem3  14950  2sqlem4  14951  trilpolemeq1  15276  trilpolemlt1  15277  redcwlpolemeq1  15290  nconstwlpolemgt0  15300