Theorem 2cnd 12209

Description: The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2cnd	⊢ (𝜑 → 2 ∈ ℂ)

Proof of Theorem 2cnd

Step	Hyp	Ref	Expression
1		2cn 12206	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 2 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11010  2c2 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11070  ax-addcl 11072

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12194

This theorem is referenced by:  subhalfhalf  12361  cnm2m1cnm3  12380  xp1d2m1eqxm1d2  12381  zeo2  12566  ge2halflem1  13013  fzosplitprm1  13684  2tnp1ge0ge0  13739  flhalf  13740  2txmodxeq0  13844  mulbinom2  14136  binom3  14137  zesq  14139  expmulnbnd  14148  discr  14153  sqoddm1div8  14156  mulsubdivbinom2  14175  swrds2m  14854  amgm2  15283  bhmafibid1cn  15379  bhmafibid2cn  15380  iseraltlem2  15596  iseralt  15598  trirecip  15776  geo2sum  15786  bpolydiflem  15967  ege2le3  16003  tanval3  16049  sinhval  16069  tanhlt1  16075  sqrt2irrlem  16163  sqrt2irr  16164  even2n  16259  oddm1even  16260  oddp1even  16261  mod2eq1n2dvds  16264  ltoddhalfle  16278  m1exp1  16293  nn0enne  16294  flodddiv4  16332  flodddiv4t2lthalf  16335  bitsp1e  16349  bitsp1o  16350  bitsfzo  16352  bitsmod  16353  bitsinv1lem  16358  sadadd2lem2  16367  sadcaddlem  16374  bitsuz  16391  bitsshft  16392  prmdiv  16702  vfermltlALT  16720  iserodd  16753  4sqlem7  16862  4sqlem10  16865  4sqlem19  16881  prmgaplem7  16975  2expltfac  17010  smndex2dlinvh  18831  efgredlemg  19660  frgpnabllem1  19791  ablsimpgfindlem1  20027  metnrmlem3  24783  iihalf1cn  24859  iihalf1cnOLD  24860  iihalf2cn  24862  iihalf2cnOLD  24863  pcoass  24957  cphipval2  25174  csbren  25332  trirn  25333  minveclem2  25359  ovolunlem1a  25430  uniioombllem5  25521  uniioombl  25523  dyaddisjlem  25529  mbfi1fseqlem5  25653  mbfi1fseqlem6  25654  dvsincos  25918  lhop1  25952  cosargd  26550  dvcnsqrt  26686  root1id  26697  ssscongptld  26765  chordthmlem  26775  chordthmlem2  26776  chordthmlem4  26778  heron  26781  dcubic1  26788  mcubic  26790  cubic2  26791  quartlem4  26803  quart  26804  cosasin  26847  cosatan  26864  atantayl  26880  atantayl2  26881  atantayl3  26882  log2tlbnd  26888  cxp2limlem  26919  divsqrtsumlem  26923  lgamgulmlem2  26973  lgamgulmlem4  26975  lgamucov  26981  ftalem2  27017  basellem2  27025  basellem3  27026  basellem5  27028  basellem8  27031  logfaclbnd  27166  perfectlem2  27174  perfect  27175  bcp1ctr  27223  bposlem1  27228  bposlem2  27229  lgslem1  27241  lgsqrlem2  27291  gausslemma2dlem1a  27309  gausslemma2dlem3  27312  gausslemma2dlem4  27313  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgsquadlem1  27324  lgsquadlem2  27325  lgsquad2lem1  27328  2lgslem1a1  27333  2lgslem1a2  27334  2lgslem1b  27336  2lgslem1c  27337  2lgslem3a1  27344  2lgslem3d1  27347  2sq2  27377  addsq2nreurex  27388  chebbnd1lem3  27415  chto1ub  27420  dchrisumlem2  27434  dchrisum0flblem2  27453  dchrisum0fno1  27455  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2  27462  logdivsum  27477  mulog2sumlem2  27479  vmalogdivsum2  27482  log2sumbnd  27488  selberglem2  27490  chpdifbndlem1  27497  selberg3lem1  27501  selberg3  27503  selberg4lem1  27504  selberg4  27505  selberg4r  27514  selberg34r  27515  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntpbnd1a  27529  pntpbnd2  27531  pntibndlem2  27535  pntlemb  27541  pntlemg  27542  pntlemh  27543  pntlemr  27546  pntlemk  27550  pntlemo  27551  ostth2lem1  27562  finsumvtxdg2ssteplem4  29534  upgrwlkdvdelem  29721  wwlksnextwrd  29882  wwlksnextinj  29884  clwlkclwwlklem2a1  29979  clwlkclwwlklem2a4  29984  clwlkclwwlklem3  29988  clwwlkext2edg  30043  clwwlknonex2lem1  30094  clwwlknonex2lem2  30095  2clwwlk2clwwlk  30337  numclwwlk1lem2foalem  30338  numclwwlk1lem2fo  30345  numclwwlk2lem1  30363  numclwlk2lem2f  30364  numclwwlk2  30368  ex-ind-dvds  30448  nrt2irr  30460  binom2subadd  32732  quad3d  32740  2exple2exp  32835  wrdt2ind  32941  archirngz  33165  archiabllem2c  33171  fldext2rspun  33702  constrrtcc  33755  constrelextdg2  33767  constraddcl  33782  constrrecl  33789  constrresqrtcl  33797  2sqr3nconstr  33801  cos9thpiminplylem1  33802  cos9thpiminplylem2  33803  cos9thpiminplylem3  33804  cos9thpiminply  33808  cos9thpinconstrlem1  33809  cos9thpinconstrlem2  33810  cos9thpinconstr  33811  sqsscirc1  33928  dya2icoseg  34297  dya2iocucvr  34304  oddpwdc  34374  eulerpartlemgs2  34400  fibp1  34421  signslema  34582  itgexpif  34626  vtsprod  34659  hgt750lemd  34668  logdivsqrle  34670  subfacp1lem1  35230  subfacp1lem5  35235  dnibndlem10  36538  knoppcnlem10  36553  knoppndvlem2  36564  knoppndvlem7  36569  knoppndvlem9  36571  knoppndvlem10  36572  knoppndvlem16  36578  irrdifflemf  37376  itg2addnclem  37717  dvasin  37750  areacirclem1  37754  areacirclem3  37756  isbnd2  37829  lcmineqlem21  42148  3lexlogpow2ineq2  42158  dvrelog2b  42165  dvrelogpow2b  42167  aks4d1p1p4  42170  aks4d1p1p6  42172  aks4d1p1p7  42173  aks4d1p1p5  42174  aks4d1p9  42187  posbezout  42199  2np3bcnp1  42243  2ap1caineq  42244  oddnumth  42410  nicomachus  42411  sumcubes  42412  ef11d  42438  cxpi11d  42442  tan3rdpi  42451  readvrec2  42460  remul02  42504  remul01  42506  dffltz  42733  fltne  42743  flt4lem5e  42755  cu3addd  42779  rmspecsqrtnq  43004  rmxluc  43034  rmyluc2  43036  rmydbl  43038  jm2.18  43086  jm2.22  43093  jm2.25  43097  jm2.27c  43105  jm3.1lem2  43116  sqrtcval  43739  imo72b2lem0  44263  refsum2cnlem1  45139  oddfl  45384  xralrple2  45458  infleinflem2  45474  sumnnodd  45735  0ellimcdiv  45752  coseq0  45967  sinmulcos  45968  coskpi2  45969  sinaover2ne0  45971  cosknegpi  45972  ioodvbdlimc1lem2  46035  ioodvbdlimc2lem  46037  itgsinexp  46058  stoweidlem1  46104  stoweidlem62  46165  wallispilem4  46171  wallispilem5  46172  wallispi  46173  wallispi2lem1  46174  wallispi2lem2  46175  wallispi2  46176  stirlinglem1  46177  stirlinglem3  46179  stirlinglem4  46180  stirlinglem5  46181  stirlinglem6  46182  stirlinglem7  46183  stirlinglem8  46184  stirlinglem10  46186  stirlinglem11  46187  stirlinglem13  46189  stirlinglem14  46190  stirlinglem15  46191  dirker2re  46195  dirkerdenne0  46196  dirkerval2  46197  dirkerre  46198  dirkertrigeqlem1  46201  dirkertrigeqlem2  46202  dirkertrigeqlem3  46203  dirkertrigeq  46204  dirkeritg  46205  dirkercncflem1  46206  dirkercncflem2  46207  dirkercncflem4  46209  fourierdlem43  46253  fourierdlem44  46254  fourierdlem56  46265  fourierdlem57  46266  fourierdlem58  46267  fourierdlem62  46271  fourierdlem66  46275  fourierdlem68  46277  fourierdlem72  46281  fourierdlem76  46285  fourierdlem79  46288  fourierdlem80  46289  fourierdlem83  46292  fourierdlem95  46304  fourierdlem104  46313  fourierdlem112  46321  fouriercnp  46329  fourierswlem  46333  sge0ad2en  46534  hoicvrrex  46659  hoiqssbllem2  46726  2tceilhalfelfzo1  47437  minusmodnep2tmod  47458  modmkpkne  47466  modm2nep1  47471  modm1nem2  47474  fmtnoodd  47638  sqrtpwpw2p  47643  fmtnorec2lem  47647  fmtnodvds  47649  goldbachthlem2  47651  fmtnoprmfac1lem  47669  fmtnoprmfac2  47672  fmtnofac1  47675  2pwp1prm  47694  mod42tp1mod8  47707  sfprmdvdsmersenne  47708  lighneallem2  47711  lighneallem4  47715  proththd  47719  quad1  47725  requad01  47726  requad1  47727  requad2  47728  dfodd6  47742  dfeven4  47743  enege  47750  onego  47751  dfeven2  47754  oddflALTV  47768  opoeALTV  47788  opeoALTV  47789  nn0onn0exALTV  47804  nn0enn0exALTV  47805  nnennexALTV  47806  mogoldbblem  47825  perfectALTV  47828  fppr2odd  47836  sgoldbeven3prm  47888  gpg3nbgrvtx0  48181  gpg3kgrtriexlem2  48189  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  pgnbgreunbgrlem2lem3  48221  0nodd  48275  2nodd  48277  2zlidl  48345  2zrngamgm  48350  2zrngagrp  48354  2zrngmmgm  48357  2zrngnmlid  48360  nn0onn0ex  48629  nn0enn0ex  48630  nnennex  48631  nnpw2even  48635  fldivexpfllog2  48671  blenpw2m1  48685  nnpw2blen  48686  blennn0em1  48697  dig2nn1st  48711  dig2bits  48720  dignn0flhalflem1  48721  dignn0flhalflem2  48722  dignn0ehalf  48723  nn0sumshdiglemA  48725  nn0sumshdiglemB  48726  itcovalt2lem2lem2  48780  ackval2  48788  ackval3  48789  itschlc0yqe  48866  itsclc0yqsollem1  48868  itsclc0yqsol  48870  itsclc0xyqsolr  48875  itsclquadb  48882  2itscplem1  48884  2itscplem3  48886  itscnhlinecirc02plem1  48888