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

Theorem 2cnd 10940
Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
2cnd (𝜑 → 2 ∈ ℂ)

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 10938 . 2 2 ∈ ℂ
21a1i 11 1 (𝜑 → 2 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9790  2c2 10917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926
This theorem is referenced by:  subhalfhalf  11113  cnm2m1cnm3  11132  xp1d2m1eqxm1d2  11133  zeo2  11296  2tnp1ge0ge0  12447  flhalf  12448  2txmodxeq0  12547  mulbinom2  12801  binom3  12802  zesq  12804  expmulnbnd  12813  discr  12818  sqoddm1div8  12845  mulsubdivbinom2  12863  amgm2  13903  iseraltlem2  14207  iseralt  14209  trirecip  14380  geo2sum  14389  bpolydiflem  14570  ege2le3  14605  tanval3  14649  sinhval  14669  tanhlt1  14675  sqrt2irr  14763  even2n  14850  oddm1even  14851  oddp1even  14852  mod2eq1n2dvds  14855  ltoddhalfle  14869  m1exp1  14877  nn0enne  14878  flodddiv4  14921  flodddiv4t2lthalf  14924  bitsp1e  14938  bitsp1o  14939  bitsfzo  14941  bitsmod  14942  bitsinv1lem  14947  sadadd2lem2  14956  sadcaddlem  14963  bitsuz  14980  bitsshft  14981  prmdiv  15274  vfermltlALT  15291  iserodd  15324  4sqlem7  15432  4sqlem10  15435  4sqlem19  15451  prmgaplem7  15545  2expltfac  15583  efgredlemg  17924  frgpnabllem1  18045  metnrmlem3  22403  iihalf1cn  22470  iihalf2cn  22472  pcoass  22563  csbren  22907  trirn  22908  minveclem2  22922  ovolunlem1a  22988  uniioombllem5  23078  uniioombl  23080  dyaddisjlem  23086  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  dvsincos  23465  lhop1  23498  cosargd  24075  dvcnsqrt  24202  root1id  24212  ssscongptld  24269  chordthmlem  24276  chordthmlem2  24277  chordthmlem4  24279  heron  24282  dcubic1  24289  mcubic  24291  cubic2  24292  quartlem4  24304  quart  24305  cosasin  24348  cosatan  24365  atantayl  24381  atantayl2  24382  atantayl3  24383  log2tlbnd  24389  cxp2limlem  24419  divsqrtsumlem  24423  lgamgulmlem2  24473  lgamgulmlem4  24475  lgamucov  24481  ftalem2  24517  basellem2  24525  basellem3  24526  basellem5  24528  basellem8  24531  logfaclbnd  24664  perfectlem2  24672  perfect  24673  bcp1ctr  24721  bposlem1  24726  bposlem2  24727  lgslem1  24739  lgsqrlem2  24789  gausslemma2dlem1a  24807  gausslemma2dlem3  24810  gausslemma2dlem4  24811  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad2lem1  24826  2lgslem1a1  24831  2lgslem1a2  24832  2lgslem1b  24834  2lgslem1c  24835  2lgslem3a1  24842  2lgslem3d1  24845  chebbnd1lem3  24877  chto1ub  24882  dchrisumlem2  24896  dchrisum0flblem2  24915  dchrisum0fno1  24917  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2  24924  mulog2sumlem2  24941  vmalogdivsum2  24944  log2sumbnd  24950  selberglem2  24952  chpdifbndlem1  24959  selberg3lem1  24963  selberg3  24965  selberg4lem1  24966  selberg4  24967  selberg4r  24976  selberg34r  24977  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6  24989  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem2  24997  pntlemb  25003  pntlemg  25004  pntlemh  25005  pntlemr  25008  pntlemk  25012  pntlemo  25013  ostth2lem1  25024  wwlkextwrd  26022  wwlkextinj  26024  clwlkisclwwlklem2a1  26073  clwlkisclwwlklem2a4  26078  clwlkisclwwlklem0  26082  clwwlkext2edg  26096  extwwlkfablem1  26367  extwwlkfablem2  26371  numclwwlkovf2ex  26379  numclwlk1lem2foa  26384  numclwlk1lem2fo  26388  numclwwlk2lem1  26395  numclwlk2lem2f  26396  numclwwlk2  26400  ex-ind-dvds  26476  archirngz  28880  archiabllem2c  28886  sqsscirc1  29088  dya2icoseg  29472  dya2iocucvr  29479  oddpwdc  29549  eulerpartlemgs2  29575  fibp1  29596  signslema  29771  subfacp1lem1  30221  subfacp1lem5  30226  dnibndlem10  31453  knoppndvlem2  31480  knoppndvlem7  31485  knoppndvlem9  31487  knoppndvlem10  31488  knoppndvlem16  31494  itg2addnclem  32427  dvasin  32462  areacirclem1  32466  areacirclem3  32468  isbnd2  32548  rmspecsqrtnq  36284  rmxluc  36315  rmyluc2  36317  rmydbl  36319  jm2.18  36369  jm2.22  36376  jm2.25  36380  jm2.27c  36388  jm3.1lem2  36399  imo72b2lem0  37283  refsum2cnlem1  38015  oddfl  38226  xralrple2  38308  infleinflem2  38325  sumnnodd  38494  0ellimcdiv  38513  coseq0  38544  sinmulcos  38545  coskpi2  38546  sinaover2ne0  38548  cosknegpi  38549  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  itgsinexp  38643  stoweidlem1  38691  stoweidlem62  38752  wallispilem4  38758  wallispilem5  38759  wallispi  38760  wallispi2lem1  38761  wallispi2lem2  38762  wallispi2  38763  stirlinglem1  38764  stirlinglem3  38766  stirlinglem4  38767  stirlinglem5  38768  stirlinglem6  38769  stirlinglem7  38770  stirlinglem8  38771  stirlinglem10  38773  stirlinglem11  38774  stirlinglem13  38776  stirlinglem14  38777  stirlinglem15  38778  dirker2re  38782  dirkerdenne0  38783  dirkerval2  38784  dirkerre  38785  dirkertrigeqlem1  38788  dirkertrigeqlem2  38789  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkeritg  38792  dirkercncflem1  38793  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem43  38840  fourierdlem44  38841  fourierdlem56  38852  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem66  38862  fourierdlem68  38864  fourierdlem72  38868  fourierdlem76  38872  fourierdlem79  38875  fourierdlem80  38876  fourierdlem83  38879  fourierdlem95  38891  fourierdlem104  38900  fourierdlem112  38908  fouriercnp  38916  fourierswlem  38920  sge0ad2en  39121  hoicvrrex  39243  hoiqssbllem2  39310  fmtnoodd  39781  sqrtpwpw2p  39786  fmtnorec2lem  39790  fmtnodvds  39792  goldbachthlem2  39794  fmtnoprmfac1lem  39812  fmtnoprmfac2  39815  fmtnofac1  39818  2pwp1prm  39839  mod42tp1mod8  39855  sfprmdvdsmersenne  39856  lighneallem2  39859  lighneallem4  39863  proththd  39867  dfodd6  39886  dfeven4  39887  enege  39894  onego  39895  dfeven2  39898  oddflALTV  39911  opoeALTV  39930  opeoALTV  39931  nn0onn0exALTV  39945  nn0enn0exALTV  39946  perfectALTV  39964  upgrwlkdvdelem  40937  wwlksnextwrd  41098  wwlksnextinj  41100  clwlkclwwlklem2a1  41196  clwlkclwwlklem2a4  41201  clwlkclwwlklem3  41205  clwwlksext2edg  41225  av-extwwlkfablem1  41503  av-numclwwlkovf2ex  41512  av-numclwlk1lem2foa  41516  av-numclwlk1lem2fo  41520  av-numclwwlk2lem1  41527  av-numclwlk2lem2f  41528  av-numclwwlk2  41532  0nodd  41595  2nodd  41597  2zlidl  41719  2zrngamgm  41724  2zrngagrp  41728  2zrngmmgm  41731  2zrngnmlid  41734  nn0onn0ex  42107  nn0enn0ex  42108  nnpw2even  42112  fldivexpfllog2  42152  blenpw2m1  42166  nnpw2blen  42167  blennn0em1  42178  dig2nn1st  42192  dig2bits  42201  dignn0flhalflem1  42202  dignn0flhalflem2  42203  dignn0ehalf  42204  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator