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

Theorem nncnd 10591
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 10580 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3439 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   CCcc 9519   NNcn 10575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-i2m1 9589  ax-1ne0 9590  ax-rrecex 9593  ax-cnre 9594
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-om 6683  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-nn 10576
This theorem is referenced by:  facdiv  12407  facndiv  12408  faclbnd  12410  faclbnd5  12418  faclbnd6  12419  facubnd  12420  facavg  12421  bccmpl  12429  bcn0  12430  bcn1  12433  bcm1k  12435  bcp1n  12436  bcp1nk  12437  bcval5  12438  bcpasc  12441  permnn  12446  hashf1  12553  hashfac  12554  relexpaddnn  13031  binom11  13793  binom1dif  13794  climcndslem2  13811  arisum2  13822  trireciplem  13823  trirecip  13824  geo2sum  13832  geo2lim  13834  fprodfac  13927  risefacfac  13978  fallfacfwd  13979  fallfacval4  13986  bcfallfac  13987  fallfacfac  13988  bpolycl  13995  bpolysum  13996  bpolydiflem  13997  fsumkthpow  13999  eftcl  14016  eftabs  14018  efcllem  14020  ege2le3  14032  efcj  14034  efaddlem  14035  eftlub  14051  eirrlem  14144  sqr2irrlem  14188  oexpneg  14256  bitsp1  14288  bitsfzolem  14291  bitsfzo  14292  bitsmod  14293  bitscmp  14295  bitsinv1lem  14298  bitsinv1  14299  2ebits  14304  bitsinvp1  14306  sadcaddlem  14314  sadadd3  14318  bitsres  14330  bitsuz  14331  bitsshft  14332  mulgcd  14391  rplpwr  14401  sqgcd  14403  prmind2  14435  isprm5  14460  prmdvdsexpr  14464  divgcdodd  14467  qmuldeneqnum  14487  divnumden  14488  qnumgt0  14490  numdensq  14494  hashdvds  14512  phiprmpw  14513  prmdiv  14522  prmdivdiv  14524  modprm0  14537  pythagtriplem4  14550  pythagtriplem6  14552  pythagtriplem7  14553  pythagtriplem14  14559  pythagtriplem15  14560  pythagtriplem19  14564  pythagtrip  14565  pcprendvds2  14572  pcpre1  14573  pcpremul  14574  pceulem  14576  pcdiv  14583  pcqmul  14584  pcelnn  14600  pcid  14603  pc2dvds  14609  pcaddlem  14614  pcadd  14615  pcfaclem  14624  qexpz  14627  expnprm  14628  prmpwdvds  14629  pockthlem  14630  pockthg  14631  infpnlem1  14635  prmreclem1  14641  prmreclem2  14642  prmreclem3  14643  prmreclem4  14644  prmreclem6  14646  4sqlem6  14668  4sqlem7  14669  4sqlem10  14672  mul4sqlem  14678  4sqlem11  14680  4sqlem12  14681  4sqlem14  14683  4sqlem17  14686  4sqlem18  14687  vdwlem1  14706  vdwlem2  14707  vdwlem3  14708  vdwlem5  14710  vdwlem6  14711  vdwlem8  14713  vdwlem9  14714  vdwlem10  14715  vdwlem12  14717  ramub1lem2  14752  ramcl  14754  gsumccat  16331  mulgnndir  16486  mulgnnass  16492  psgnunilem5  16841  odf1o2  16915  pgp0  16938  sylow1lem1  16940  odcau  16946  sylow2blem3  16964  sylow3lem3  16971  sylow3lem4  16972  gexexlem  17180  ablfacrp2  17436  ablfac1lem  17437  ablfac1eu  17442  pgpfac1lem3a  17445  pgpfac1lem3  17446  zringlpirlem3  18822  znrrg  18900  cpmadugsumlemF  19667  lebnumlem3  21753  ovollb2lem  22189  ovolunlem1a  22197  ovolunlem1  22198  uniioombllem3  22284  uniioombllem4  22285  dyaddisjlem  22294  mbfi1fseqlem3  22414  mbfi1fseqlem4  22415  dgrcolem1  22960  vieta1lem1  22996  vieta1lem2  22997  elqaalem2  23006  elqaalem3  23007  aalioulem1  23018  aaliou3lem2  23029  aaliou3lem8  23031  aaliou3lem6  23034  aaliou3lem9  23036  taylfvallem1  23042  tayl0  23047  taylply2  23053  taylply  23054  dvtaylp  23055  taylthlem1  23058  taylthlem2  23059  pserdvlem2  23113  advlogexp  23328  cxpmul2  23362  cxpeq  23425  atantayl3  23593  leibpi  23596  log2cnv  23598  log2tlbnd  23599  birthdaylem2  23606  birthdaylem3  23607  amgmlem  23643  amgm  23644  emcllem5  23653  fsumharmonic  23665  zetacvg  23668  dmgmdivn0  23681  lgamgulmlem3  23684  lgamgulmlem4  23685  lgamgulmlem5  23686  lgamgulmlem6  23687  lgamgulm2  23689  lgamcvg2  23708  gamcvg  23709  gamcvg2lem  23712  facgam  23719  wilthlem1  23721  wilthlem2  23722  wilthlem3  23723  basellem1  23733  basellem2  23734  basellem3  23735  basellem4  23736  basellem5  23737  basellem8  23740  vmaprm  23770  sgmval2  23796  0sgm  23797  sgmf  23798  vma1  23819  dvdsdivcl  23836  fsumdvdsdiaglem  23838  dvdsflf1o  23842  muinv  23848  dvdsmulf1o  23849  sgmppw  23851  1sgmprm  23853  1sgm2ppw  23854  sgmmul  23855  chtublem  23865  fsumvma2  23868  chpchtsum  23873  logfaclbnd  23876  logexprlim  23879  mersenne  23881  perfect1  23882  perfectlem1  23883  perfectlem2  23884  perfect  23885  dchrsum2  23922  dchrhash  23925  bcmono  23931  bcp1ctr  23933  bclbnd  23934  bposlem1  23938  bposlem2  23939  bposlem3  23940  bposlem5  23942  bposlem6  23943  lgsval2lem  23960  lgsqrlem2  23996  lgseisenlem1  24003  lgseisenlem4  24006  lgsquadlem1  24008  lgsquadlem2  24009  lgsquadlem3  24010  lgsquad2  24014  m1lgs  24016  2sqlem3  24020  2sqlem4  24021  chebbnd1lem1  24033  chebbnd1  24036  rplogsumlem1  24048  rplogsumlem2  24049  rpvmasumlem  24051  dchrisumlem1  24053  dchrmusum2  24058  dchrvmasumlem1  24059  dchrvmasum2lem  24060  dchrvmasum2if  24061  dchrvmasumlem2  24062  dchrvmasumlem3  24063  dchrvmasumiflem1  24065  dchrisum0flblem1  24072  dchrisum0flblem2  24073  dchrisum0fno1  24075  rpvmasum2  24076  rplogsum  24091  mulogsumlem  24095  mulogsum  24096  mulog2sumlem2  24099  vmalogdivsum2  24102  vmalogdivsum  24103  2vmadivsumlem  24104  logsqvma  24106  selberglem2  24110  selberglem3  24111  selberg  24112  selberg2lem  24114  logdivbnd  24120  selberg3lem1  24121  selberg4lem1  24124  pntrsumo1  24129  pntrsumbnd2  24131  selberg3r  24133  selberg4r  24134  selberg34r  24135  pntsval2  24140  pntrlog2bndlem2  24142  pntrlog2bndlem4  24144  pntrlog2bndlem6  24147  pntpbnd1  24150  pntpbnd2  24151  pntlemg  24162  pntlemn  24164  pntlemf  24169  pnt  24178  padicabvf  24195  ostth2lem2  24198  ostth3  24202  hashclwwlkn  25240  eupares  25379  numdenneg  28045  ltesubnnd  28050  qqhnm  28409  oddpwdc  28785  eulerpartlemsv2  28789  eulerpartlems  28791  eulerpartlemsv3  28792  eulerpartlemgc  28793  eulerpartlemv  28795  eulerpartlemgs2  28811  fibp1  28832  ballotlemfc0  28923  ballotlemfcc  28924  signsvtn0  29019  subfacp1lem1  29463  subfacp1lem5  29468  subfacval2  29471  subfaclim  29472  cvmliftlem2  29570  cvmliftlem7  29575  cvmliftlem10  29578  cvmliftlem11  29579  cvmliftlem13  29580  bcm1nt  29933  bcprod  29934  iprodgam  29938  faclimlem1  29939  faclimlem2  29940  faclim2  29944  nn0prpwlem  30537  nn0prpw  30538  irrapxlem4  35102  irrapxlem5  35103  pellexlem2  35107  pellexlem6  35111  pell1234qrne0  35130  pell1234qrreccl  35131  pell1234qrmulcl  35132  pell1234qrdich  35138  pell14qrdich  35146  pell1qrge1  35147  pell1qr1  35148  pell14qrgapw  35153  rmxyneg  35197  rmxm1  35211  rmxluc  35213  rmxdbl  35216  jm2.19lem1  35273  jm2.27c  35291  phisum  35503  itgpowd  35526  relexpmulnn  35668  relexpmulg  35669  inductionexd  35958  lcmgcdlem  36040  hashnzfzclim  36055  bcccl  36072  bcc0  36073  bccp1k  36074  bccm1k  36075  binomcxplemwb  36081  fsumnncl  36921  mccllem  36954  clim1fr1  36956  sumnnodd  36985  dvsinexp  37054  dvxpaek  37086  dvnxpaek  37088  dvnprodlem2  37093  itgsinexplem1  37101  itgsinexp  37102  stoweidlem1  37132  stoweidlem11  37142  stoweidlem25  37156  stoweidlem26  37157  stoweidlem34  37165  stoweidlem37  37168  stoweidlem38  37169  stoweidlem42  37173  wallispi2lem1  37202  wallispi2  37204  stirlinglem4  37208  stirlinglem5  37209  stirlinglem10  37214  stirlinglem15  37219  dirkertrigeqlem3  37231  dirkertrigeq  37232  dirkercncflem2  37235  dirkercncflem4  37237  fourierdlem11  37249  fourierdlem15  37253  fourierdlem79  37317  fourierdlem83  37321  sqwvfourb  37361  etransclem14  37380  etransclem15  37381  etransclem20  37386  etransclem21  37387  etransclem22  37388  etransclem23  37389  etransclem24  37390  etransclem25  37391  etransclem28  37394  etransclem31  37397  etransclem32  37398  etransclem33  37399  etransclem34  37400  etransclem35  37401  etransclem38  37404  etransclem41  37407  etransclem44  37410  etransclem45  37411  etransclem47  37413  etransclem48  37414  deccarry  37647  iccpartgtprec  37668  oexpnegALTV  37740  perfectALTVlem1  37777  perfectALTVlem2  37778  perfectALTV  37779  proththdlem  37840  proththd  37841  nnpw2pmod  38695  nnolog2flm1  38702  blennn0em1  38703  blengt1fldiv2p1  38705  nn0sumshdiglemB  38732
  Copyright terms: Public domain W3C validator