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

Theorem nncnd 10006
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 9995 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3338 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8978   NNcn 9990
This theorem is referenced by:  facdiv  11568  facndiv  11569  faclbnd  11571  faclbnd5  11579  faclbnd6  11580  facubnd  11581  facavg  11582  bccmpl  11590  bcn0  11591  bcn1  11594  bcm1k  11596  bcp1n  11597  bcp1nk  11598  bcval5  11599  bcpasc  11602  permnn  11607  hashf1  11696  hashfac  11697  wrdeqcats1  11778  binom11  12601  binom1dif  12602  climcndslem2  12620  arisum2  12630  trireciplem  12631  trirecip  12632  geo2sum  12640  geo2lim  12642  eftcl  12666  eftabs  12668  efcllem  12670  ege2le3  12682  efcj  12684  efaddlem  12685  eftlub  12700  eirrlem  12793  sqr2irrlem  12837  oexpneg  12901  bitsp1  12933  bitsfzolem  12936  bitsfzo  12937  bitsmod  12938  bitscmp  12940  bitsinv1lem  12943  bitsinv1  12944  2ebits  12949  bitsinvp1  12951  sadcaddlem  12959  sadadd3  12963  bitsres  12975  bitsuz  12976  bitsshft  12977  mulgcd  13036  rplpwr  13046  sqgcd  13048  prmind2  13080  isprm5  13102  prmdvdsexpr  13106  divgcdodd  13109  qmuldeneqnum  13129  divnumden  13130  qnumgt0  13132  numdensq  13136  hashdvds  13154  phiprmpw  13155  prmdiv  13164  prmdivdiv  13166  pythagtriplem4  13183  pythagtriplem6  13185  pythagtriplem7  13186  pythagtriplem14  13192  pythagtriplem15  13193  pythagtriplem19  13197  pythagtrip  13198  pcprendvds2  13205  pcpre1  13206  pcpremul  13207  pceulem  13209  pcdiv  13216  pcqmul  13217  pcelnn  13233  pcid  13236  pc2dvds  13242  pcaddlem  13247  pcadd  13248  pcfaclem  13257  qexpz  13260  expnprm  13261  prmpwdvds  13262  pockthlem  13263  pockthg  13264  infpnlem1  13268  prmreclem1  13274  prmreclem2  13275  prmreclem3  13276  prmreclem4  13277  prmreclem6  13279  4sqlem6  13301  4sqlem7  13302  4sqlem10  13305  mul4sqlem  13311  4sqlem11  13313  4sqlem12  13314  4sqlem14  13316  4sqlem17  13319  4sqlem18  13320  vdwlem1  13339  vdwlem2  13340  vdwlem3  13341  vdwlem5  13343  vdwlem6  13344  vdwlem8  13346  vdwlem9  13347  vdwlem10  13348  vdwlem12  13350  ramub1lem2  13385  ramcl  13387  gsumccat  14777  mulgnndir  14902  mulgnnass  14908  odf1o2  15197  pgp0  15220  sylow1lem1  15222  odcau  15228  sylow2blem3  15246  sylow3lem3  15253  sylow3lem4  15254  gexexlem  15457  ablfacrp2  15615  ablfac1lem  15616  ablfac1eu  15621  pgpfac1lem3a  15624  pgpfac1lem3  15625  zlpirlem3  16760  znrrg  16836  lebnumlem3  18978  ovollb2lem  19374  ovolunlem1a  19382  ovolunlem1  19383  uniioombllem3  19467  uniioombllem4  19468  dyaddisjlem  19477  mbfi1fseqlem3  19599  mbfi1fseqlem4  19600  dgrcolem1  20181  vieta1lem1  20217  vieta1lem2  20218  elqaalem2  20227  elqaalem3  20228  aalioulem1  20239  aaliou3lem2  20250  aaliou3lem8  20252  aaliou3lem6  20255  aaliou3lem9  20257  taylfvallem1  20263  tayl0  20268  taylply2  20274  taylply  20275  dvtaylp  20276  taylthlem1  20279  taylthlem2  20280  pserdvlem2  20334  advlogexp  20536  cxpmul2  20570  cxpeq  20631  atantayl3  20769  leibpi  20772  log2cnv  20774  log2tlbnd  20775  birthdaylem2  20781  birthdaylem3  20782  amgmlem  20818  amgm  20819  emcllem5  20828  fsumharmonic  20840  wilthlem1  20841  wilthlem2  20842  wilthlem3  20843  basellem1  20853  basellem2  20854  basellem3  20855  basellem4  20856  basellem5  20857  basellem8  20860  vmaprm  20890  sgmval2  20916  0sgm  20917  sgmf  20918  vma1  20939  dvdsdivcl  20956  fsumdvdsdiaglem  20958  dvdsflf1o  20962  muinv  20968  dvdsmulf1o  20969  sgmppw  20971  1sgmprm  20973  1sgm2ppw  20974  sgmmul  20975  chtublem  20985  fsumvma2  20988  chpchtsum  20993  logfaclbnd  20996  logexprlim  20999  mersenne  21001  perfect1  21002  perfectlem1  21003  perfectlem2  21004  perfect  21005  dchrsum2  21042  dchrhash  21045  bcmono  21051  bcp1ctr  21053  bclbnd  21054  bposlem1  21058  bposlem2  21059  bposlem3  21060  bposlem5  21062  bposlem6  21063  lgsval2lem  21080  lgsqrlem2  21116  lgseisenlem1  21123  lgseisenlem4  21126  lgsquadlem1  21128  lgsquadlem2  21129  lgsquadlem3  21130  lgsquad2  21134  m1lgs  21136  2sqlem3  21140  2sqlem4  21141  chebbnd1lem1  21153  chebbnd1  21156  rplogsumlem1  21168  rplogsumlem2  21169  rpvmasumlem  21171  dchrisumlem1  21173  dchrmusum2  21178  dchrvmasumlem1  21179  dchrvmasum2lem  21180  dchrvmasum2if  21181  dchrvmasumlem2  21182  dchrvmasumlem3  21183  dchrvmasumiflem1  21185  dchrisum0flblem1  21192  dchrisum0flblem2  21193  dchrisum0fno1  21195  rpvmasum2  21196  rplogsum  21211  mulogsumlem  21215  mulogsum  21216  mulog2sumlem2  21219  vmalogdivsum2  21222  vmalogdivsum  21223  2vmadivsumlem  21224  logsqvma  21226  selberglem2  21230  selberglem3  21231  selberg  21232  selberg2lem  21234  logdivbnd  21240  selberg3lem1  21241  selberg4lem1  21244  pntrsumo1  21249  pntrsumbnd2  21251  selberg3r  21253  selberg4r  21254  selberg34r  21255  pntsval2  21260  pntrlog2bndlem2  21262  pntrlog2bndlem4  21264  pntrlog2bndlem6  21267  pntpbnd1  21270  pntpbnd2  21271  pntlemg  21282  pntlemn  21284  pntlemf  21289  pnt  21298  padicabvf  21315  ostth2lem2  21318  ostth3  21322  eupares  21687  numdenneg  24150  ltesubnnd  24152  qqhnm  24364  ballotlemfc0  24740  ballotlemfcc  24741  zetacvg  24789  dmgmdivn0  24802  lgamgulmlem3  24805  lgamgulmlem4  24806  lgamgulmlem5  24807  lgamgulmlem6  24808  lgamgulm2  24810  lgamcvg2  24829  gamcvg  24830  gamcvg2lem  24833  facgam  24840  subfacp1lem1  24855  subfacp1lem5  24860  subfacval2  24863  subfaclim  24864  cvmliftlem2  24963  cvmliftlem7  24968  cvmliftlem10  24971  cvmliftlem11  24972  cvmliftlem13  24973  fprodfac  25286  iprodgam  25309  risefacfac  25341  fallfacfwd  25342  fallfacval4  25349  bcfallfac  25350  fallfacfac  25351  faclimlem1  25352  faclimlem2  25353  faclim2  25357  bpolycl  26063  bpolysum  26064  bpolydiflem  26065  fsumkthpow  26067  mblfinlem  26207  nn0prpwlem  26279  nn0prpw  26280  irrapxlem4  26842  irrapxlem5  26843  pellexlem2  26847  pellexlem6  26851  pell1234qrne0  26870  pell1234qrreccl  26871  pell1234qrmulcl  26872  pell1234qrdich  26878  pell14qrdich  26886  pell1qrge1  26887  pell1qr1  26888  pell14qrgapw  26893  rmxyneg  26937  rmxm1  26951  rmxluc  26953  rmxdbl  26956  jm2.19lem1  27014  jm2.27c  27032  psgnunilem5  27349  phisum  27450  clim1fr1  27658  dvsinexp  27671  itgsinexplem1  27679  itgsinexp  27680  stoweidlem1  27681  stoweidlem11  27691  stoweidlem25  27705  stoweidlem26  27706  stoweidlem34  27714  stoweidlem37  27717  stoweidlem38  27718  stoweidlem42  27722  wallispi2lem1  27751  wallispi2  27753  stirlinglem4  27757  stirlinglem5  27758  stirlinglem10  27763  stirlinglem15  27768  modprm0  28158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-i2m1 9048  ax-1ne0 9049  ax-rrecex 9052  ax-cnre 9053
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-recs 6625  df-rdg 6660  df-nn 9991
  Copyright terms: Public domain W3C validator