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

Theorem nncnd 10622
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 10611 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3429 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   CCcc 9534   NNcn 10606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-i2m1 9604  ax-1ne0 9605  ax-rrecex 9608  ax-cnre 9609
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-om 6690  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-nn 10607
This theorem is referenced by:  facdiv  12469  facndiv  12470  faclbnd  12472  faclbnd5  12480  faclbnd6  12481  facubnd  12482  facavg  12483  bccmpl  12491  bcn0  12492  bcn1  12495  bcm1k  12497  bcp1n  12498  bcp1nk  12499  bcval5  12500  bcpasc  12503  permnn  12508  hashf1  12617  hashfac  12618  relexpaddnn  13107  binom11  13883  binom1dif  13884  climcndslem2  13901  arisum2  13912  trireciplem  13913  trirecip  13914  geo2sum  13922  geo2lim  13924  fprodfac  14020  risefacfac  14081  fallfacfwd  14082  fallfacval4  14089  bcfallfac  14090  fallfacfac  14091  bpolycl  14098  bpolysum  14099  bpolydiflem  14100  fsumkthpow  14102  eftcl  14121  eftabs  14123  efcllem  14125  ege2le3  14137  efcj  14139  efaddlem  14140  eftlub  14156  eirrlem  14249  sqr2irrlem  14293  oexpneg  14361  bitsp1  14397  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsmod  14403  bitscmp  14405  bitsinv1lem  14408  bitsinv1  14409  2ebits  14414  bitsinvp1  14416  sadcaddlem  14424  sadadd3  14428  bitsres  14440  bitsuz  14441  bitsshft  14442  mulgcd  14507  rplpwr  14517  sqgcd  14519  lcmgcdlem  14564  3lcm2e6woprm  14573  prmind2  14628  isprm5  14644  divgcdodd  14646  prmdvdsexpr  14662  coprmprod  14671  coprmproddvdslem  14672  qmuldeneqnum  14689  divnumden  14690  qnumgt0  14692  numdensq  14696  hashdvds  14716  phiprmpw  14717  prmdiv  14726  prmdivdiv  14728  modprm0  14749  pythagtriplem4  14762  pythagtriplem6  14764  pythagtriplem7  14765  pythagtriplem14  14771  pythagtriplem15  14772  pythagtriplem19  14776  pythagtrip  14777  pcprendvds2  14784  pcpre1  14785  pcpremul  14786  pceulem  14788  pcdiv  14795  pcqmul  14796  pcelnn  14812  pcid  14815  pc2dvds  14821  pcaddlem  14826  pcadd  14827  pcfaclem  14836  qexpz  14839  expnprm  14840  prmpwdvds  14841  pockthlem  14842  pockthg  14843  infpnlem1  14847  prmreclem1  14853  prmreclem2  14854  prmreclem3  14855  prmreclem4  14856  prmreclem6  14858  4sqlem6  14880  4sqlem7  14881  4sqlem10  14884  mul4sqlem  14890  4sqlem11  14892  4sqlem12  14893  4sqlem14OLD  14895  4sqlem17OLD  14898  4sqlem18OLD  14899  4sqlem14  14901  4sqlem17  14904  4sqlem18  14905  vdwlem1  14924  vdwlem2  14925  vdwlem3  14926  vdwlem5  14928  vdwlem6  14929  vdwlem8  14931  vdwlem9  14932  vdwlem10  14933  vdwlem12  14935  ramub1lem2  14978  ramcl  14980  prmop1  14989  prmdvdsprmo  14993  prmgaplem7  15020  prmgaplem8  15021  gsumccat  16618  mulgnndir  16773  mulgnnass  16779  psgnunilem5  17128  odf1o2  17215  pgp0  17241  sylow1lem1  17243  odcau  17249  sylow2blem3  17267  sylow3lem3  17274  sylow3lem4  17275  gexexlem  17483  ablfacrp2  17693  ablfac1lem  17694  ablfac1eu  17699  pgpfac1lem3a  17702  pgpfac1lem3  17703  zringlpirlem3OLD  19048  zringlpirlem3  19050  znrrg  19129  cpmadugsumlemF  19893  lebnumlem3  21984  lebnumlem3OLD  21987  ovollb2lem  22434  ovolunlem1a  22442  ovolunlem1  22443  uniioombllem3  22536  uniioombllem4  22537  dyaddisjlem  22546  mbfi1fseqlem3  22668  mbfi1fseqlem4  22669  dgrcolem1  23220  vieta1lem1  23256  vieta1lem2  23257  elqaalem2  23266  elqaalem3  23267  elqaalem2OLD  23269  elqaalem3OLD  23270  aalioulem1  23281  aaliou3lem2  23292  aaliou3lem8  23294  aaliou3lem6  23297  aaliou3lem9  23299  taylfvallem1  23305  tayl0  23310  taylply2  23316  taylply  23317  dvtaylp  23318  taylthlem1  23321  taylthlem2  23322  pserdvlem2  23376  advlogexp  23593  cxpmul2  23627  cxpeq  23690  atantayl3  23858  leibpi  23861  log2cnv  23863  log2tlbnd  23864  birthdaylem2  23871  birthdaylem3  23872  amgmlem  23908  amgm  23909  emcllem5  23918  fsumharmonic  23930  zetacvg  23933  dmgmdivn0  23946  lgamgulmlem3  23949  lgamgulmlem4  23950  lgamgulmlem5  23951  lgamgulmlem6  23952  lgamgulm2  23954  lgamcvg2  23973  gamcvg  23974  gamcvg2lem  23977  facgam  23984  wilthlem1  23986  wilthlem2  23987  wilthlem3  23988  basellem1  24000  basellem2  24001  basellem3  24002  basellem4  24003  basellem5  24004  basellem8  24007  vmaprm  24037  sgmval2  24063  0sgm  24064  sgmf  24065  vma1  24086  dvdsdivcl  24103  fsumdvdsdiaglem  24105  dvdsflf1o  24109  muinv  24115  dvdsmulf1o  24116  sgmppw  24118  1sgmprm  24120  1sgm2ppw  24121  sgmmul  24122  chtublem  24132  fsumvma2  24135  chpchtsum  24140  logfaclbnd  24143  logexprlim  24146  mersenne  24148  perfect1  24149  perfectlem1  24150  perfectlem2  24151  perfect  24152  dchrsum2  24189  dchrhash  24192  bcmono  24198  bcp1ctr  24200  bclbnd  24201  bposlem1  24205  bposlem2  24206  bposlem3  24207  bposlem5  24209  bposlem6  24210  lgsval2lem  24227  lgsqrlem2  24263  lgseisenlem1  24270  lgseisenlem4  24273  lgsquadlem1  24275  lgsquadlem2  24276  lgsquadlem3  24277  lgsquad2  24281  m1lgs  24283  2sqlem3  24287  2sqlem4  24288  chebbnd1lem1  24300  chebbnd1  24303  rplogsumlem1  24315  rplogsumlem2  24316  rpvmasumlem  24318  dchrisumlem1  24320  dchrmusum2  24325  dchrvmasumlem1  24326  dchrvmasum2lem  24327  dchrvmasum2if  24328  dchrvmasumlem2  24329  dchrvmasumlem3  24330  dchrvmasumiflem1  24332  dchrisum0flblem1  24339  dchrisum0flblem2  24340  dchrisum0fno1  24342  rpvmasum2  24343  rplogsum  24358  mulogsumlem  24362  mulogsum  24363  mulog2sumlem2  24366  vmalogdivsum2  24369  vmalogdivsum  24370  2vmadivsumlem  24371  logsqvma  24373  selberglem2  24377  selberglem3  24378  selberg  24379  selberg2lem  24381  logdivbnd  24387  selberg3lem1  24388  selberg4lem1  24391  pntrsumo1  24396  pntrsumbnd2  24398  selberg3r  24400  selberg4r  24401  selberg34r  24402  pntsval2  24407  pntrlog2bndlem2  24409  pntrlog2bndlem4  24411  pntrlog2bndlem6  24414  pntpbnd1  24417  pntpbnd2  24418  pntlemg  24429  pntlemn  24431  pntlemf  24436  pnt  24445  padicabvf  24462  ostth2lem2  24465  ostth3  24469  hashclwwlkn  25557  eupares  25696  numdenneg  28373  ltesubnnd  28378  1smat1  28623  madjusmdetlem2  28647  madjusmdetlem4  28649  qqhnm  28787  oddpwdc  29180  eulerpartlemsv2  29184  eulerpartlems  29186  eulerpartlemsv3  29187  eulerpartlemgc  29188  eulerpartlemv  29190  eulerpartlemgs2  29206  fibp1  29227  ballotlemfc0  29318  ballotlemfcc  29319  signsvtn0  29452  subfacp1lem1  29895  subfacp1lem5  29900  subfacval2  29903  subfaclim  29904  cvmliftlem2  30002  cvmliftlem7  30007  cvmliftlem10  30010  cvmliftlem11  30011  cvmliftlem13  30012  bcm1nt  30366  bcprod  30367  iprodgam  30371  faclimlem1  30372  faclimlem2  30373  faclim2  30377  nn0prpwlem  30971  nn0prpw  30972  poimirlem1  31934  poimirlem2  31935  poimirlem6  31939  poimirlem7  31940  poimirlem8  31941  poimirlem9  31942  poimirlem10  31943  poimirlem11  31944  poimirlem12  31945  poimirlem13  31946  poimirlem15  31948  poimirlem16  31949  poimirlem17  31950  poimirlem18  31951  poimirlem19  31952  poimirlem20  31953  poimirlem21  31954  poimirlem22  31955  poimirlem23  31956  poimirlem24  31957  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem31  31964  irrapxlem4  35663  irrapxlem5  35664  pellexlem2  35668  pellexlem6  35672  pell1234qrne0  35693  pell1234qrreccl  35694  pell1234qrmulcl  35695  pell1234qrdich  35701  pell14qrdich  35709  pell1qrge1  35710  pell1qr1  35711  pell14qrgapw  35716  rmxyneg  35762  rmxm1  35776  rmxluc  35778  rmxdbl  35781  jm2.19lem1  35838  jm2.27c  35856  phisum  36070  itgpowd  36093  relexpmulnn  36295  relexpmulg  36296  inductionexd  36587  hashnzfzclim  36665  bcccl  36682  bcc0  36683  bccp1k  36684  bccm1k  36685  binomcxplemwb  36691  fsumnncl  37644  mccllem  37671  clim1fr1  37673  sumnnodd  37704  dvsinexp  37774  dvxpaek  37809  dvnxpaek  37811  dvnprodlem2  37816  itgsinexplem1  37824  itgsinexp  37825  stoweidlem1  37855  stoweidlem11  37865  stoweidlem25  37879  stoweidlem26  37880  stoweidlem34  37889  stoweidlem37  37892  stoweidlem38  37893  stoweidlem42  37897  wallispi2lem1  37927  wallispi2  37929  stirlinglem4  37933  stirlinglem5  37934  stirlinglem10  37939  stirlinglem15  37944  dirkertrigeqlem3  37956  dirkertrigeq  37957  dirkercncflem2  37960  dirkercncflem4  37962  fourierdlem11  37974  fourierdlem15  37978  fourierdlem79  38043  fourierdlem83  38047  sqwvfourb  38087  etransclem14  38107  etransclem15  38108  etransclem20  38113  etransclem21  38114  etransclem22  38115  etransclem23  38116  etransclem24  38117  etransclem25  38118  etransclem28  38121  etransclem31  38124  etransclem32  38125  etransclem33  38126  etransclem34  38127  etransclem35  38128  etransclem38  38131  etransclem41  38134  etransclem44  38137  etransclem45  38138  etransclem47  38140  etransclem48OLD  38141  etransclem48  38142  nnfoctbdjlem  38287  deccarry  38709  iccpartgtprec  38728  oexpnegALTV  38800  perfectALTVlem1  38837  perfectALTVlem2  38838  perfectALTV  38839  proththdlem  38907  proththd  38908  nnpw2pmod  40381  nnolog2flm1  40388  blennn0em1  40389  blengt1fldiv2p1  40391  nn0sumshdiglemB  40418
  Copyright terms: Public domain W3C validator