Theorem nncnd 9004

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7877   NNcn 8990

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4151  ax-cnex 7970  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3875  df-inn 8991

This theorem is referenced by:  peano5uzti  9434  qapne  9713  qtri3or  10330  exbtwnzlemstep  10337  intfracq  10412  flqdiv  10413  modqmulnn  10434  addmodid  10464  modaddmodup  10479  modsumfzodifsn  10488  addmodlteq  10490  facdiv  10830  facndiv  10831  faclbnd  10833  faclbnd6  10836  facubnd  10837  facavg  10838  bccmpl  10846  bcn0  10847  bcn1  10850  bcm1k  10852  bcp1n  10853  bcp1nk  10854  bcval5  10855  bcpasc  10858  permnn  10863  cvg1nlemcxze  11147  cvg1nlemcau  11149  resqrexlemcalc3  11181  binom11  11651  binom1dif  11652  divcnv  11662  arisum2  11664  trireciplem  11665  trirecip  11666  expcnvap0  11667  geo2sum  11679  geo2lim  11681  cvgratnnlembern  11688  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratz  11697  eftcl  11819  eftabs  11821  efcllemp  11823  ege2le3  11836  efcj  11838  efaddlem  11839  eftlub  11855  eirraplem  11942  oexpneg  12042  divalglemnn  12083  bitsp1  12115  bitsfzolem  12118  bitsfzo  12119  dvdsgcdidd  12161  bezoutlemnewy  12163  mulgcd  12183  rplpwr  12194  sqgcd  12196  lcmgcdlem  12245  3lcm2e6woprm  12254  cncongr1  12271  cncongr2  12272  prmind2  12288  isprm5  12310  divgcdodd  12311  prmdvdsexpr  12318  sqrt2irrlem  12329  oddpwdclemxy  12337  oddpwdclemodd  12340  oddpwdclemdc  12341  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  sqrt2irraplemnn  12347  sqrt2irrap  12348  qmuldeneqnum  12363  divnumden  12364  qnumgt0  12366  numdensq  12370  hashdvds  12389  phiprmpw  12390  prmdiv  12403  prmdivdiv  12405  phisum  12409  modprm0  12423  pythagtriplem4  12437  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem19  12451  pythagtrip  12452  pcprendvds2  12460  pcpre1  12461  pcpremul  12462  pceulem  12463  pcdiv  12471  pcqmul  12472  pcelnn  12490  pcid  12493  pc2dvds  12499  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  pcaddlem  12508  pcadd  12509  pcfaclem  12518  qexpz  12521  expnprm  12522  oddprmdvds  12523  prmpwdvds  12524  pockthlem  12525  pockthg  12526  infpnlem1  12528  4sqlem6  12552  4sqlem7  12553  4sqlem10  12556  mul4sqlem  12562  4sqlem11  12570  4sqlem12  12571  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  oddennn  12609  evenennn  12610  mulgnndir  13281  mulgnnass  13287  znrrg  14216  logbgcd1irraplemap  15205  wilthlem1  15216  0sgm  15221  mpodvdsmulf1o  15226  1sgmprm  15230  1sgm2ppw  15231  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsval2lem  15251  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2  15324  m1lgs  15326  2sqlem3  15358  2sqlem4  15359  trilpolemeq1  15684  trilpolemlt1  15685  redcwlpolemeq1  15698  nconstwlpolemgt0  15708