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

Theorem 2cnd 10604
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 10602 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CCcc 9479   2c2 10581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  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 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-2 10590
This theorem is referenced by:  cnm2m1cnm3  10786  zeo2  10945  flhalf  11944  2txmodxeq0  12029  binom3  12269  zesq  12271  expmulnbnd  12280  discr  12285  amgm2  13284  iseraltlem2  13587  iseralt  13589  trirecip  13756  geo2sum  13764  ege2le3  13907  tanval3  13951  sinhval  13971  tanhlt1  13977  sqrt2irr  14066  oddm1even  14131  oddp1even  14132  bitsp1e  14166  bitsp1o  14167  bitsfzo  14169  bitsmod  14170  bitsinv1lem  14175  sadadd2lem2  14184  sadcaddlem  14191  bitsuz  14208  bitsshft  14209  prmdiv  14399  iserodd  14443  4sqlem7  14546  4sqlem10  14549  4sqlem19  14565  2expltfac  14661  efgredlemg  16959  frgpnabllem1  17076  metnrmlem3  21531  iihalf1cn  21598  iihalf2cn  21600  pcoass  21690  csbren  21992  trirn  21993  minveclem2  22007  ovolunlem1a  22073  uniioombllem5  22162  uniioombl  22164  dyaddisjlem  22170  mbfi1fseqlem5  22292  mbfi1fseqlem6  22293  dvsincos  22548  lhop1  22581  cosargd  23161  root1id  23296  ssscongptld  23353  chordthmlem  23360  chordthmlem2  23361  chordthmlem4  23363  heron  23366  dcubic1  23373  mcubic  23375  cubic2  23376  quartlem4  23388  quart  23389  cosasin  23432  cosatan  23449  atantayl  23465  atantayl2  23466  atantayl3  23467  log2tlbnd  23473  cxp2limlem  23503  divsqrtsumlem  23507  ftalem2  23545  basellem2  23553  basellem3  23554  basellem5  23556  basellem8  23559  logfaclbnd  23695  perfect  23704  bcp1ctr  23752  bposlem1  23757  bposlem2  23758  lgslem1  23769  lgsqrlem2  23815  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgseisenlem4  23825  lgsquadlem1  23827  lgsquadlem2  23828  lgsquad2lem1  23831  chebbnd1lem3  23854  chto1ub  23859  dchrisumlem2  23873  dchrisum0flblem2  23892  dchrisum0fno1  23894  dchrisum0lem1b  23898  dchrisum0lem1  23899  dchrisum0lem2  23901  mulog2sumlem2  23918  vmalogdivsum2  23921  log2sumbnd  23927  selberglem2  23929  chpdifbndlem1  23936  selberg3lem1  23940  selberg3  23942  selberg4lem1  23943  selberg4  23944  selberg4r  23953  selberg34r  23954  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntrlog2bndlem6  23966  pntpbnd1a  23968  pntpbnd2  23970  pntibndlem2  23974  pntlemb  23980  pntlemg  23981  pntlemh  23982  pntlemr  23985  pntlemk  23989  pntlemo  23990  ostth2lem1  24001  wwlkextwrd  24930  wwlkextinj  24932  clwlkisclwwlklem2a1  24981  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem0  24990  clwwlkext2edg  25004  extwwlkfablem1  25276  extwwlkfablem2  25280  numclwwlkovf2ex  25288  numclwlk1lem2foa  25293  numclwlk1lem2fo  25297  numclwwlk2lem1  25304  numclwlk2lem2f  25305  numclwwlk2  25309  ex-ind-dvds  25372  archirngz  27967  archiabllem2c  27973  sqsscirc1  28125  dya2icoseg  28485  dya2iocucvr  28492  oddpwdc  28557  eulerpartlemgs2  28583  fibp1  28604  signslema  28783  lgamgulmlem2  28836  lgamgulmlem4  28838  lgamucov  28844  subfacp1lem1  28887  subfacp1lem5  28892  bpolydiflem  30044  itg2addnclem  30306  dvcnsqrt  30341  dvasin  30343  areacirclem1  30347  areacirclem3  30349  isbnd2  30519  rmxluc  31111  rmyluc2  31113  rmydbl  31115  jm2.18  31169  jm2.22  31176  jm2.25  31180  jm2.27c  31188  jm3.1lem2  31199  refsum2cnlem1  31652  oddfl  31699  m1expeven  31824  sumnnodd  31875  0ellimcdiv  31894  coseq0  31903  sinmulcos  31904  coskpi2  31905  sinaover2ne0  31907  cosknegpi  31908  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  itgsinexp  31992  stoweidlem1  32022  stoweidlem62  32083  wallispilem4  32089  wallispilem5  32090  wallispi  32091  wallispi2lem1  32092  wallispi2lem2  32093  wallispi2  32094  stirlinglem1  32095  stirlinglem3  32097  stirlinglem4  32098  stirlinglem5  32099  stirlinglem6  32100  stirlinglem7  32101  stirlinglem8  32102  stirlinglem10  32104  stirlinglem11  32105  stirlinglem13  32107  stirlinglem14  32108  stirlinglem15  32109  dirker2re  32113  dirkerdenne0  32114  dirkerval2  32115  dirkerre  32116  dirkertrigeqlem1  32119  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkertrigeq  32122  dirkeritg  32123  dirkercncflem1  32124  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem43  32171  fourierdlem44  32172  fourierdlem56  32184  fourierdlem57  32185  fourierdlem58  32186  fourierdlem62  32190  fourierdlem66  32194  fourierdlem68  32196  fourierdlem72  32200  fourierdlem76  32204  fourierdlem79  32207  fourierdlem80  32208  fourierdlem83  32211  fourierdlem95  32223  fourierdlem104  32232  fourierdlem112  32240  fouriercnp  32248  fourierswlem  32252  xp1d2m1eqxm1d2  32532  mod2eq1n2dvds  32534  elmod2  32535  dfodd6  32552  dfeven4  32553  enege  32559  onego  32560  dfeven2  32561  oddflALTV  32574  opoeALTV  32589  opeoALTV  32590  nn0onn0exALTV  32604  nn0enn0exALTV  32605  0nodd  32870  2nodd  32872  2zlidl  32994  2zrngamgm  32999  2zrngagrp  33003  2zrngmmgm  33006  2zrngnmlid  33009  nn0enne  33390  nn0onn0ex  33395  nn0enn0ex  33396  nnpw2even  33400  fldivexpfllog2  33440  blenpw2m1  33454  nnpw2blen  33455  blennn0em1  33466  dig2nn1st  33480  dig2bits  33489  dignn0flhalflem1  33490  dignn0flhalflem2  33491  dignn0ehalf  33492  nn0sumshdiglemA  33494  nn0sumshdiglemB  33495  imo72b2lem0  38434
  Copyright terms: Public domain W3C validator