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

Theorem nncnd 10621
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 10610 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3459 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   CCcc 9533   NNcn 10605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-i2m1 9603  ax-1ne0 9604  ax-rrecex 9607  ax-cnre 9608
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6300  df-om 6699  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-nn 10606
This theorem is referenced by:  facdiv  12465  facndiv  12466  faclbnd  12468  faclbnd5  12476  faclbnd6  12477  facubnd  12478  facavg  12479  bccmpl  12487  bcn0  12488  bcn1  12491  bcm1k  12493  bcp1n  12494  bcp1nk  12495  bcval5  12496  bcpasc  12499  permnn  12504  hashf1  12611  hashfac  12612  relexpaddnn  13093  binom11  13868  binom1dif  13869  climcndslem2  13886  arisum2  13897  trireciplem  13898  trirecip  13899  geo2sum  13907  geo2lim  13909  fprodfac  14005  risefacfac  14066  fallfacfwd  14067  fallfacval4  14074  bcfallfac  14075  fallfacfac  14076  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  fsumkthpow  14087  eftcl  14106  eftabs  14108  efcllem  14110  ege2le3  14122  efcj  14124  efaddlem  14125  eftlub  14141  eirrlem  14234  sqr2irrlem  14278  oexpneg  14346  bitsp1  14382  bitsfzolem  14385  bitsfzolemOLD  14386  bitsfzo  14387  bitsmod  14388  bitscmp  14390  bitsinv1lem  14393  bitsinv1  14394  2ebits  14399  bitsinvp1  14401  sadcaddlem  14409  sadadd3  14413  bitsres  14425  bitsuz  14426  bitsshft  14427  mulgcd  14492  rplpwr  14502  sqgcd  14504  lcmgcdlem  14549  3lcm2e6woprm  14558  prmind2  14613  isprm5  14629  divgcdodd  14631  prmdvdsexpr  14647  coprmprod  14656  coprmproddvdslem  14657  qmuldeneqnum  14674  divnumden  14675  qnumgt0  14677  numdensq  14681  hashdvds  14701  phiprmpw  14702  prmdiv  14711  prmdivdiv  14713  modprm0  14734  pythagtriplem4  14747  pythagtriplem6  14749  pythagtriplem7  14750  pythagtriplem14  14756  pythagtriplem15  14757  pythagtriplem19  14761  pythagtrip  14762  pcprendvds2  14769  pcpre1  14770  pcpremul  14771  pceulem  14773  pcdiv  14780  pcqmul  14781  pcelnn  14797  pcid  14800  pc2dvds  14806  pcaddlem  14811  pcadd  14812  pcfaclem  14821  qexpz  14824  expnprm  14825  prmpwdvds  14826  pockthlem  14827  pockthg  14828  infpnlem1  14832  prmreclem1  14838  prmreclem2  14839  prmreclem3  14840  prmreclem4  14841  prmreclem6  14843  4sqlem6  14865  4sqlem7  14866  4sqlem10  14869  mul4sqlem  14875  4sqlem11  14877  4sqlem12  14878  4sqlem14OLD  14880  4sqlem17OLD  14883  4sqlem18OLD  14884  4sqlem14  14886  4sqlem17  14889  4sqlem18  14890  vdwlem1  14909  vdwlem2  14910  vdwlem3  14911  vdwlem5  14913  vdwlem6  14914  vdwlem8  14916  vdwlem9  14917  vdwlem10  14918  vdwlem12  14920  ramub1lem2  14963  ramcl  14965  prmop1  14974  prmdvdsprmo  14978  prmgaplem7  15005  prmgaplem8  15006  gsumccat  16603  mulgnndir  16758  mulgnnass  16764  psgnunilem5  17113  odf1o2  17200  pgp0  17226  sylow1lem1  17228  odcau  17234  sylow2blem3  17252  sylow3lem3  17259  sylow3lem4  17260  gexexlem  17468  ablfacrp2  17678  ablfac1lem  17679  ablfac1eu  17684  pgpfac1lem3a  17687  pgpfac1lem3  17688  zringlpirlem3OLD  19032  zringlpirlem3  19034  znrrg  19113  cpmadugsumlemF  19877  lebnumlem3  21968  lebnumlem3OLD  21971  ovollb2lem  22418  ovolunlem1a  22426  ovolunlem1  22427  uniioombllem3  22520  uniioombllem4  22521  dyaddisjlem  22530  mbfi1fseqlem3  22652  mbfi1fseqlem4  22653  dgrcolem1  23204  vieta1lem1  23240  vieta1lem2  23241  elqaalem2  23250  elqaalem3  23251  elqaalem2OLD  23253  elqaalem3OLD  23254  aalioulem1  23265  aaliou3lem2  23276  aaliou3lem8  23278  aaliou3lem6  23281  aaliou3lem9  23283  taylfvallem1  23289  tayl0  23294  taylply2  23300  taylply  23301  dvtaylp  23302  taylthlem1  23305  taylthlem2  23306  pserdvlem2  23360  advlogexp  23577  cxpmul2  23611  cxpeq  23674  atantayl3  23842  leibpi  23845  log2cnv  23847  log2tlbnd  23848  birthdaylem2  23855  birthdaylem3  23856  amgmlem  23892  amgm  23893  emcllem5  23902  fsumharmonic  23914  zetacvg  23917  dmgmdivn0  23930  lgamgulmlem3  23933  lgamgulmlem4  23934  lgamgulmlem5  23935  lgamgulmlem6  23936  lgamgulm2  23938  lgamcvg2  23957  gamcvg  23958  gamcvg2lem  23961  facgam  23968  wilthlem1  23970  wilthlem2  23971  wilthlem3  23972  basellem1  23984  basellem2  23985  basellem3  23986  basellem4  23987  basellem5  23988  basellem8  23991  vmaprm  24021  sgmval2  24047  0sgm  24048  sgmf  24049  vma1  24070  dvdsdivcl  24087  fsumdvdsdiaglem  24089  dvdsflf1o  24093  muinv  24099  dvdsmulf1o  24100  sgmppw  24102  1sgmprm  24104  1sgm2ppw  24105  sgmmul  24106  chtublem  24116  fsumvma2  24119  chpchtsum  24124  logfaclbnd  24127  logexprlim  24130  mersenne  24132  perfect1  24133  perfectlem1  24134  perfectlem2  24135  perfect  24136  dchrsum2  24173  dchrhash  24176  bcmono  24182  bcp1ctr  24184  bclbnd  24185  bposlem1  24189  bposlem2  24190  bposlem3  24191  bposlem5  24193  bposlem6  24194  lgsval2lem  24211  lgsqrlem2  24247  lgseisenlem1  24254  lgseisenlem4  24257  lgsquadlem1  24259  lgsquadlem2  24260  lgsquadlem3  24261  lgsquad2  24265  m1lgs  24267  2sqlem3  24271  2sqlem4  24272  chebbnd1lem1  24284  chebbnd1  24287  rplogsumlem1  24299  rplogsumlem2  24300  rpvmasumlem  24302  dchrisumlem1  24304  dchrmusum2  24309  dchrvmasumlem1  24310  dchrvmasum2lem  24311  dchrvmasum2if  24312  dchrvmasumlem2  24313  dchrvmasumlem3  24314  dchrvmasumiflem1  24316  dchrisum0flblem1  24323  dchrisum0flblem2  24324  dchrisum0fno1  24326  rpvmasum2  24327  rplogsum  24342  mulogsumlem  24346  mulogsum  24347  mulog2sumlem2  24350  vmalogdivsum2  24353  vmalogdivsum  24354  2vmadivsumlem  24355  logsqvma  24357  selberglem2  24361  selberglem3  24362  selberg  24363  selberg2lem  24365  logdivbnd  24371  selberg3lem1  24372  selberg4lem1  24375  pntrsumo1  24380  pntrsumbnd2  24382  selberg3r  24384  selberg4r  24385  selberg34r  24386  pntsval2  24391  pntrlog2bndlem2  24393  pntrlog2bndlem4  24395  pntrlog2bndlem6  24398  pntpbnd1  24401  pntpbnd2  24402  pntlemg  24413  pntlemn  24415  pntlemf  24420  pnt  24429  padicabvf  24446  ostth2lem2  24449  ostth3  24453  hashclwwlkn  25540  eupares  25679  numdenneg  28367  ltesubnnd  28372  1smat1  28619  madjusmdetlem2  28643  madjusmdetlem4  28645  qqhnm  28783  oddpwdc  29176  eulerpartlemsv2  29180  eulerpartlems  29182  eulerpartlemsv3  29183  eulerpartlemgc  29184  eulerpartlemv  29186  eulerpartlemgs2  29202  fibp1  29223  ballotlemfc0  29314  ballotlemfcc  29315  signsvtn0  29448  subfacp1lem1  29891  subfacp1lem5  29896  subfacval2  29899  subfaclim  29900  cvmliftlem2  29998  cvmliftlem7  30003  cvmliftlem10  30006  cvmliftlem11  30007  cvmliftlem13  30008  bcm1nt  30361  bcprod  30362  iprodgam  30366  faclimlem1  30367  faclimlem2  30368  faclim2  30372  nn0prpwlem  30964  nn0prpw  30965  poimirlem1  31849  poimirlem2  31850  poimirlem6  31854  poimirlem7  31855  poimirlem8  31856  poimirlem9  31857  poimirlem10  31858  poimirlem11  31859  poimirlem12  31860  poimirlem13  31861  poimirlem15  31863  poimirlem16  31864  poimirlem17  31865  poimirlem18  31866  poimirlem19  31867  poimirlem20  31868  poimirlem21  31869  poimirlem22  31870  poimirlem23  31871  poimirlem24  31872  poimirlem25  31873  poimirlem26  31874  poimirlem27  31875  poimirlem31  31879  irrapxlem4  35583  irrapxlem5  35584  pellexlem2  35588  pellexlem6  35592  pell1234qrne0  35613  pell1234qrreccl  35614  pell1234qrmulcl  35615  pell1234qrdich  35621  pell14qrdich  35629  pell1qrge1  35630  pell1qr1  35631  pell14qrgapw  35636  rmxyneg  35682  rmxm1  35696  rmxluc  35698  rmxdbl  35701  jm2.19lem1  35758  jm2.27c  35776  phisum  35990  itgpowd  36013  relexpmulnn  36155  relexpmulg  36156  inductionexd  36445  hashnzfzclim  36523  bcccl  36540  bcc0  36541  bccp1k  36542  bccm1k  36543  binomcxplemwb  36549  fsumnncl  37440  mccllem  37464  clim1fr1  37466  sumnnodd  37497  dvsinexp  37567  dvxpaek  37602  dvnxpaek  37604  dvnprodlem2  37609  itgsinexplem1  37617  itgsinexp  37618  stoweidlem1  37648  stoweidlem11  37658  stoweidlem25  37672  stoweidlem26  37673  stoweidlem34  37682  stoweidlem37  37685  stoweidlem38  37686  stoweidlem42  37690  wallispi2lem1  37720  wallispi2  37722  stirlinglem4  37726  stirlinglem5  37727  stirlinglem10  37732  stirlinglem15  37737  dirkertrigeqlem3  37749  dirkertrigeq  37750  dirkercncflem2  37753  dirkercncflem4  37755  fourierdlem11  37767  fourierdlem15  37771  fourierdlem79  37836  fourierdlem83  37840  sqwvfourb  37880  etransclem14  37900  etransclem15  37901  etransclem20  37906  etransclem21  37907  etransclem22  37908  etransclem23  37909  etransclem24  37910  etransclem25  37911  etransclem28  37914  etransclem31  37917  etransclem32  37918  etransclem33  37919  etransclem34  37920  etransclem35  37921  etransclem38  37924  etransclem41  37927  etransclem44  37930  etransclem45  37931  etransclem47  37933  etransclem48OLD  37934  etransclem48  37935  nnfoctbdjlem  38023  deccarry  38335  iccpartgtprec  38354  oexpnegALTV  38426  perfectALTVlem1  38463  perfectALTVlem2  38464  perfectALTV  38465  proththdlem  38533  proththd  38534  nnpw2pmod  39459  nnolog2flm1  39466  blennn0em1  39467  blengt1fldiv2p1  39469  nn0sumshdiglemB  39496
  Copyright terms: Public domain W3C validator