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

Theorem nncnd 10359
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 10348 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3375 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9301   NNcn 10343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-i2m1 9371  ax-1ne0 9372  ax-rrecex 9375  ax-cnre 9376
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-om 6498  df-recs 6853  df-rdg 6887  df-nn 10344
This theorem is referenced by:  facdiv  12084  facndiv  12085  faclbnd  12087  faclbnd5  12095  faclbnd6  12096  facubnd  12097  facavg  12098  bccmpl  12106  bcn0  12107  bcn1  12110  bcm1k  12112  bcp1n  12113  bcp1nk  12114  bcval5  12115  bcpasc  12118  permnn  12123  hashf1  12231  hashfac  12232  wrdeqcats1  12389  binom11  13316  binom1dif  13317  climcndslem2  13334  arisum2  13344  trireciplem  13345  trirecip  13346  geo2sum  13354  geo2lim  13356  eftcl  13380  eftabs  13382  efcllem  13384  ege2le3  13396  efcj  13398  efaddlem  13399  eftlub  13414  eirrlem  13507  sqr2irrlem  13551  oexpneg  13616  bitsp1  13648  bitsfzolem  13651  bitsfzo  13652  bitsmod  13653  bitscmp  13655  bitsinv1lem  13658  bitsinv1  13659  2ebits  13664  bitsinvp1  13666  sadcaddlem  13674  sadadd3  13678  bitsres  13690  bitsuz  13691  bitsshft  13692  mulgcd  13751  rplpwr  13761  sqgcd  13763  prmind2  13795  isprm5  13819  prmdvdsexpr  13823  divgcdodd  13826  qmuldeneqnum  13846  divnumden  13847  qnumgt0  13849  numdensq  13853  hashdvds  13871  phiprmpw  13872  prmdiv  13881  prmdivdiv  13883  modprm0  13894  pythagtriplem4  13907  pythagtriplem6  13909  pythagtriplem7  13910  pythagtriplem14  13916  pythagtriplem15  13917  pythagtriplem19  13921  pythagtrip  13922  pcprendvds2  13929  pcpre1  13930  pcpremul  13931  pceulem  13933  pcdiv  13940  pcqmul  13941  pcelnn  13957  pcid  13960  pc2dvds  13966  pcaddlem  13971  pcadd  13972  pcfaclem  13981  qexpz  13984  expnprm  13985  prmpwdvds  13986  pockthlem  13987  pockthg  13988  infpnlem1  13992  prmreclem1  13998  prmreclem2  13999  prmreclem3  14000  prmreclem4  14001  prmreclem6  14003  4sqlem6  14025  4sqlem7  14026  4sqlem10  14029  mul4sqlem  14035  4sqlem11  14037  4sqlem12  14038  4sqlem14  14040  4sqlem17  14043  4sqlem18  14044  vdwlem1  14063  vdwlem2  14064  vdwlem3  14065  vdwlem5  14067  vdwlem6  14068  vdwlem8  14070  vdwlem9  14071  vdwlem10  14072  vdwlem12  14074  ramub1lem2  14109  ramcl  14111  gsumccat  15540  mulgnndir  15670  mulgnnass  15676  psgnunilem5  16021  odf1o2  16093  pgp0  16116  sylow1lem1  16118  odcau  16124  sylow2blem3  16142  sylow3lem3  16149  sylow3lem4  16150  gexexlem  16355  ablfacrp2  16590  ablfac1lem  16591  ablfac1eu  16596  pgpfac1lem3a  16599  pgpfac1lem3  16600  zringlpirlem3  17927  zlpirlem3  17932  znrrg  18020  lebnumlem3  20557  ovollb2lem  20993  ovolunlem1a  21001  ovolunlem1  21002  uniioombllem3  21087  uniioombllem4  21088  dyaddisjlem  21097  mbfi1fseqlem3  21217  mbfi1fseqlem4  21218  dgrcolem1  21762  vieta1lem1  21798  vieta1lem2  21799  elqaalem2  21808  elqaalem3  21809  aalioulem1  21820  aaliou3lem2  21831  aaliou3lem8  21833  aaliou3lem6  21836  aaliou3lem9  21838  taylfvallem1  21844  tayl0  21849  taylply2  21855  taylply  21856  dvtaylp  21857  taylthlem1  21860  taylthlem2  21861  pserdvlem2  21915  advlogexp  22122  cxpmul2  22156  cxpeq  22217  atantayl3  22356  leibpi  22359  log2cnv  22361  log2tlbnd  22362  birthdaylem2  22368  birthdaylem3  22369  amgmlem  22405  amgm  22406  emcllem5  22415  fsumharmonic  22427  wilthlem1  22428  wilthlem2  22429  wilthlem3  22430  basellem1  22440  basellem2  22441  basellem3  22442  basellem4  22443  basellem5  22444  basellem8  22447  vmaprm  22477  sgmval2  22503  0sgm  22504  sgmf  22505  vma1  22526  dvdsdivcl  22543  fsumdvdsdiaglem  22545  dvdsflf1o  22549  muinv  22555  dvdsmulf1o  22556  sgmppw  22558  1sgmprm  22560  1sgm2ppw  22561  sgmmul  22562  chtublem  22572  fsumvma2  22575  chpchtsum  22580  logfaclbnd  22583  logexprlim  22586  mersenne  22588  perfect1  22589  perfectlem1  22590  perfectlem2  22591  perfect  22592  dchrsum2  22629  dchrhash  22632  bcmono  22638  bcp1ctr  22640  bclbnd  22641  bposlem1  22645  bposlem2  22646  bposlem3  22647  bposlem5  22649  bposlem6  22650  lgsval2lem  22667  lgsqrlem2  22703  lgseisenlem1  22710  lgseisenlem4  22713  lgsquadlem1  22715  lgsquadlem2  22716  lgsquadlem3  22717  lgsquad2  22721  m1lgs  22723  2sqlem3  22727  2sqlem4  22728  chebbnd1lem1  22740  chebbnd1  22743  rplogsumlem1  22755  rplogsumlem2  22756  rpvmasumlem  22758  dchrisumlem1  22760  dchrmusum2  22765  dchrvmasumlem1  22766  dchrvmasum2lem  22767  dchrvmasum2if  22768  dchrvmasumlem2  22769  dchrvmasumlem3  22770  dchrvmasumiflem1  22772  dchrisum0flblem1  22779  dchrisum0flblem2  22780  dchrisum0fno1  22782  rpvmasum2  22783  rplogsum  22798  mulogsumlem  22802  mulogsum  22803  mulog2sumlem2  22806  vmalogdivsum2  22809  vmalogdivsum  22810  2vmadivsumlem  22811  logsqvma  22813  selberglem2  22817  selberglem3  22818  selberg  22819  selberg2lem  22821  logdivbnd  22827  selberg3lem1  22828  selberg4lem1  22831  pntrsumo1  22836  pntrsumbnd2  22838  selberg3r  22840  selberg4r  22841  selberg34r  22842  pntsval2  22847  pntrlog2bndlem2  22849  pntrlog2bndlem4  22851  pntrlog2bndlem6  22854  pntpbnd1  22857  pntpbnd2  22858  pntlemg  22869  pntlemn  22871  pntlemf  22876  pnt  22885  padicabvf  22902  ostth2lem2  22905  ostth3  22909  eupares  23618  numdenneg  26108  ltesubnnd  26113  qqhnm  26441  oddpwdc  26759  eulerpartlemsv2  26763  eulerpartlems  26765  eulerpartlemsv3  26766  eulerpartlemgc  26767  eulerpartlemv  26769  eulerpartlemgs2  26785  fibp1  26806  ballotlemfc0  26897  ballotlemfcc  26898  signsvtn0  26993  zetacvg  27023  dmgmdivn0  27036  lgamgulmlem3  27039  lgamgulmlem4  27040  lgamgulmlem5  27041  lgamgulmlem6  27042  lgamgulm2  27044  lgamcvg2  27063  gamcvg  27064  gamcvg2lem  27067  facgam  27074  subfacp1lem1  27089  subfacp1lem5  27094  subfacval2  27097  subfaclim  27098  cvmliftlem2  27197  cvmliftlem7  27202  cvmliftlem10  27205  cvmliftlem11  27206  cvmliftlem13  27207  fprodfac  27505  iprodgam  27528  risefacfac  27560  fallfacfwd  27561  fallfacval4  27568  bcfallfac  27569  fallfacfac  27570  faclimlem1  27571  faclimlem2  27572  faclim2  27576  bpolycl  28217  bpolysum  28218  bpolydiflem  28219  fsumkthpow  28221  nn0prpwlem  28543  nn0prpw  28544  irrapxlem4  29192  irrapxlem5  29193  pellexlem2  29197  pellexlem6  29201  pell1234qrne0  29220  pell1234qrreccl  29221  pell1234qrmulcl  29222  pell1234qrdich  29228  pell14qrdich  29236  pell1qrge1  29237  pell1qr1  29238  pell14qrgapw  29243  rmxyneg  29287  rmxm1  29301  rmxluc  29303  rmxdbl  29306  jm2.19lem1  29364  jm2.27c  29382  phisum  29593  itgpowd  29616  clim1fr1  29800  dvsinexp  29813  itgsinexplem1  29820  itgsinexp  29821  stoweidlem1  29822  stoweidlem11  29832  stoweidlem25  29846  stoweidlem26  29847  stoweidlem34  29855  stoweidlem37  29858  stoweidlem38  29859  stoweidlem42  29863  wallispi2lem1  29892  wallispi2  29894  stirlinglem4  29898  stirlinglem5  29899  stirlinglem10  29904  stirlinglem15  29909  hashclwwlkn  30536
  Copyright terms: Public domain W3C validator