Theorem nncnd 9070

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

Syntax hints:   -> wi 4   e. wcel 2177   CCcc 7943   NNcn 9056

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4170  ax-cnex 8036  ax-resscn 8037  ax-1re 8039  ax-addrcl 8042

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-in 3176  df-ss 3183  df-int 3892  df-inn 9057

This theorem is referenced by:  peano5uzti  9501  qapne  9780  qtri3or  10405  exbtwnzlemstep  10412  intfracq  10487  flqdiv  10488  modqmulnn  10509  addmodid  10539  modaddmodup  10554  modsumfzodifsn  10563  addmodlteq  10565  facdiv  10905  facndiv  10906  faclbnd  10908  faclbnd6  10911  facubnd  10912  facavg  10913  bccmpl  10921  bcn0  10922  bcn1  10925  bcm1k  10927  bcp1n  10928  bcp1nk  10929  bcval5  10930  bcpasc  10933  permnn  10938  cvg1nlemcxze  11368  cvg1nlemcau  11370  resqrexlemcalc3  11402  binom11  11872  binom1dif  11873  divcnv  11883  arisum2  11885  trireciplem  11886  trirecip  11887  expcnvap0  11888  geo2sum  11900  geo2lim  11902  cvgratnnlembern  11909  cvgratnnlemnexp  11910  cvgratnnlemmn  11911  cvgratnnlemsumlt  11914  cvgratnnlemfm  11915  cvgratnnlemrate  11916  cvgratz  11918  eftcl  12040  eftabs  12042  efcllemp  12044  ege2le3  12057  efcj  12059  efaddlem  12060  eftlub  12076  eirraplem  12163  oexpneg  12263  divalglemnn  12304  bitsp1  12337  bitsfzolem  12340  bitsfzo  12341  bitsmod  12342  bitscmp  12344  bitsinv1lem  12347  bitsinv1  12348  dvdsgcdidd  12390  bezoutlemnewy  12392  mulgcd  12412  rplpwr  12423  sqgcd  12425  lcmgcdlem  12474  3lcm2e6woprm  12483  cncongr1  12500  cncongr2  12501  prmind2  12517  isprm5  12539  divgcdodd  12540  prmdvdsexpr  12547  sqrt2irrlem  12558  oddpwdclemxy  12566  oddpwdclemodd  12569  oddpwdclemdc  12570  oddpwdc  12571  sqpweven  12572  2sqpwodd  12573  sqrt2irraplemnn  12576  sqrt2irrap  12577  qmuldeneqnum  12592  divnumden  12593  qnumgt0  12595  numdensq  12599  hashdvds  12618  phiprmpw  12619  prmdiv  12632  prmdivdiv  12634  phisum  12638  modprm0  12652  pythagtriplem4  12666  pythagtriplem6  12668  pythagtriplem7  12669  pythagtriplem14  12675  pythagtriplem15  12676  pythagtriplem16  12677  pythagtriplem19  12680  pythagtrip  12681  pcprendvds2  12689  pcpre1  12690  pcpremul  12691  pceulem  12692  pcdiv  12700  pcqmul  12701  pcelnn  12719  pcid  12722  pc2dvds  12728  dvdsprmpweqnn  12734  dvdsprmpweqle  12735  pcaddlem  12737  pcadd  12738  pcfaclem  12747  qexpz  12750  expnprm  12751  oddprmdvds  12752  prmpwdvds  12753  pockthlem  12754  pockthg  12755  infpnlem1  12757  4sqlem6  12781  4sqlem7  12782  4sqlem10  12785  mul4sqlem  12791  4sqlem11  12799  4sqlem12  12800  4sqlem14  12802  4sqlem17  12805  4sqlem18  12806  oddennn  12838  evenennn  12839  mulgnndir  13562  mulgnnass  13568  znrrg  14497  logbgcd1irraplemap  15516  wilthlem1  15527  0sgm  15532  mpodvdsmulf1o  15537  1sgmprm  15541  1sgm2ppw  15542  mersenne  15544  perfect1  15545  perfectlem1  15546  perfectlem2  15547  perfect  15548  lgsval2lem  15562  gausslemma2dlem6  15619  gausslemma2dlem7  15620  gausslemma2d  15621  lgseisenlem1  15622  lgseisenlem4  15625  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2  15635  m1lgs  15637  2sqlem3  15669  2sqlem4  15670  trilpolemeq1  16120  trilpolemlt1  16121  redcwlpolemeq1  16134  nconstwlpolemgt0  16144