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

Theorem nncnd 9941
Description: A natural number 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 9930 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3282 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8914   NNcn 9925
This theorem is referenced by:  facdiv  11498  facndiv  11499  faclbnd  11501  faclbnd5  11509  faclbnd6  11510  facubnd  11511  facavg  11512  bccmpl  11520  bcn0  11521  bcn1  11524  bcm1k  11526  bcp1n  11527  bcp1nk  11528  bcval5  11529  bcpasc  11532  permnn  11537  hashf1  11626  hashfac  11627  wrdeqcats1  11708  binom11  12531  binom1dif  12532  climcndslem2  12550  arisum2  12560  trireciplem  12561  trirecip  12562  geo2sum  12570  geo2lim  12572  eftcl  12596  eftabs  12598  efcllem  12600  ege2le3  12612  efcj  12614  efaddlem  12615  eftlub  12630  eirrlem  12723  sqr2irrlem  12767  oexpneg  12831  bitsp1  12863  bitsfzolem  12866  bitsfzo  12867  bitsmod  12868  bitscmp  12870  bitsinv1lem  12873  bitsinv1  12874  2ebits  12879  bitsinvp1  12881  sadcaddlem  12889  sadadd3  12893  bitsres  12905  bitsuz  12906  bitsshft  12907  mulgcd  12966  rplpwr  12976  sqgcd  12978  prmind2  13010  isprm5  13032  prmdvdsexpr  13036  divgcdodd  13039  qmuldeneqnum  13059  divnumden  13060  qnumgt0  13062  numdensq  13066  hashdvds  13084  phiprmpw  13085  prmdiv  13094  prmdivdiv  13096  pythagtriplem4  13113  pythagtriplem6  13115  pythagtriplem7  13116  pythagtriplem14  13122  pythagtriplem15  13123  pythagtriplem19  13127  pythagtrip  13128  pcprendvds2  13135  pcpre1  13136  pcpremul  13137  pceulem  13139  pcdiv  13146  pcqmul  13147  pcelnn  13163  pcid  13166  pc2dvds  13172  pcaddlem  13177  pcadd  13178  pcfaclem  13187  qexpz  13190  expnprm  13191  prmpwdvds  13192  pockthlem  13193  pockthg  13194  infpnlem1  13198  prmreclem1  13204  prmreclem2  13205  prmreclem3  13206  prmreclem4  13207  prmreclem6  13209  4sqlem6  13231  4sqlem7  13232  4sqlem10  13235  mul4sqlem  13241  4sqlem11  13243  4sqlem12  13244  4sqlem14  13246  4sqlem17  13249  4sqlem18  13250  vdwlem1  13269  vdwlem2  13270  vdwlem3  13271  vdwlem5  13273  vdwlem6  13274  vdwlem8  13276  vdwlem9  13277  vdwlem10  13278  vdwlem12  13280  ramub1lem2  13315  ramcl  13317  gsumccat  14707  mulgnndir  14832  mulgnnass  14838  odf1o2  15127  pgp0  15150  sylow1lem1  15152  odcau  15158  sylow2blem3  15176  sylow3lem3  15183  sylow3lem4  15184  gexexlem  15387  ablfacrp2  15545  ablfac1lem  15546  ablfac1eu  15551  pgpfac1lem3a  15554  pgpfac1lem3  15555  zlpirlem3  16686  znrrg  16762  lebnumlem3  18852  ovollb2lem  19244  ovolunlem1a  19252  ovolunlem1  19253  uniioombllem3  19337  uniioombllem4  19338  dyaddisjlem  19347  mbfi1fseqlem3  19469  mbfi1fseqlem4  19470  dgrcolem1  20051  vieta1lem1  20087  vieta1lem2  20088  elqaalem2  20097  elqaalem3  20098  aalioulem1  20109  aaliou3lem2  20120  aaliou3lem8  20122  aaliou3lem6  20125  aaliou3lem9  20127  taylfvallem1  20133  tayl0  20138  taylply2  20144  taylply  20145  dvtaylp  20146  taylthlem1  20149  taylthlem2  20150  pserdvlem2  20204  advlogexp  20406  cxpmul2  20440  cxpeq  20501  atantayl3  20639  leibpi  20642  log2cnv  20644  log2tlbnd  20645  birthdaylem2  20651  birthdaylem3  20652  amgmlem  20688  amgm  20689  emcllem5  20698  fsumharmonic  20710  wilthlem1  20711  wilthlem2  20712  wilthlem3  20713  basellem1  20723  basellem2  20724  basellem3  20725  basellem4  20726  basellem5  20727  basellem8  20730  vmaprm  20760  sgmval2  20786  0sgm  20787  sgmf  20788  vma1  20809  dvdsdivcl  20826  fsumdvdsdiaglem  20828  dvdsflf1o  20832  muinv  20838  dvdsmulf1o  20839  sgmppw  20841  1sgmprm  20843  1sgm2ppw  20844  sgmmul  20845  chtublem  20855  fsumvma2  20858  chpchtsum  20863  logfaclbnd  20866  logexprlim  20869  mersenne  20871  perfect1  20872  perfectlem1  20873  perfectlem2  20874  perfect  20875  dchrsum2  20912  dchrhash  20915  bcmono  20921  bcp1ctr  20923  bclbnd  20924  bposlem1  20928  bposlem2  20929  bposlem3  20930  bposlem5  20932  bposlem6  20933  lgsval2lem  20950  lgsqrlem2  20986  lgseisenlem1  20993  lgseisenlem4  20996  lgsquadlem1  20998  lgsquadlem2  20999  lgsquadlem3  21000  lgsquad2  21004  m1lgs  21006  2sqlem3  21010  2sqlem4  21011  chebbnd1lem1  21023  chebbnd1  21026  rplogsumlem1  21038  rplogsumlem2  21039  rpvmasumlem  21041  dchrisumlem1  21043  dchrmusum2  21048  dchrvmasumlem1  21049  dchrvmasum2lem  21050  dchrvmasum2if  21051  dchrvmasumlem2  21052  dchrvmasumlem3  21053  dchrvmasumiflem1  21055  dchrisum0flblem1  21062  dchrisum0flblem2  21063  dchrisum0fno1  21065  rpvmasum2  21066  rplogsum  21081  mulogsumlem  21085  mulogsum  21086  mulog2sumlem2  21089  vmalogdivsum2  21092  vmalogdivsum  21093  2vmadivsumlem  21094  logsqvma  21096  selberglem2  21100  selberglem3  21101  selberg  21102  selberg2lem  21104  logdivbnd  21110  selberg3lem1  21111  selberg4lem1  21114  pntrsumo1  21119  pntrsumbnd2  21121  selberg3r  21123  selberg4r  21124  selberg34r  21125  pntsval2  21130  pntrlog2bndlem2  21132  pntrlog2bndlem4  21134  pntrlog2bndlem6  21137  pntpbnd1  21140  pntpbnd2  21141  pntlemg  21152  pntlemn  21154  pntlemf  21159  pnt  21168  padicabvf  21185  ostth2lem2  21188  ostth3  21192  eupares  21538  numdenneg  23991  ltesubnnd  23993  qqhnm  24166  ballotlemfc0  24522  ballotlemfcc  24523  zetacvg  24571  dmgmdivn0  24584  lgamgulmlem3  24587  lgamgulmlem4  24588  lgamgulmlem5  24589  lgamgulmlem6  24590  lgamgulm2  24592  lgamcvg2  24611  gamcvg  24612  gamcvg2lem  24615  facgam  24622  subfacp1lem1  24637  subfacp1lem5  24642  subfacval2  24645  subfaclim  24646  cvmliftlem2  24745  cvmliftlem7  24750  cvmliftlem10  24753  cvmliftlem11  24754  cvmliftlem13  24755  fprodfac  25068  risefacfac  25110  fallfacfac  25111  fallfacfwd  25112  faclimlem1  25113  faclimlem2  25114  faclim2  25118  bpolycl  25805  bpolysum  25806  bpolydiflem  25807  fsumkthpow  25809  nn0prpwlem  26009  nn0prpw  26010  irrapxlem4  26572  irrapxlem5  26573  pellexlem2  26577  pellexlem6  26581  pell1234qrne0  26600  pell1234qrreccl  26601  pell1234qrmulcl  26602  pell1234qrdich  26608  pell14qrdich  26616  pell1qrge1  26617  pell1qr1  26618  pell14qrgapw  26623  rmxyneg  26667  rmxm1  26681  rmxluc  26683  rmxdbl  26686  jm2.19lem1  26744  jm2.27c  26762  psgnunilem5  27079  phisum  27180  clim1fr1  27388  dvsinexp  27401  itgsinexplem1  27409  itgsinexp  27410  stoweidlem1  27411  stoweidlem11  27421  stoweidlem25  27435  stoweidlem26  27436  stoweidlem34  27444  stoweidlem37  27447  stoweidlem38  27448  stoweidlem42  27452  wallispi2lem1  27481  wallispi2  27483  stirlinglem4  27487  stirlinglem5  27488  stirlinglem10  27493  stirlinglem15  27498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-i2m1 8984  ax-1ne0 8985  ax-rrecex 8988  ax-cnre 8989
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-recs 6562  df-rdg 6597  df-nn 9926
  Copyright terms: Public domain W3C validator