Theorem nncnd 9147

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8020   NNcn 9133

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 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

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 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9134

This theorem is referenced by:  peano5uzti  9578  qapne  9863  qtri3or  10490  exbtwnzlemstep  10497  intfracq  10572  flqdiv  10573  modqmulnn  10594  addmodid  10624  modaddmodup  10639  modsumfzodifsn  10648  addmodlteq  10650  facdiv  10990  facndiv  10991  faclbnd  10993  faclbnd6  10996  facubnd  10997  facavg  10998  bccmpl  11006  bcn0  11007  bcn1  11010  bcm1k  11012  bcp1n  11013  bcp1nk  11014  bcval5  11015  bcpasc  11018  permnn  11023  cvg1nlemcxze  11533  cvg1nlemcau  11535  resqrexlemcalc3  11567  binom11  12037  binom1dif  12038  divcnv  12048  arisum2  12050  trireciplem  12051  trirecip  12052  expcnvap0  12053  geo2sum  12065  geo2lim  12067  cvgratnnlembern  12074  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratz  12083  eftcl  12205  eftabs  12207  efcllemp  12209  ege2le3  12222  efcj  12224  efaddlem  12225  eftlub  12241  eirraplem  12328  oexpneg  12428  divalglemnn  12469  bitsp1  12502  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitscmp  12509  bitsinv1lem  12512  bitsinv1  12513  dvdsgcdidd  12555  bezoutlemnewy  12557  mulgcd  12577  rplpwr  12588  sqgcd  12590  lcmgcdlem  12639  3lcm2e6woprm  12648  cncongr1  12665  cncongr2  12666  prmind2  12682  isprm5  12704  divgcdodd  12705  prmdvdsexpr  12712  sqrt2irrlem  12723  oddpwdclemxy  12731  oddpwdclemodd  12734  oddpwdclemdc  12735  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  sqrt2irraplemnn  12741  sqrt2irrap  12742  qmuldeneqnum  12757  divnumden  12758  qnumgt0  12760  numdensq  12764  hashdvds  12783  phiprmpw  12784  prmdiv  12797  prmdivdiv  12799  phisum  12803  modprm0  12817  pythagtriplem4  12831  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem19  12845  pythagtrip  12846  pcprendvds2  12854  pcpre1  12855  pcpremul  12856  pceulem  12857  pcdiv  12865  pcqmul  12866  pcelnn  12884  pcid  12887  pc2dvds  12893  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  pcaddlem  12902  pcadd  12903  pcfaclem  12912  qexpz  12915  expnprm  12916  oddprmdvds  12917  prmpwdvds  12918  pockthlem  12919  pockthg  12920  infpnlem1  12922  4sqlem6  12946  4sqlem7  12947  4sqlem10  12950  mul4sqlem  12956  4sqlem11  12964  4sqlem12  12965  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  oddennn  13003  evenennn  13004  mulgnndir  13728  mulgnnass  13734  znrrg  14664  logbgcd1irraplemap  15683  wilthlem1  15694  0sgm  15699  mpodvdsmulf1o  15704  1sgmprm  15708  1sgm2ppw  15709  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsval2lem  15729  gausslemma2dlem6  15786  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2  15802  m1lgs  15804  2sqlem3  15836  2sqlem4  15837  trilpolemeq1  16580  trilpolemlt1  16581  redcwlpolemeq1  16594  nconstwlpolemgt0  16604