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

Theorem 2cnd 10386
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 10384 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9272   2c2 10363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-ov 6089  df-2 10372
This theorem is referenced by:  zeo2  10720  flhalf  11666  2txmodxeq0  11751  zesq  11979  expmulnbnd  11988  discr  11993  amgm2  12849  iseraltlem2  13152  iseralt  13154  trirecip  13317  geo2sum  13325  ege2le3  13367  tanval3  13410  sinhval  13430  tanhlt1  13436  sqr2irr  13523  oddm1even  13585  oddp1even  13586  bitsp1e  13620  bitsp1o  13621  bitsfzo  13623  bitsmod  13624  bitsinv1lem  13629  sadadd2lem2  13638  sadcaddlem  13645  bitsuz  13662  bitsshft  13663  prmdiv  13852  4sqlem7  13997  4sqlem10  14000  4sqlem19  14016  2expltfac  14111  efgredlemg  16228  frgpnabllem1  16340  metnrmlem3  20406  iihalf1cn  20473  iihalf2cn  20475  pcoass  20565  csbren  20867  trirn  20868  minveclem2  20882  ovolunlem1a  20948  uniioombllem5  21036  uniioombl  21038  dyaddisjlem  21044  mbfi1fseqlem5  21166  mbfi1fseqlem6  21167  dvsincos  21422  lhop1  21455  cosargd  22026  root1id  22161  ssscongptld  22189  chordthmlem  22196  chordthmlem2  22197  chordthmlem4  22199  heron  22202  dcubic1  22209  mcubic  22211  cubic2  22212  quartlem4  22224  quart  22225  cosasin  22268  cosatan  22285  atantayl  22301  atantayl2  22302  atantayl3  22303  log2tlbnd  22309  cxp2limlem  22338  divsqrsumlem  22342  ftalem2  22380  basellem2  22388  basellem3  22389  basellem5  22391  logfaclbnd  22530  perfect  22539  bcp1ctr  22587  bposlem1  22592  bposlem2  22593  lgslem1  22604  lgsqrlem2  22650  lgseisenlem1  22657  lgseisenlem2  22658  lgseisenlem3  22659  lgseisenlem4  22660  lgsquadlem1  22662  lgsquadlem2  22663  lgsquad2lem1  22666  chebbnd1lem3  22689  chto1ub  22694  dchrisumlem2  22708  dchrisum0flblem2  22727  dchrisum0fno1  22729  dchrisum0lem1b  22733  dchrisum0lem1  22734  dchrisum0lem2  22736  mulog2sumlem2  22753  vmalogdivsum2  22756  log2sumbnd  22762  selberglem2  22764  chpdifbndlem1  22771  selberg3lem1  22775  selberg3  22777  selberg4lem1  22778  selberg4  22779  selberg4r  22788  selberg34r  22789  pntrlog2bndlem3  22797  pntrlog2bndlem4  22798  pntrlog2bndlem5  22799  pntrlog2bndlem6  22801  pntpbnd1a  22803  pntpbnd2  22805  pntibndlem2  22809  pntlemb  22815  pntlemg  22816  pntlemh  22817  pntlemr  22820  pntlemk  22824  pntlemo  22825  ostth2lem1  22836  archirngz  26151  archiabllem2c  26157  sqsscirc1  26286  dya2icoseg  26640  dya2iocucvr  26647  oddpwdc  26685  eulerpartlemgs2  26711  fibp1  26732  signslema  26911  lgamgulmlem2  26964  lgamgulmlem4  26966  lgamucov  26972  subfacp1lem1  27015  subfacp1lem5  27020  bpolydiflem  28144  itg2addnclem  28386  dvcnsqr  28421  dvasin  28423  areacirclem1  28427  areacirclem3  28429  isbnd2  28625  rmxluc  29220  rmyluc2  29222  rmydbl  29224  jm2.18  29280  jm2.22  29287  jm2.25  29291  jm2.27c  29299  jm3.1lem2  29310  refsum2cnlem1  29702  m1expeven  29715  itgsinexp  29738  stoweidlem1  29739  stoweidlem62  29800  wallispilem4  29806  wallispilem5  29807  wallispi  29808  wallispi2lem1  29809  wallispi2  29811  stirlinglem1  29812  stirlinglem3  29814  stirlinglem4  29815  stirlinglem5  29816  stirlinglem6  29817  stirlinglem7  29818  stirlinglem8  29819  stirlinglem10  29821  stirlinglem11  29822  stirlinglem13  29824  stirlinglem14  29825  stirlinglem15  29826  cnm2m1cnm3  30122  wwlkextwrd  30303  wwlkextinj  30305  clwlkisclwwlklem2a1  30384  clwlkisclwwlklem2a4  30389  clwlkisclwwlklem0  30393  clwwlkext2edg  30407  extwwlkfablem1  30610  extwwlkfablem2  30614  numclwwlkovf2ex  30622  numclwlk1lem2foa  30627  numclwlk1lem2fo  30631  numclwwlk2lem1  30638  numclwlk2lem2f  30639  numclwwlk2  30643
  Copyright terms: Public domain W3C validator