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

Theorem 2cnd 11206
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 11204 . 2 2 ∈ ℂ
21a1i 11 1 (𝜑 → 2 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103  cc 10047  2c2 11183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-i2m1 10117  ax-1ne0 10118  ax-rrecex 10121  ax-cnre 10122
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009  df-ov 6768  df-2 11192
This theorem is referenced by:  subhalfhalf  11379  cnm2m1cnm3  11398  xp1d2m1eqxm1d2  11399  zeo2  11577  fzosplitprm1  12693  2tnp1ge0ge0  12745  flhalf  12746  2txmodxeq0  12845  mulbinom2  13099  binom3  13100  zesq  13102  expmulnbnd  13111  discr  13116  sqoddm1div8  13143  mulsubdivbinom2  13161  swrds2m  13807  amgm2  14229  iseraltlem2  14533  iseralt  14535  trirecip  14715  geo2sum  14724  bpolydiflem  14905  ege2le3  14940  tanval3  14984  sinhval  15004  tanhlt1  15010  sqrt2irrlem  15097  sqrt2irr  15099  even2n  15189  oddm1even  15190  oddp1even  15191  mod2eq1n2dvds  15194  ltoddhalfle  15208  m1exp1  15216  nn0enne  15217  flodddiv4  15260  flodddiv4t2lthalf  15263  bitsp1e  15277  bitsp1o  15278  bitsfzo  15280  bitsmod  15281  bitsinv1lem  15286  sadadd2lem2  15295  sadcaddlem  15302  bitsuz  15319  bitsshft  15320  prmdiv  15613  vfermltlALT  15630  iserodd  15663  4sqlem7  15771  4sqlem10  15774  4sqlem19  15790  prmgaplem7  15884  2expltfac  15922  efgredlemg  18276  frgpnabllem1  18397  metnrmlem3  22786  iihalf1cn  22853  iihalf2cn  22855  pcoass  22945  cphipval2  23161  csbren  23303  trirn  23304  minveclem2  23318  ovolunlem1a  23385  uniioombllem5  23476  uniioombl  23478  dyaddisjlem  23484  mbfi1fseqlem5  23606  mbfi1fseqlem6  23607  dvsincos  23864  lhop1  23897  cosargd  24474  dvcnsqrt  24605  root1id  24615  ssscongptld  24672  chordthmlem  24679  chordthmlem2  24680  chordthmlem4  24682  heron  24685  dcubic1  24692  mcubic  24694  cubic2  24695  quartlem4  24707  quart  24708  cosasin  24751  cosatan  24768  atantayl  24784  atantayl2  24785  atantayl3  24786  log2tlbnd  24792  cxp2limlem  24822  divsqrtsumlem  24826  lgamgulmlem2  24876  lgamgulmlem4  24878  lgamucov  24884  ftalem2  24920  basellem2  24928  basellem3  24929  basellem5  24931  basellem8  24934  logfaclbnd  25067  perfectlem2  25075  perfect  25076  bcp1ctr  25124  bposlem1  25129  bposlem2  25130  lgslem1  25142  lgsqrlem2  25192  gausslemma2dlem1a  25210  gausslemma2dlem3  25213  gausslemma2dlem4  25214  lgseisenlem1  25220  lgseisenlem2  25221  lgseisenlem3  25222  lgseisenlem4  25223  lgsquadlem1  25225  lgsquadlem2  25226  lgsquad2lem1  25229  2lgslem1a1  25234  2lgslem1a2  25235  2lgslem1b  25237  2lgslem1c  25238  2lgslem3a1  25245  2lgslem3d1  25248  chebbnd1lem3  25280  chto1ub  25285  dchrisumlem2  25299  dchrisum0flblem2  25318  dchrisum0fno1  25320  dchrisum0lem1b  25324  dchrisum0lem1  25325  dchrisum0lem2  25327  mulog2sumlem2  25344  vmalogdivsum2  25347  log2sumbnd  25353  selberglem2  25355  chpdifbndlem1  25362  selberg3lem1  25366  selberg3  25368  selberg4lem1  25369  selberg4  25370  selberg4r  25379  selberg34r  25380  pntrlog2bndlem3  25388  pntrlog2bndlem4  25389  pntrlog2bndlem5  25390  pntrlog2bndlem6  25392  pntpbnd1a  25394  pntpbnd2  25396  pntibndlem2  25400  pntlemb  25406  pntlemg  25407  pntlemh  25408  pntlemr  25411  pntlemk  25415  pntlemo  25416  ostth2lem1  25427  finsumvtxdg2ssteplem4  26575  upgrwlkdvdelem  26763  wwlksnextwrd  26936  wwlksnextinj  26938  clwlkclwwlklem2a1  27036  clwlkclwwlklem2a4  27041  clwlkclwwlklem3  27045  clwwlkext2edg  27107  clwwlknonex2lem1  27177  clwwlknonex2lem2  27178  extwwlkfablem1OLD  27418  2clwwlk2clwwlk  27428  numclwlk1lem2foalem  27431  numclwlk1lem2fo  27438  numclwwlk2lem1  27458  numclwlk2lem2f  27459  numclwwlk2  27463  numclwwlk2lem1OLD  27465  numclwlk2lem2fOLD  27466  numclwwlk2OLD  27470  ex-ind-dvds  27550  archirngz  29973  archiabllem2c  29979  sqsscirc1  30184  dya2icoseg  30569  dya2iocucvr  30576  oddpwdc  30646  eulerpartlemgs2  30672  fibp1  30693  signslema  30869  itgexpif  30914  vtsprod  30947  hgt750lemd  30956  logdivsqrle  30958  subfacp1lem1  31389  subfacp1lem5  31394  dnibndlem10  32704  knoppndvlem2  32731  knoppndvlem7  32736  knoppndvlem9  32738  knoppndvlem10  32739  knoppndvlem16  32745  itg2addnclem  33693  dvasin  33728  areacirclem1  33732  areacirclem3  33734  isbnd2  33814  rmspecsqrtnq  37889  rmxluc  37920  rmyluc2  37922  rmydbl  37924  jm2.18  37974  jm2.22  37981  jm2.25  37985  jm2.27c  37993  jm3.1lem2  38004  imo72b2lem0  38884  refsum2cnlem1  39612  oddfl  39905  xralrple2  39985  infleinflem2  40002  sumnnodd  40282  0ellimcdiv  40301  coseq0  40495  sinmulcos  40496  coskpi2  40497  sinaover2ne0  40499  cosknegpi  40500  ioodvbdlimc1lem2  40567  ioodvbdlimc2lem  40569  itgsinexp  40590  stoweidlem1  40638  stoweidlem62  40699  wallispilem4  40705  wallispilem5  40706  wallispi  40707  wallispi2lem1  40708  wallispi2lem2  40709  wallispi2  40710  stirlinglem1  40711  stirlinglem3  40713  stirlinglem4  40714  stirlinglem5  40715  stirlinglem6  40716  stirlinglem7  40717  stirlinglem8  40718  stirlinglem10  40720  stirlinglem11  40721  stirlinglem13  40723  stirlinglem14  40724  stirlinglem15  40725  dirker2re  40729  dirkerdenne0  40730  dirkerval2  40731  dirkerre  40732  dirkertrigeqlem1  40735  dirkertrigeqlem2  40736  dirkertrigeqlem3  40737  dirkertrigeq  40738  dirkeritg  40739  dirkercncflem1  40740  dirkercncflem2  40741  dirkercncflem4  40743  fourierdlem43  40787  fourierdlem44  40788  fourierdlem56  40799  fourierdlem57  40800  fourierdlem58  40801  fourierdlem62  40805  fourierdlem66  40809  fourierdlem68  40811  fourierdlem72  40815  fourierdlem76  40819  fourierdlem79  40822  fourierdlem80  40823  fourierdlem83  40826  fourierdlem95  40838  fourierdlem104  40847  fourierdlem112  40855  fouriercnp  40863  fourierswlem  40867  sge0ad2en  41068  hoicvrrex  41193  hoiqssbllem2  41260  fmtnoodd  41872  sqrtpwpw2p  41877  fmtnorec2lem  41881  fmtnodvds  41883  goldbachthlem2  41885  fmtnoprmfac1lem  41903  fmtnoprmfac2  41906  fmtnofac1  41909  2pwp1prm  41930  mod42tp1mod8  41946  sfprmdvdsmersenne  41947  lighneallem2  41950  lighneallem4  41954  proththd  41958  dfodd6  41977  dfeven4  41978  enege  41985  onego  41986  dfeven2  41989  oddflALTV  42002  opoeALTV  42021  opeoALTV  42022  nn0onn0exALTV  42036  nn0enn0exALTV  42037  mogoldbblem  42056  perfectALTV  42059  sgoldbeven3prm  42098  0nodd  42237  2nodd  42239  2zlidl  42361  2zrngamgm  42366  2zrngagrp  42370  2zrngmmgm  42373  2zrngnmlid  42376  nn0onn0ex  42745  nn0enn0ex  42746  nnpw2even  42750  fldivexpfllog2  42786  blenpw2m1  42800  nnpw2blen  42801  blennn0em1  42812  dig2nn1st  42826  dig2bits  42835  dignn0flhalflem1  42836  dignn0flhalflem2  42837  dignn0ehalf  42838  nn0sumshdiglemA  42840  nn0sumshdiglemB  42841
  Copyright terms: Public domain W3C validator