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

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

Proof of Theorem 2cnd
StepHypRef Expression
1 2cn 11129 . 2 2 ∈ ℂ
21a1i 11 1 (𝜑 → 2 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cc 9972  2c2 11108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117
This theorem is referenced by:  subhalfhalf  11304  cnm2m1cnm3  11323  xp1d2m1eqxm1d2  11324  zeo2  11502  fzosplitprm1  12618  2tnp1ge0ge0  12670  flhalf  12671  2txmodxeq0  12770  mulbinom2  13024  binom3  13025  zesq  13027  expmulnbnd  13036  discr  13041  sqoddm1div8  13068  mulsubdivbinom2  13086  amgm2  14153  iseraltlem2  14457  iseralt  14459  trirecip  14639  geo2sum  14648  bpolydiflem  14829  ege2le3  14864  tanval3  14908  sinhval  14928  tanhlt1  14934  sqrt2irrlem  15021  sqrt2irr  15023  even2n  15113  oddm1even  15114  oddp1even  15115  mod2eq1n2dvds  15118  ltoddhalfle  15132  m1exp1  15140  nn0enne  15141  flodddiv4  15184  flodddiv4t2lthalf  15187  bitsp1e  15201  bitsp1o  15202  bitsfzo  15204  bitsmod  15205  bitsinv1lem  15210  sadadd2lem2  15219  sadcaddlem  15226  bitsuz  15243  bitsshft  15244  prmdiv  15537  vfermltlALT  15554  iserodd  15587  4sqlem7  15695  4sqlem10  15698  4sqlem19  15714  prmgaplem7  15808  2expltfac  15846  efgredlemg  18201  frgpnabllem1  18322  metnrmlem3  22711  iihalf1cn  22778  iihalf2cn  22780  pcoass  22870  cphipval2  23086  csbren  23228  trirn  23229  minveclem2  23243  ovolunlem1a  23310  uniioombllem5  23401  uniioombl  23403  dyaddisjlem  23409  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  dvsincos  23789  lhop1  23822  cosargd  24399  dvcnsqrt  24530  root1id  24540  ssscongptld  24597  chordthmlem  24604  chordthmlem2  24605  chordthmlem4  24607  heron  24610  dcubic1  24617  mcubic  24619  cubic2  24620  quartlem4  24632  quart  24633  cosasin  24676  cosatan  24693  atantayl  24709  atantayl2  24710  atantayl3  24711  log2tlbnd  24717  cxp2limlem  24747  divsqrtsumlem  24751  lgamgulmlem2  24801  lgamgulmlem4  24803  lgamucov  24809  ftalem2  24845  basellem2  24853  basellem3  24854  basellem5  24856  basellem8  24859  logfaclbnd  24992  perfectlem2  25000  perfect  25001  bcp1ctr  25049  bposlem1  25054  bposlem2  25055  lgslem1  25067  lgsqrlem2  25117  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  gausslemma2dlem4  25139  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  2lgslem1a1  25159  2lgslem1a2  25160  2lgslem1b  25162  2lgslem1c  25163  2lgslem3a1  25170  2lgslem3d1  25173  chebbnd1lem3  25205  chto1ub  25210  dchrisumlem2  25224  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2  25252  mulog2sumlem2  25269  vmalogdivsum2  25272  log2sumbnd  25278  selberglem2  25280  chpdifbndlem1  25287  selberg3lem1  25291  selberg3  25293  selberg4lem1  25294  selberg4  25295  selberg4r  25304  selberg34r  25305  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2  25325  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemr  25336  pntlemk  25340  pntlemo  25341  ostth2lem1  25352  finsumvtxdg2ssteplem4  26500  upgrwlkdvdelem  26688  wwlksnextwrd  26860  wwlksnextinj  26862  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a4  26963  clwlkclwwlklem3  26967  clwwlkext2edg  27020  clwwlknonex2lem1  27082  clwwlknonex2lem2  27083  extwwlkfablem1OLD  27323  2clwwlk2clwwlklem2lem2  27329  2clwwlk2clwwlk  27338  numclwlk1lem2foalem  27341  numclwlk1lem2fo  27348  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2  27361  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwwlk2OLD  27368  ex-ind-dvds  27448  archirngz  29871  archiabllem2c  29877  sqsscirc1  30082  dya2icoseg  30467  dya2iocucvr  30474  oddpwdc  30544  eulerpartlemgs2  30570  fibp1  30591  signslema  30767  itgexpif  30812  vtsprod  30845  hgt750lemd  30854  logdivsqrle  30856  subfacp1lem1  31287  subfacp1lem5  31292  dnibndlem10  32602  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem9  32636  knoppndvlem10  32637  knoppndvlem16  32643  itg2addnclem  33591  dvasin  33626  areacirclem1  33630  areacirclem3  33632  isbnd2  33712  rmspecsqrtnq  37787  rmxluc  37818  rmyluc2  37820  rmydbl  37822  jm2.18  37872  jm2.22  37879  jm2.25  37883  jm2.27c  37891  jm3.1lem2  37902  imo72b2lem0  38782  refsum2cnlem1  39510  oddfl  39803  xralrple2  39883  infleinflem2  39900  sumnnodd  40180  0ellimcdiv  40199  coseq0  40393  sinmulcos  40394  coskpi2  40395  sinaover2ne0  40397  cosknegpi  40398  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  itgsinexp  40488  stoweidlem1  40536  stoweidlem62  40597  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  stirlinglem13  40621  stirlinglem14  40622  stirlinglem15  40623  dirker2re  40627  dirkerdenne0  40628  dirkerval2  40629  dirkerre  40630  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem43  40685  fourierdlem44  40686  fourierdlem56  40697  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem66  40707  fourierdlem68  40709  fourierdlem72  40713  fourierdlem76  40717  fourierdlem79  40720  fourierdlem80  40721  fourierdlem83  40724  fourierdlem95  40736  fourierdlem104  40745  fourierdlem112  40753  fouriercnp  40761  fourierswlem  40765  sge0ad2en  40966  hoicvrrex  41091  hoiqssbllem2  41158  fmtnoodd  41770  sqrtpwpw2p  41775  fmtnorec2lem  41779  fmtnodvds  41781  goldbachthlem2  41783  fmtnoprmfac1lem  41801  fmtnoprmfac2  41804  fmtnofac1  41807  2pwp1prm  41828  mod42tp1mod8  41844  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem4  41852  proththd  41856  dfodd6  41875  dfeven4  41876  enege  41883  onego  41884  dfeven2  41887  oddflALTV  41900  opoeALTV  41919  opeoALTV  41920  nn0onn0exALTV  41934  nn0enn0exALTV  41935  mogoldbblem  41954  perfectALTV  41957  sgoldbeven3prm  41996  0nodd  42135  2nodd  42137  2zlidl  42259  2zrngamgm  42264  2zrngagrp  42268  2zrngmmgm  42271  2zrngnmlid  42274  nn0onn0ex  42643  nn0enn0ex  42644  nnpw2even  42648  fldivexpfllog2  42684  blenpw2m1  42698  nnpw2blen  42699  blennn0em1  42710  dig2nn1st  42724  dig2bits  42733  dignn0flhalflem1  42734  dignn0flhalflem2  42735  dignn0ehalf  42736  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator