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

Theorem 2cnd 10682
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 10680 . 2  |-  2  e.  CC
21a1i 11 1  |-  ( ph  ->  2  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   CCcc 9537   2c2 10659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293  df-2 10668
This theorem is referenced by:  cnm2m1cnm3  10864  zeo2  11022  flhalf  12062  2txmodxeq0  12150  binom3  12393  zesq  12395  expmulnbnd  12404  discr  12409  amgm2  13432  iseraltlem2  13749  iseralt  13751  trirecip  13921  geo2sum  13929  bpolydiflem  14107  ege2le3  14144  tanval3  14188  sinhval  14208  tanhlt1  14214  sqrt2irr  14301  oddm1even  14366  oddp1even  14367  bitsp1e  14405  bitsp1o  14406  bitsfzo  14409  bitsmod  14410  bitsinv1lem  14415  sadadd2lem2  14424  sadcaddlem  14431  bitsuz  14448  bitsshft  14449  prmdiv  14733  vfermltlALT  14753  iserodd  14785  4sqlem7  14888  4sqlem10  14891  4sqlem19  14913  prmgaplem7  15027  2expltfac  15063  efgredlemg  17392  frgpnabllem1  17509  metnrmlem3  21878  metnrmlem3OLD  21893  iihalf1cn  21960  iihalf2cn  21962  pcoass  22055  csbren  22353  trirn  22354  minveclem2  22368  minveclem2OLD  22380  ovolunlem1a  22449  uniioombllem5  22545  uniioombl  22547  dyaddisjlem  22553  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  dvsincos  22933  lhop1  22966  cosargd  23557  dvcnsqrt  23684  root1id  23694  ssscongptld  23751  chordthmlem  23758  chordthmlem2  23759  chordthmlem4  23761  heron  23764  dcubic1  23771  mcubic  23773  cubic2  23774  quartlem4  23786  quart  23787  cosasin  23830  cosatan  23847  atantayl  23863  atantayl2  23864  atantayl3  23865  log2tlbnd  23871  cxp2limlem  23901  divsqrtsumlem  23905  lgamgulmlem2  23955  lgamgulmlem4  23957  lgamucov  23963  ftalem2  23998  basellem2  24008  basellem3  24009  basellem5  24011  basellem8  24014  logfaclbnd  24150  perfectlem2  24158  perfect  24159  bcp1ctr  24207  bposlem1  24212  bposlem2  24213  lgslem1  24224  lgsqrlem2  24270  lgseisenlem1  24277  lgseisenlem2  24278  lgseisenlem3  24279  lgseisenlem4  24280  lgsquadlem1  24282  lgsquadlem2  24283  lgsquad2lem1  24286  chebbnd1lem3  24309  chto1ub  24314  dchrisumlem2  24328  dchrisum0flblem2  24347  dchrisum0fno1  24349  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2  24356  mulog2sumlem2  24373  vmalogdivsum2  24376  log2sumbnd  24382  selberglem2  24384  chpdifbndlem1  24391  selberg3lem1  24395  selberg3  24397  selberg4lem1  24398  selberg4  24399  selberg4r  24408  selberg34r  24409  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntrlog2bndlem6  24421  pntpbnd1a  24423  pntpbnd2  24425  pntibndlem2  24429  pntlemb  24435  pntlemg  24436  pntlemh  24437  pntlemr  24440  pntlemk  24444  pntlemo  24445  ostth2lem1  24456  wwlkextwrd  25456  wwlkextinj  25458  clwlkisclwwlklem2a1  25507  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem0  25516  clwwlkext2edg  25530  extwwlkfablem1  25802  extwwlkfablem2  25806  numclwwlkovf2ex  25814  numclwlk1lem2foa  25819  numclwlk1lem2fo  25823  numclwwlk2lem1  25830  numclwlk2lem2f  25831  numclwwlk2  25835  ex-ind-dvds  25899  archirngz  28506  archiabllem2c  28512  sqsscirc1  28714  dya2icoseg  29099  dya2iocucvr  29106  oddpwdc  29187  eulerpartlemgs2  29213  fibp1  29234  signslema  29451  subfacp1lem1  29902  subfacp1lem5  29907  itg2addnclem  31993  dvasin  32028  areacirclem1  32032  areacirclem3  32034  isbnd2  32115  rmxluc  35784  rmyluc2  35786  rmydbl  35788  jm2.18  35843  jm2.22  35850  jm2.25  35854  jm2.27c  35862  jm3.1lem2  35873  imo72b2lem0  36608  refsum2cnlem1  37358  oddfl  37487  xralrple2  37577  m1expevenOLD  37670  sumnnodd  37710  0ellimcdiv  37730  coseq0  37739  sinmulcos  37740  coskpi2  37741  sinaover2ne0  37743  cosknegpi  37744  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  itgsinexp  37831  stoweidlem1  37861  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem4  37930  wallispilem5  37931  wallispi  37932  wallispi2lem1  37933  wallispi2lem2  37934  wallispi2  37935  stirlinglem1  37936  stirlinglem3  37938  stirlinglem4  37939  stirlinglem5  37940  stirlinglem6  37941  stirlinglem7  37942  stirlinglem8  37943  stirlinglem10  37945  stirlinglem11  37946  stirlinglem13  37948  stirlinglem14  37949  stirlinglem15  37950  dirker2re  37954  dirkerdenne0  37955  dirkerval2  37956  dirkerre  37957  dirkertrigeqlem1  37960  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  dirkertrigeq  37963  dirkeritg  37964  dirkercncflem1  37965  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem43  38014  fourierdlem44  38015  fourierdlem56  38026  fourierdlem57  38027  fourierdlem58  38028  fourierdlem62  38032  fourierdlem66  38036  fourierdlem68  38038  fourierdlem72  38042  fourierdlem76  38046  fourierdlem79  38049  fourierdlem80  38050  fourierdlem83  38053  fourierdlem95  38065  fourierdlem104  38074  fourierdlem112  38082  fouriercnp  38090  fourierswlem  38094  sge0ad2en  38273  hoicvrrex  38378  hoiqssbllem2  38445  xp1d2m1eqxm1d2  38711  mod2eq1n2dvds  38725  elmod2OLD  38726  dfodd6  38767  dfeven4  38768  enege  38775  onego  38776  dfeven2  38779  oddflALTV  38792  opoeALTV  38812  opeoALTV  38813  nn0onn0exALTV  38827  nn0enn0exALTV  38828  perfectALTV  38845  proththd  38914  upgrspths1wlklem  39696  0nodd  39863  2nodd  39865  2zlidl  39987  2zrngamgm  39992  2zrngagrp  39996  2zrngmmgm  39999  2zrngnmlid  40002  nn0enne  40379  nn0onn0ex  40384  nn0enn0ex  40385  nnpw2even  40389  fldivexpfllog2  40429  blenpw2m1  40443  nnpw2blen  40444  blennn0em1  40455  dig2nn1st  40469  dig2bits  40478  dignn0flhalflem1  40479  dignn0flhalflem2  40480  dignn0ehalf  40481  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484
  Copyright terms: Public domain W3C validator