Theorem nncnd 9032

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 9023	. 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 7905   NNcn 9018

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 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004

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 9019

This theorem is referenced by:  peano5uzti  9463  qapne  9742  qtri3or  10364  exbtwnzlemstep  10371  intfracq  10446  flqdiv  10447  modqmulnn  10468  addmodid  10498  modaddmodup  10513  modsumfzodifsn  10522  addmodlteq  10524  facdiv  10864  facndiv  10865  faclbnd  10867  faclbnd6  10870  facubnd  10871  facavg  10872  bccmpl  10880  bcn0  10881  bcn1  10884  bcm1k  10886  bcp1n  10887  bcp1nk  10888  bcval5  10889  bcpasc  10892  permnn  10897  cvg1nlemcxze  11212  cvg1nlemcau  11214  resqrexlemcalc3  11246  binom11  11716  binom1dif  11717  divcnv  11727  arisum2  11729  trireciplem  11730  trirecip  11731  expcnvap0  11732  geo2sum  11744  geo2lim  11746  cvgratnnlembern  11753  cvgratnnlemnexp  11754  cvgratnnlemmn  11755  cvgratnnlemsumlt  11758  cvgratnnlemfm  11759  cvgratnnlemrate  11760  cvgratz  11762  eftcl  11884  eftabs  11886  efcllemp  11888  ege2le3  11901  efcj  11903  efaddlem  11904  eftlub  11920  eirraplem  12007  oexpneg  12107  divalglemnn  12148  bitsp1  12181  bitsfzolem  12184  bitsfzo  12185  bitsmod  12186  bitscmp  12188  bitsinv1lem  12191  bitsinv1  12192  dvdsgcdidd  12234  bezoutlemnewy  12236  mulgcd  12256  rplpwr  12267  sqgcd  12269  lcmgcdlem  12318  3lcm2e6woprm  12327  cncongr1  12344  cncongr2  12345  prmind2  12361  isprm5  12383  divgcdodd  12384  prmdvdsexpr  12391  sqrt2irrlem  12402  oddpwdclemxy  12410  oddpwdclemodd  12413  oddpwdclemdc  12414  oddpwdc  12415  sqpweven  12416  2sqpwodd  12417  sqrt2irraplemnn  12420  sqrt2irrap  12421  qmuldeneqnum  12436  divnumden  12437  qnumgt0  12439  numdensq  12443  hashdvds  12462  phiprmpw  12463  prmdiv  12476  prmdivdiv  12478  phisum  12482  modprm0  12496  pythagtriplem4  12510  pythagtriplem6  12512  pythagtriplem7  12513  pythagtriplem14  12519  pythagtriplem15  12520  pythagtriplem16  12521  pythagtriplem19  12524  pythagtrip  12525  pcprendvds2  12533  pcpre1  12534  pcpremul  12535  pceulem  12536  pcdiv  12544  pcqmul  12545  pcelnn  12563  pcid  12566  pc2dvds  12572  dvdsprmpweqnn  12578  dvdsprmpweqle  12579  pcaddlem  12581  pcadd  12582  pcfaclem  12591  qexpz  12594  expnprm  12595  oddprmdvds  12596  prmpwdvds  12597  pockthlem  12598  pockthg  12599  infpnlem1  12601  4sqlem6  12625  4sqlem7  12626  4sqlem10  12629  mul4sqlem  12635  4sqlem11  12643  4sqlem12  12644  4sqlem14  12646  4sqlem17  12649  4sqlem18  12650  oddennn  12682  evenennn  12683  mulgnndir  13405  mulgnnass  13411  znrrg  14340  logbgcd1irraplemap  15359  wilthlem1  15370  0sgm  15375  mpodvdsmulf1o  15380  1sgmprm  15384  1sgm2ppw  15385  mersenne  15387  perfect1  15388  perfectlem1  15389  perfectlem2  15390  perfect  15391  lgsval2lem  15405  gausslemma2dlem6  15462  gausslemma2dlem7  15463  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem4  15468  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad2  15478  m1lgs  15480  2sqlem3  15512  2sqlem4  15513  trilpolemeq1  15843  trilpolemlt1  15844  redcwlpolemeq1  15857  nconstwlpolemgt0  15867