Theorem nncnd 9049

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

Syntax hints:   -> wi 4   e. wcel 2175   CCcc 7922   NNcn 9035

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 8015  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-in 3171  df-ss 3178  df-int 3885  df-inn 9036

This theorem is referenced by:  peano5uzti  9480  qapne  9759  qtri3or  10381  exbtwnzlemstep  10388  intfracq  10463  flqdiv  10464  modqmulnn  10485  addmodid  10515  modaddmodup  10530  modsumfzodifsn  10539  addmodlteq  10541  facdiv  10881  facndiv  10882  faclbnd  10884  faclbnd6  10887  facubnd  10888  facavg  10889  bccmpl  10897  bcn0  10898  bcn1  10901  bcm1k  10903  bcp1n  10904  bcp1nk  10905  bcval5  10906  bcpasc  10909  permnn  10914  cvg1nlemcxze  11235  cvg1nlemcau  11237  resqrexlemcalc3  11269  binom11  11739  binom1dif  11740  divcnv  11750  arisum2  11752  trireciplem  11753  trirecip  11754  expcnvap0  11755  geo2sum  11767  geo2lim  11769  cvgratnnlembern  11776  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  cvgratnnlemsumlt  11781  cvgratnnlemfm  11782  cvgratnnlemrate  11783  cvgratz  11785  eftcl  11907  eftabs  11909  efcllemp  11911  ege2le3  11924  efcj  11926  efaddlem  11927  eftlub  11943  eirraplem  12030  oexpneg  12130  divalglemnn  12171  bitsp1  12204  bitsfzolem  12207  bitsfzo  12208  bitsmod  12209  bitscmp  12211  bitsinv1lem  12214  bitsinv1  12215  dvdsgcdidd  12257  bezoutlemnewy  12259  mulgcd  12279  rplpwr  12290  sqgcd  12292  lcmgcdlem  12341  3lcm2e6woprm  12350  cncongr1  12367  cncongr2  12368  prmind2  12384  isprm5  12406  divgcdodd  12407  prmdvdsexpr  12414  sqrt2irrlem  12425  oddpwdclemxy  12433  oddpwdclemodd  12436  oddpwdclemdc  12437  oddpwdc  12438  sqpweven  12439  2sqpwodd  12440  sqrt2irraplemnn  12443  sqrt2irrap  12444  qmuldeneqnum  12459  divnumden  12460  qnumgt0  12462  numdensq  12466  hashdvds  12485  phiprmpw  12486  prmdiv  12499  prmdivdiv  12501  phisum  12505  modprm0  12519  pythagtriplem4  12533  pythagtriplem6  12535  pythagtriplem7  12536  pythagtriplem14  12542  pythagtriplem15  12543  pythagtriplem16  12544  pythagtriplem19  12547  pythagtrip  12548  pcprendvds2  12556  pcpre1  12557  pcpremul  12558  pceulem  12559  pcdiv  12567  pcqmul  12568  pcelnn  12586  pcid  12589  pc2dvds  12595  dvdsprmpweqnn  12601  dvdsprmpweqle  12602  pcaddlem  12604  pcadd  12605  pcfaclem  12614  qexpz  12617  expnprm  12618  oddprmdvds  12619  prmpwdvds  12620  pockthlem  12621  pockthg  12622  infpnlem1  12624  4sqlem6  12648  4sqlem7  12649  4sqlem10  12652  mul4sqlem  12658  4sqlem11  12666  4sqlem12  12667  4sqlem14  12669  4sqlem17  12672  4sqlem18  12673  oddennn  12705  evenennn  12706  mulgnndir  13429  mulgnnass  13435  znrrg  14364  logbgcd1irraplemap  15383  wilthlem1  15394  0sgm  15399  mpodvdsmulf1o  15404  1sgmprm  15408  1sgm2ppw  15409  mersenne  15411  perfect1  15412  perfectlem1  15413  perfectlem2  15414  perfect  15415  lgsval2lem  15429  gausslemma2dlem6  15486  gausslemma2dlem7  15487  gausslemma2d  15488  lgseisenlem1  15489  lgseisenlem4  15492  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  lgsquad2  15502  m1lgs  15504  2sqlem3  15536  2sqlem4  15537  trilpolemeq1  15912  trilpolemlt1  15913  redcwlpolemeq1  15926  nconstwlpolemgt0  15936