Theorem nncnd 9120

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7993   NNcn 9106

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3923  df-inn 9107

This theorem is referenced by:  peano5uzti  9551  qapne  9830  qtri3or  10455  exbtwnzlemstep  10462  intfracq  10537  flqdiv  10538  modqmulnn  10559  addmodid  10589  modaddmodup  10604  modsumfzodifsn  10613  addmodlteq  10615  facdiv  10955  facndiv  10956  faclbnd  10958  faclbnd6  10961  facubnd  10962  facavg  10963  bccmpl  10971  bcn0  10972  bcn1  10975  bcm1k  10977  bcp1n  10978  bcp1nk  10979  bcval5  10980  bcpasc  10983  permnn  10988  cvg1nlemcxze  11488  cvg1nlemcau  11490  resqrexlemcalc3  11522  binom11  11992  binom1dif  11993  divcnv  12003  arisum2  12005  trireciplem  12006  trirecip  12007  expcnvap0  12008  geo2sum  12020  geo2lim  12022  cvgratnnlembern  12029  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratz  12038  eftcl  12160  eftabs  12162  efcllemp  12164  ege2le3  12177  efcj  12179  efaddlem  12180  eftlub  12196  eirraplem  12283  oexpneg  12383  divalglemnn  12424  bitsp1  12457  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitscmp  12464  bitsinv1lem  12467  bitsinv1  12468  dvdsgcdidd  12510  bezoutlemnewy  12512  mulgcd  12532  rplpwr  12543  sqgcd  12545  lcmgcdlem  12594  3lcm2e6woprm  12603  cncongr1  12620  cncongr2  12621  prmind2  12637  isprm5  12659  divgcdodd  12660  prmdvdsexpr  12667  sqrt2irrlem  12678  oddpwdclemxy  12686  oddpwdclemodd  12689  oddpwdclemdc  12690  oddpwdc  12691  sqpweven  12692  2sqpwodd  12693  sqrt2irraplemnn  12696  sqrt2irrap  12697  qmuldeneqnum  12712  divnumden  12713  qnumgt0  12715  numdensq  12719  hashdvds  12738  phiprmpw  12739  prmdiv  12752  prmdivdiv  12754  phisum  12758  modprm0  12772  pythagtriplem4  12786  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem19  12800  pythagtrip  12801  pcprendvds2  12809  pcpre1  12810  pcpremul  12811  pceulem  12812  pcdiv  12820  pcqmul  12821  pcelnn  12839  pcid  12842  pc2dvds  12848  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  pcaddlem  12857  pcadd  12858  pcfaclem  12867  qexpz  12870  expnprm  12871  oddprmdvds  12872  prmpwdvds  12873  pockthlem  12874  pockthg  12875  infpnlem1  12877  4sqlem6  12901  4sqlem7  12902  4sqlem10  12905  mul4sqlem  12911  4sqlem11  12919  4sqlem12  12920  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  oddennn  12958  evenennn  12959  mulgnndir  13683  mulgnnass  13689  znrrg  14618  logbgcd1irraplemap  15637  wilthlem1  15648  0sgm  15653  mpodvdsmulf1o  15658  1sgmprm  15662  1sgm2ppw  15663  mersenne  15665  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsval2lem  15683  gausslemma2dlem6  15740  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2  15756  m1lgs  15758  2sqlem3  15790  2sqlem4  15791  trilpolemeq1  16367  trilpolemlt1  16368  redcwlpolemeq1  16381  nconstwlpolemgt0  16391