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

Theorem 2cnd 10397
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 10395 . 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 9283   2c2 10374
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 2423  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rrecex 9357  ax-cnre 9358
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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-ov 6097  df-2 10383
This theorem is referenced by:  zeo2  10731  flhalf  11677  2txmodxeq0  11762  zesq  11990  expmulnbnd  11999  discr  12004  amgm2  12860  iseraltlem2  13163  iseralt  13165  trirecip  13328  geo2sum  13336  ege2le3  13378  tanval3  13421  sinhval  13441  tanhlt1  13447  sqr2irr  13534  oddm1even  13596  oddp1even  13597  bitsp1e  13631  bitsp1o  13632  bitsfzo  13634  bitsmod  13635  bitsinv1lem  13640  sadadd2lem2  13649  sadcaddlem  13656  bitsuz  13673  bitsshft  13674  prmdiv  13863  4sqlem7  14008  4sqlem10  14011  4sqlem19  14027  2expltfac  14122  efgredlemg  16242  frgpnabllem1  16354  metnrmlem3  20440  iihalf1cn  20507  iihalf2cn  20509  pcoass  20599  csbren  20901  trirn  20902  minveclem2  20916  ovolunlem1a  20982  uniioombllem5  21070  uniioombl  21072  dyaddisjlem  21078  mbfi1fseqlem5  21200  mbfi1fseqlem6  21201  dvsincos  21456  lhop1  21489  cosargd  22060  root1id  22195  ssscongptld  22223  chordthmlem  22230  chordthmlem2  22231  chordthmlem4  22233  heron  22236  dcubic1  22243  mcubic  22245  cubic2  22246  quartlem4  22258  quart  22259  cosasin  22302  cosatan  22319  atantayl  22335  atantayl2  22336  atantayl3  22337  log2tlbnd  22343  cxp2limlem  22372  divsqrsumlem  22376  ftalem2  22414  basellem2  22422  basellem3  22423  basellem5  22425  logfaclbnd  22564  perfect  22573  bcp1ctr  22621  bposlem1  22626  bposlem2  22627  lgslem1  22638  lgsqrlem2  22684  lgseisenlem1  22691  lgseisenlem2  22692  lgseisenlem3  22693  lgseisenlem4  22694  lgsquadlem1  22696  lgsquadlem2  22697  lgsquad2lem1  22700  chebbnd1lem3  22723  chto1ub  22728  dchrisumlem2  22742  dchrisum0flblem2  22761  dchrisum0fno1  22763  dchrisum0lem1b  22767  dchrisum0lem1  22768  dchrisum0lem2  22770  mulog2sumlem2  22787  vmalogdivsum2  22790  log2sumbnd  22796  selberglem2  22798  chpdifbndlem1  22805  selberg3lem1  22809  selberg3  22811  selberg4lem1  22812  selberg4  22813  selberg4r  22822  selberg34r  22823  pntrlog2bndlem3  22831  pntrlog2bndlem4  22832  pntrlog2bndlem5  22833  pntrlog2bndlem6  22835  pntpbnd1a  22837  pntpbnd2  22839  pntibndlem2  22843  pntlemb  22849  pntlemg  22850  pntlemh  22851  pntlemr  22854  pntlemk  22858  pntlemo  22859  ostth2lem1  22870  archirngz  26209  archiabllem2c  26215  sqsscirc1  26341  dya2icoseg  26695  dya2iocucvr  26702  oddpwdc  26740  eulerpartlemgs2  26766  fibp1  26787  signslema  26966  lgamgulmlem2  27019  lgamgulmlem4  27021  lgamucov  27027  subfacp1lem1  27070  subfacp1lem5  27075  bpolydiflem  28200  itg2addnclem  28446  dvcnsqr  28481  dvasin  28483  areacirclem1  28487  areacirclem3  28489  isbnd2  28685  rmxluc  29280  rmyluc2  29282  rmydbl  29284  jm2.18  29340  jm2.22  29347  jm2.25  29351  jm2.27c  29359  jm3.1lem2  29370  refsum2cnlem1  29762  m1expeven  29775  itgsinexp  29798  stoweidlem1  29799  stoweidlem62  29860  wallispilem4  29866  wallispilem5  29867  wallispi  29868  wallispi2lem1  29869  wallispi2  29871  stirlinglem1  29872  stirlinglem3  29874  stirlinglem4  29875  stirlinglem5  29876  stirlinglem6  29877  stirlinglem7  29878  stirlinglem8  29879  stirlinglem10  29881  stirlinglem11  29882  stirlinglem13  29884  stirlinglem14  29885  stirlinglem15  29886  cnm2m1cnm3  30182  wwlkextwrd  30363  wwlkextinj  30365  clwlkisclwwlklem2a1  30444  clwlkisclwwlklem2a4  30449  clwlkisclwwlklem0  30453  clwwlkext2edg  30467  extwwlkfablem1  30670  extwwlkfablem2  30674  numclwwlkovf2ex  30682  numclwlk1lem2foa  30687  numclwlk1lem2fo  30691  numclwwlk2lem1  30698  numclwlk2lem2f  30699  numclwwlk2  30703
  Copyright terms: Public domain W3C validator