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

Theorem 2cnd 10671
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
2cnd  |-  ( ph  ->  2  e.  CC )

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 10669 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   CCcc 9526   2c2 10648
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-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-i2m1 9596  ax-1ne0 9597  ax-rrecex 9600  ax-cnre 9601
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299  df-2 10657
This theorem is referenced by:  cnm2m1cnm3  10853  zeo2  11011  flhalf  12048  2txmodxeq0  12136  binom3  12379  zesq  12381  expmulnbnd  12390  discr  12395  amgm2  13400  iseraltlem2  13716  iseralt  13718  trirecip  13888  geo2sum  13896  bpolydiflem  14074  ege2le3  14111  tanval3  14155  sinhval  14175  tanhlt1  14181  sqrt2irr  14268  oddm1even  14333  oddp1even  14334  bitsp1e  14369  bitsp1o  14370  bitsfzo  14372  bitsmod  14373  bitsinv1lem  14378  sadadd2lem2  14387  sadcaddlem  14394  bitsuz  14411  bitsshft  14412  prmdiv  14691  vfermltlALT  14705  iserodd  14737  4sqlem7  14840  4sqlem10  14843  4sqlem19  14865  prmgaplem7  14979  2expltfac  15015  efgredlemg  17320  frgpnabllem1  17437  metnrmlem3  21782  iihalf1cn  21849  iihalf2cn  21851  pcoass  21941  csbren  22239  trirn  22240  minveclem2  22254  ovolunlem1a  22323  uniioombllem5  22419  uniioombl  22421  dyaddisjlem  22427  mbfi1fseqlem5  22551  mbfi1fseqlem6  22552  dvsincos  22807  lhop1  22840  cosargd  23419  dvcnsqrt  23546  root1id  23556  ssscongptld  23613  chordthmlem  23620  chordthmlem2  23621  chordthmlem4  23623  heron  23626  dcubic1  23633  mcubic  23635  cubic2  23636  quartlem4  23648  quart  23649  cosasin  23692  cosatan  23709  atantayl  23725  atantayl2  23726  atantayl3  23727  log2tlbnd  23733  cxp2limlem  23763  divsqrtsumlem  23767  lgamgulmlem2  23817  lgamgulmlem4  23819  lgamucov  23825  ftalem2  23860  basellem2  23868  basellem3  23869  basellem5  23871  basellem8  23874  logfaclbnd  24010  perfectlem2  24018  perfect  24019  bcp1ctr  24067  bposlem1  24072  bposlem2  24073  lgslem1  24084  lgsqrlem2  24130  lgseisenlem1  24137  lgseisenlem2  24138  lgseisenlem3  24139  lgseisenlem4  24140  lgsquadlem1  24142  lgsquadlem2  24143  lgsquad2lem1  24146  chebbnd1lem3  24169  chto1ub  24174  dchrisumlem2  24188  dchrisum0flblem2  24207  dchrisum0fno1  24209  dchrisum0lem1b  24213  dchrisum0lem1  24214  dchrisum0lem2  24216  mulog2sumlem2  24233  vmalogdivsum2  24236  log2sumbnd  24242  selberglem2  24244  chpdifbndlem1  24251  selberg3lem1  24255  selberg3  24257  selberg4lem1  24258  selberg4  24259  selberg4r  24268  selberg34r  24269  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntrlog2bndlem6  24281  pntpbnd1a  24283  pntpbnd2  24285  pntibndlem2  24289  pntlemb  24295  pntlemg  24296  pntlemh  24297  pntlemr  24300  pntlemk  24304  pntlemo  24305  ostth2lem1  24316  wwlkextwrd  25298  wwlkextinj  25300  clwlkisclwwlklem2a1  25349  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem0  25358  clwwlkext2edg  25372  extwwlkfablem1  25644  extwwlkfablem2  25648  numclwwlkovf2ex  25656  numclwlk1lem2foa  25661  numclwlk1lem2fo  25665  numclwwlk2lem1  25672  numclwlk2lem2f  25673  numclwwlk2  25677  ex-ind-dvds  25741  archirngz  28341  archiabllem2c  28347  sqsscirc1  28550  dya2icoseg  28935  dya2iocucvr  28942  oddpwdc  29010  eulerpartlemgs2  29036  fibp1  29057  signslema  29236  subfacp1lem1  29687  subfacp1lem5  29692  itg2addnclem  31697  dvasin  31732  areacirclem1  31736  areacirclem3  31738  isbnd2  31819  rmxluc  35494  rmyluc2  35496  rmydbl  35498  jm2.18  35553  jm2.22  35560  jm2.25  35564  jm2.27c  35572  jm3.1lem2  35583  imo72b2lem0  36249  refsum2cnlem1  37002  oddfl  37100  m1expevenOLD  37246  sumnnodd  37286  0ellimcdiv  37306  coseq0  37315  sinmulcos  37316  coskpi2  37317  sinaover2ne0  37319  cosknegpi  37320  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  itgsinexp  37404  stoweidlem1  37434  stoweidlem62  37496  stoweidlem62OLD  37497  wallispilem4  37503  wallispilem5  37504  wallispi  37505  wallispi2lem1  37506  wallispi2lem2  37507  wallispi2  37508  stirlinglem1  37509  stirlinglem3  37511  stirlinglem4  37512  stirlinglem5  37513  stirlinglem6  37514  stirlinglem7  37515  stirlinglem8  37516  stirlinglem10  37518  stirlinglem11  37519  stirlinglem13  37521  stirlinglem14  37522  stirlinglem15  37523  dirker2re  37527  dirkerdenne0  37528  dirkerval2  37529  dirkerre  37530  dirkertrigeqlem1  37533  dirkertrigeqlem2  37534  dirkertrigeqlem3  37535  dirkertrigeq  37536  dirkeritg  37537  dirkercncflem1  37538  dirkercncflem2  37539  dirkercncflem4  37541  fourierdlem43  37585  fourierdlem44  37586  fourierdlem56  37598  fourierdlem57  37599  fourierdlem58  37600  fourierdlem62  37604  fourierdlem66  37608  fourierdlem68  37610  fourierdlem72  37614  fourierdlem76  37618  fourierdlem79  37621  fourierdlem80  37622  fourierdlem83  37625  fourierdlem95  37637  fourierdlem104  37646  fourierdlem112  37654  fouriercnp  37662  fourierswlem  37666  xp1d2m1eqxm1d2  38114  mod2eq1n2dvds  38128  elmod2OLD  38129  dfodd6  38170  dfeven4  38171  enege  38178  onego  38179  dfeven2  38182  oddflALTV  38195  opoeALTV  38215  opeoALTV  38216  nn0onn0exALTV  38230  nn0enn0exALTV  38231  perfectALTV  38248  proththd  38317  0nodd  38581  2nodd  38583  2zlidl  38705  2zrngamgm  38710  2zrngagrp  38714  2zrngmmgm  38717  2zrngnmlid  38720  nn0enne  39100  nn0onn0ex  39105  nn0enn0ex  39106  nnpw2even  39110  fldivexpfllog2  39150  blenpw2m1  39164  nnpw2blen  39165  blennn0em1  39176  dig2nn1st  39190  dig2bits  39199  dignn0flhalflem1  39200  dignn0flhalflem2  39201  dignn0ehalf  39202  nn0sumshdiglemA  39204  nn0sumshdiglemB  39205
  Copyright terms: Public domain W3C validator