MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nncnd Structured version   Visualization version   Unicode version

Theorem nncnd 10647
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
StepHypRef Expression
1 nnsscn 10636 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3416 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   CCcc 9555   NNcn 10631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-i2m1 9625  ax-1ne0 9626  ax-rrecex 9629  ax-cnre 9630
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-nn 10632
This theorem is referenced by:  facdiv  12510  facndiv  12511  faclbnd  12513  faclbnd5  12521  faclbnd6  12522  facubnd  12523  facavg  12524  bccmpl  12532  bcn0  12533  bcn1  12536  bcm1k  12538  bcp1n  12539  bcp1nk  12540  bcval5  12541  bcpasc  12544  permnn  12549  hashf1  12661  hashfac  12662  relexpaddnn  13191  binom11  13967  binom1dif  13968  climcndslem2  13985  arisum2  13996  trireciplem  13997  trirecip  13998  geo2sum  14006  geo2lim  14008  fprodfac  14104  risefacfac  14165  fallfacfwd  14166  fallfacval4  14173  bcfallfac  14174  fallfacfac  14175  bpolycl  14182  bpolysum  14183  bpolydiflem  14184  fsumkthpow  14186  eftcl  14205  eftabs  14207  efcllem  14209  ege2le3  14221  efcj  14223  efaddlem  14224  eftlub  14240  eirrlem  14333  sqr2irrlem  14377  oexpneg  14446  bitsp1  14483  bitsfzolem  14486  bitsfzolemOLD  14487  bitsfzo  14488  bitsmod  14489  bitscmp  14491  bitsinv1lem  14494  bitsinv1  14495  2ebits  14500  bitsinvp1  14502  sadcaddlem  14510  sadadd3  14514  bitsres  14526  bitsuz  14527  bitsshft  14528  mulgcd  14593  rplpwr  14603  sqgcd  14605  lcmgcdlem  14650  3lcm2e6woprm  14659  prmind2  14714  isprm5  14730  divgcdodd  14732  prmdvdsexpr  14748  coprmprod  14757  coprmproddvdslem  14758  qmuldeneqnum  14775  divnumden  14776  qnumgt0  14778  numdensq  14782  hashdvds  14802  phiprmpw  14803  prmdiv  14812  prmdivdiv  14814  modprm0  14835  pythagtriplem4  14848  pythagtriplem6  14850  pythagtriplem7  14851  pythagtriplem14  14857  pythagtriplem15  14858  pythagtriplem19  14862  pythagtrip  14863  pcprendvds2  14870  pcpre1  14871  pcpremul  14872  pceulem  14874  pcdiv  14881  pcqmul  14882  pcelnn  14898  pcid  14901  pc2dvds  14907  pcaddlem  14912  pcadd  14913  pcfaclem  14922  qexpz  14925  expnprm  14926  prmpwdvds  14927  pockthlem  14928  pockthg  14929  infpnlem1  14933  prmreclem1  14939  prmreclem2  14940  prmreclem3  14941  prmreclem4  14942  prmreclem6  14944  4sqlem6  14966  4sqlem7  14967  4sqlem10  14970  mul4sqlem  14976  4sqlem11  14978  4sqlem12  14979  4sqlem14OLD  14981  4sqlem17OLD  14984  4sqlem18OLD  14985  4sqlem14  14987  4sqlem17  14990  4sqlem18  14991  vdwlem1  15010  vdwlem2  15011  vdwlem3  15012  vdwlem5  15014  vdwlem6  15015  vdwlem8  15017  vdwlem9  15018  vdwlem10  15019  vdwlem12  15021  ramub1lem2  15064  ramcl  15066  prmop1  15075  prmdvdsprmo  15079  prmgaplem7  15106  prmgaplem8  15107  gsumccat  16703  mulgnndir  16858  mulgnnass  16864  psgnunilem5  17213  odf1o2  17300  pgp0  17326  sylow1lem1  17328  odcau  17334  sylow2blem3  17352  sylow3lem3  17359  sylow3lem4  17360  gexexlem  17568  ablfacrp2  17778  ablfac1lem  17779  ablfac1eu  17784  pgpfac1lem3a  17787  pgpfac1lem3  17788  zringlpirlem3OLD  19132  zringlpirlem3  19134  znrrg  19213  cpmadugsumlemF  19977  lebnumlem3  22069  lebnumlem3OLD  22072  ovollb2lem  22519  ovolunlem1a  22527  ovolunlem1  22528  uniioombllem3  22622  uniioombllem4  22623  dyaddisjlem  22632  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  dgrcolem1  23306  vieta1lem1  23342  vieta1lem2  23343  elqaalem2  23352  elqaalem3  23353  elqaalem2OLD  23355  elqaalem3OLD  23356  aalioulem1  23367  aaliou3lem2  23378  aaliou3lem8  23380  aaliou3lem6  23383  aaliou3lem9  23385  taylfvallem1  23391  tayl0  23396  taylply2  23402  taylply  23403  dvtaylp  23404  taylthlem1  23407  taylthlem2  23408  pserdvlem2  23462  advlogexp  23679  cxpmul2  23713  cxpeq  23776  atantayl3  23944  leibpi  23947  log2cnv  23949  log2tlbnd  23950  birthdaylem2  23957  birthdaylem3  23958  amgmlem  23994  amgm  23995  emcllem5  24004  fsumharmonic  24016  zetacvg  24019  dmgmdivn0  24032  lgamgulmlem3  24035  lgamgulmlem4  24036  lgamgulmlem5  24037  lgamgulmlem6  24038  lgamgulm2  24040  lgamcvg2  24059  gamcvg  24060  gamcvg2lem  24063  facgam  24070  wilthlem1  24072  wilthlem2  24073  wilthlem3  24074  basellem1  24086  basellem2  24087  basellem3  24088  basellem4  24089  basellem5  24090  basellem8  24093  vmaprm  24123  sgmval2  24149  0sgm  24150  sgmf  24151  vma1  24172  dvdsdivcl  24189  fsumdvdsdiaglem  24191  dvdsflf1o  24195  muinv  24201  dvdsmulf1o  24202  sgmppw  24204  1sgmprm  24206  1sgm2ppw  24207  sgmmul  24208  chtublem  24218  fsumvma2  24221  chpchtsum  24226  logfaclbnd  24229  logexprlim  24232  mersenne  24234  perfect1  24235  perfectlem1  24236  perfectlem2  24237  perfect  24238  dchrsum2  24275  dchrhash  24278  bcmono  24284  bcp1ctr  24286  bclbnd  24287  bposlem1  24291  bposlem2  24292  bposlem3  24293  bposlem5  24295  bposlem6  24296  lgsval2lem  24313  lgsqrlem2  24349  lgseisenlem1  24356  lgseisenlem4  24359  lgsquadlem1  24361  lgsquadlem2  24362  lgsquadlem3  24363  lgsquad2  24367  m1lgs  24369  2sqlem3  24373  2sqlem4  24374  chebbnd1lem1  24386  chebbnd1  24389  rplogsumlem1  24401  rplogsumlem2  24402  rpvmasumlem  24404  dchrisumlem1  24406  dchrmusum2  24411  dchrvmasumlem1  24412  dchrvmasum2lem  24413  dchrvmasum2if  24414  dchrvmasumlem2  24415  dchrvmasumlem3  24416  dchrvmasumiflem1  24418  dchrisum0flblem1  24425  dchrisum0flblem2  24426  dchrisum0fno1  24428  rpvmasum2  24429  rplogsum  24444  mulogsumlem  24448  mulogsum  24449  mulog2sumlem2  24452  vmalogdivsum2  24455  vmalogdivsum  24456  2vmadivsumlem  24457  logsqvma  24459  selberglem2  24463  selberglem3  24464  selberg  24465  selberg2lem  24467  logdivbnd  24473  selberg3lem1  24474  selberg4lem1  24477  pntrsumo1  24482  pntrsumbnd2  24484  selberg3r  24486  selberg4r  24487  selberg34r  24488  pntsval2  24493  pntrlog2bndlem2  24495  pntrlog2bndlem4  24497  pntrlog2bndlem6  24500  pntpbnd1  24503  pntpbnd2  24504  pntlemg  24515  pntlemn  24517  pntlemf  24522  pnt  24531  padicabvf  24548  ostth2lem2  24551  ostth3  24555  hashclwwlkn  25643  eupares  25782  numdenneg  28455  ltesubnnd  28460  1smat1  28704  madjusmdetlem2  28728  madjusmdetlem4  28730  qqhnm  28868  oddpwdc  29260  eulerpartlemsv2  29264  eulerpartlems  29266  eulerpartlemsv3  29267  eulerpartlemgc  29268  eulerpartlemv  29270  eulerpartlemgs2  29286  fibp1  29307  ballotlemfc0  29398  ballotlemfcc  29399  signsvtn0  29531  subfacp1lem1  29974  subfacp1lem5  29979  subfacval2  29982  subfaclim  29983  cvmliftlem2  30081  cvmliftlem7  30086  cvmliftlem10  30089  cvmliftlem11  30090  cvmliftlem13  30091  bcm1nt  30444  bcprod  30445  iprodgam  30449  faclimlem1  30450  faclimlem2  30451  faclim2  30455  nn0prpwlem  31049  nn0prpw  31050  poimirlem1  32005  poimirlem2  32006  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem9  32013  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem13  32017  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem31  32035  irrapxlem4  35740  irrapxlem5  35741  pellexlem2  35745  pellexlem6  35749  pell1234qrne0  35770  pell1234qrreccl  35771  pell1234qrmulcl  35772  pell1234qrdich  35778  pell14qrdich  35786  pell1qrge1  35787  pell1qr1  35788  pell14qrgapw  35793  rmxyneg  35839  rmxm1  35853  rmxluc  35855  rmxdbl  35858  jm2.19lem1  35915  jm2.27c  35933  phisum  36147  itgpowd  36170  relexpmulnn  36372  relexpmulg  36373  inductionexd  36664  hashnzfzclim  36741  bcccl  36758  bcc0  36759  bccp1k  36760  bccm1k  36761  binomcxplemwb  36767  fsumnncl  37746  mccllem  37774  clim1fr1  37776  sumnnodd  37807  dvsinexp  37877  dvxpaek  37912  dvnxpaek  37914  dvnprodlem2  37919  itgsinexplem1  37927  itgsinexp  37928  stoweidlem1  37973  stoweidlem11  37983  stoweidlem25  37997  stoweidlem26  37998  stoweidlem34  38007  stoweidlem37  38010  stoweidlem38  38011  stoweidlem42  38015  wallispi2lem1  38045  wallispi2  38047  stirlinglem4  38051  stirlinglem5  38052  stirlinglem10  38057  stirlinglem15  38062  dirkertrigeqlem3  38074  dirkertrigeq  38075  dirkercncflem2  38078  dirkercncflem4  38080  fourierdlem11  38092  fourierdlem15  38096  fourierdlem79  38161  fourierdlem83  38165  sqwvfourb  38205  etransclem14  38225  etransclem15  38226  etransclem20  38231  etransclem21  38232  etransclem22  38233  etransclem23  38234  etransclem24  38235  etransclem25  38236  etransclem28  38239  etransclem31  38242  etransclem32  38243  etransclem33  38244  etransclem34  38245  etransclem35  38246  etransclem38  38249  etransclem41  38252  etransclem44  38255  etransclem45  38256  etransclem47  38258  etransclem48OLD  38259  etransclem48  38260  nnfoctbdjlem  38409  deccarry  38860  iccpartgtprec  38879  oexpnegALTV  38951  perfectALTVlem1  38988  perfectALTVlem2  38989  perfectALTV  38990  proththdlem  39058  proththd  39059  eucrct2eupth  40157  nnpw2pmod  40902  nnolog2flm1  40909  blennn0em1  40910  blengt1fldiv2p1  40912  nn0sumshdiglemB  40939
  Copyright terms: Public domain W3C validator