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

Theorem 2cnd 10597
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 10595 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   CCcc 9479   2c2 10574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-2 10583
This theorem is referenced by:  cnm2m1cnm3  10779  zeo2  10936  flhalf  11918  2txmodxeq0  12003  zesq  12244  expmulnbnd  12253  discr  12258  amgm2  13151  iseraltlem2  13454  iseralt  13456  trirecip  13626  geo2sum  13634  ege2le3  13676  tanval3  13719  sinhval  13739  tanhlt1  13745  sqr2irr  13832  oddm1even  13895  oddp1even  13896  bitsp1e  13930  bitsp1o  13931  bitsfzo  13933  bitsmod  13934  bitsinv1lem  13939  sadadd2lem2  13948  sadcaddlem  13955  bitsuz  13972  bitsshft  13973  prmdiv  14163  4sqlem7  14310  4sqlem10  14313  4sqlem19  14329  2expltfac  14424  efgredlemg  16549  frgpnabllem1  16661  metnrmlem3  21093  iihalf1cn  21160  iihalf2cn  21162  pcoass  21252  csbren  21554  trirn  21555  minveclem2  21569  ovolunlem1a  21635  uniioombllem5  21724  uniioombl  21726  dyaddisjlem  21732  mbfi1fseqlem5  21854  mbfi1fseqlem6  21855  dvsincos  22110  lhop1  22143  cosargd  22714  root1id  22849  ssscongptld  22877  chordthmlem  22884  chordthmlem2  22885  chordthmlem4  22887  heron  22890  dcubic1  22897  mcubic  22899  cubic2  22900  quartlem4  22912  quart  22913  cosasin  22956  cosatan  22973  atantayl  22989  atantayl2  22990  atantayl3  22991  log2tlbnd  22997  cxp2limlem  23026  divsqrsumlem  23030  ftalem2  23068  basellem2  23076  basellem3  23077  basellem5  23079  logfaclbnd  23218  perfect  23227  bcp1ctr  23275  bposlem1  23280  bposlem2  23281  lgslem1  23292  lgsqrlem2  23338  lgseisenlem1  23345  lgseisenlem2  23346  lgseisenlem3  23347  lgseisenlem4  23348  lgsquadlem1  23350  lgsquadlem2  23351  lgsquad2lem1  23354  chebbnd1lem3  23377  chto1ub  23382  dchrisumlem2  23396  dchrisum0flblem2  23415  dchrisum0fno1  23417  dchrisum0lem1b  23421  dchrisum0lem1  23422  dchrisum0lem2  23424  mulog2sumlem2  23441  vmalogdivsum2  23444  log2sumbnd  23450  selberglem2  23452  chpdifbndlem1  23459  selberg3lem1  23463  selberg3  23465  selberg4lem1  23466  selberg4  23467  selberg4r  23476  selberg34r  23477  pntrlog2bndlem3  23485  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  pntrlog2bndlem6  23489  pntpbnd1a  23491  pntpbnd2  23493  pntibndlem2  23497  pntlemb  23503  pntlemg  23504  pntlemh  23505  pntlemr  23508  pntlemk  23512  pntlemo  23513  ostth2lem1  23524  wwlkextwrd  24390  wwlkextinj  24392  clwlkisclwwlklem2a1  24441  clwlkisclwwlklem2a4  24446  clwlkisclwwlklem0  24450  clwwlkext2edg  24464  extwwlkfablem1  24737  extwwlkfablem2  24741  numclwwlkovf2ex  24749  numclwlk1lem2foa  24754  numclwlk1lem2fo  24758  numclwwlk2lem1  24765  numclwlk2lem2f  24766  numclwwlk2  24770  archirngz  27381  archiabllem2c  27387  sqsscirc1  27512  dya2icoseg  27874  dya2iocucvr  27881  oddpwdc  27919  eulerpartlemgs2  27945  fibp1  27966  signslema  28145  lgamgulmlem2  28198  lgamgulmlem4  28200  lgamucov  28206  subfacp1lem1  28249  subfacp1lem5  28254  bpolydiflem  29379  itg2addnclem  29630  dvcnsqr  29665  dvasin  29667  areacirclem1  29671  areacirclem3  29673  isbnd2  29869  rmxluc  30463  rmyluc2  30465  rmydbl  30467  jm2.18  30523  jm2.22  30530  jm2.25  30534  jm2.27c  30542  jm3.1lem2  30553  refsum2cnlem1  30945  m1expeven  31096  sumnnodd  31127  coskpi2  31157  cosknegpi  31160  ioodvbdlimc1lem2  31217  ioodvbdlimc2lem  31219  itgsinexp  31227  stoweidlem1  31256  stoweidlem62  31317  wallispilem4  31323  wallispilem5  31324  wallispi  31325  wallispi2lem1  31326  wallispi2  31328  stirlinglem1  31329  stirlinglem3  31331  stirlinglem4  31332  stirlinglem5  31333  stirlinglem6  31334  stirlinglem7  31335  stirlinglem8  31336  stirlinglem10  31338  stirlinglem11  31339  stirlinglem13  31341  stirlinglem14  31342  stirlinglem15  31343  fouriercnp  31482  fourierswlem  31486
  Copyright terms: Public domain W3C validator