Theorem nncnd 9268

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   NNcn 9254

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9255

This theorem is referenced by:  peano5uzti  9704  qapne  9989  ltesubnnd  10120  qtri3or  10624  exbtwnzlemstep  10631  intfracq  10706  flqdiv  10707  modqmulnn  10728  addmodid  10758  modaddmodup  10773  modsumfzodifsn  10782  addmodlteq  10784  facdiv  11125  facndiv  11126  faclbnd  11128  faclbnd6  11131  facubnd  11132  facavg  11133  bccmpl  11141  bcn0  11142  bcn1  11145  bcm1k  11147  bcp1n  11148  bcp1nk  11149  bcval5  11150  bcpasc  11153  permnn  11159  cvg1nlemcxze  11692  cvg1nlemcau  11694  resqrexlemcalc3  11726  binom11  12197  binom1dif  12198  divcnv  12208  arisum2  12210  trireciplem  12211  trirecip  12212  expcnvap0  12213  geo2sum  12225  geo2lim  12227  cvgratnnlembern  12234  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratz  12243  eftcl  12365  eftabs  12367  efcllemp  12369  ege2le3  12382  efcj  12384  efaddlem  12385  eftlub  12401  eirraplem  12488  oexpneg  12588  divalglemnn  12629  bitsp1  12662  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  bitsinv1  12673  dvdsgcdidd  12715  bezoutlemnewy  12717  mulgcd  12737  rplpwr  12748  sqgcd  12750  lcmgcdlem  12799  3lcm2e6woprm  12808  cncongr1  12825  cncongr2  12826  prmind2  12842  isprm5  12864  divgcdodd  12865  prmdvdsexpr  12872  sqrt2irrlem  12883  oddpwdclemxy  12891  oddpwdclemodd  12894  oddpwdclemdc  12895  oddpwdc  12896  sqpweven  12897  2sqpwodd  12898  sqrt2irraplemnn  12901  sqrt2irrap  12902  qmuldeneqnum  12917  divnumden  12918  qnumgt0  12920  numdensq  12924  hashdvds  12943  phiprmpw  12944  prmdiv  12957  prmdivdiv  12959  phisum  12963  modprm0  12977  pythagtriplem4  12991  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem19  13005  pythagtrip  13006  pcprendvds2  13014  pcpre1  13015  pcpremul  13016  pceulem  13017  pcdiv  13025  pcqmul  13026  pcelnn  13044  pcid  13047  pc2dvds  13053  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  pcaddlem  13062  pcadd  13063  pcfaclem  13072  qexpz  13075  expnprm  13076  oddprmdvds  13077  prmpwdvds  13078  pockthlem  13079  pockthg  13080  infpnlem1  13082  4sqlem6  13106  4sqlem7  13107  4sqlem10  13110  mul4sqlem  13116  4sqlem11  13124  4sqlem12  13125  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  ballotfilemfc0  13176  ballotfilemfcc  13177  oddennn  13227  evenennn  13228  mulgnndir  13904  mulgnnass  13910  znrrg  14934  logbgcd1irraplemap  15960  pellexlem2  15972  wilthlem1  15974  0sgm  15979  mpodvdsmulf1o  15984  1sgmprm  15988  1sgm2ppw  15989  mersenne  15991  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsval2lem  16009  gausslemma2dlem6  16066  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2  16082  m1lgs  16084  2sqlem3  16116  2sqlem4  16117  trilpolemeq1  16950  trilpolemlt1  16951  redcwlpolemeq1  16965  nconstwlpolemgt0  16976