Theorem 2cnd 12334

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 12331	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 2 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11113  2c2 12310

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-addcl 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12318

This theorem is used by:  subhalfhalf  12493  cnm2m1cnm3  12512  xp1d2m1eqxm1d2  12513  zeo2  12699  ge2halflem1  13149  fzosplitprm1  13824  2tnp1ge0ge0  13880  flhalf  13881  2txmodxeq0  13985  mulbinom2  14277  binom3  14278  zesq  14280  expmulnbnd  14289  discr  14294  sqoddm1div8  14297  mulsubdivbinom2  14316  swrds2m  15002  amgm2  15445  bhmafibid1cn  15541  bhmafibid2cn  15542  iseraltlem2  15758  iseralt  15760  trirecip  15940  geo2sum  15950  bpolydiflem  16130  bpoly4  16135  ege2le3  16166  tanval3  16212  sinhval  16232  tanhlt1  16238  sqrt2irrlem  16326  sqrt2irr  16327  even2n  16422  oddm1even  16423  oddp1even  16424  mod2eq1n2dvds  16427  ltoddhalfle  16441  m1exp1  16456  nn0enne  16457  flodddiv4  16495  flodddiv4t2lthalf  16498  bitsp1e  16512  bitsp1o  16513  bitsfzo  16515  bitsmod  16516  bitsinv1lem  16521  sadadd2lem2  16530  sadcaddlem  16537  bitsuz  16554  bitsshft  16555  prmdiv  16866  vfermltlALT  16884  iserodd  16917  4sqlem7  17026  4sqlem10  17029  4sqlem19  17045  prmgaplem7  17139  2expltfac  17174  smndex2dlinvh  19016  efgredlemg  19856  frgpnabllem1  19987  ablsimpgfindlem1  20223  metnrmlem3  25070  iihalf1cn  25142  iihalf2cn  25144  pcoass  25234  cphipval2  25451  csbren  25609  trirn  25610  minveclem2  25636  ovolunlem1a  25706  uniioombllem5  25797  uniioombl  25799  dyaddisjlem  25805  mbfi1fseqlem5  25929  mbfi1fseqlem6  25930  dvsincos  26191  lhop1  26224  cosargd  26824  dvcnsqrt  26960  root1id  26970  ssscongptld  27038  chordthmlem  27048  chordthmlem2  27049  chordthmlem4  27051  heron  27054  dcubic1  27061  mcubic  27063  cubic2  27064  quartlem4  27076  quart  27077  cosasin  27120  cosatan  27137  atantayl  27153  atantayl2  27154  atantayl3  27155  log2tlbnd  27161  cxp2limlem  27191  divsqrtsumlem  27195  lgamgulmlem2  27245  lgamgulmlem4  27247  lgamucov  27253  ftalem2  27289  basellem2  27297  basellem3  27298  basellem5  27300  basellem8  27303  logfaclbnd  27437  perfectlem2  27445  perfect  27446  bcp1ctr  27494  bposlem1  27499  bposlem2  27500  lgslem1  27512  lgsqrlem2  27562  gausslemma2dlem1a  27580  gausslemma2dlem3  27583  gausslemma2dlem4  27584  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem3  27592  lgseisenlem4  27593  lgsquadlem1  27595  lgsquadlem2  27596  lgsquad2lem1  27599  2lgslem1a1  27604  2lgslem1a2  27605  2lgslem1b  27607  2lgslem1c  27608  2lgslem3a1  27615  2lgslem3d1  27618  2sq2  27648  addsq2nreurex  27659  chebbnd1lem3  27686  chto1ub  27691  dchrisumlem2  27705  dchrisum0flblem2  27724  dchrisum0fno1  27726  dchrisum0lem1b  27730  dchrisum0lem1  27731  dchrisum0lem2  27733  logdivsum  27748  mulog2sumlem2  27750  vmalogdivsum2  27753  log2sumbnd  27759  selberglem2  27761  chpdifbndlem1  27768  selberg3lem1  27772  selberg3  27774  selberg4lem1  27775  selberg4  27776  selberg4r  27785  selberg34r  27786  pntrlog2bndlem3  27794  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntpbnd1a  27800  pntpbnd2  27802  pntibndlem2  27806  pntlemb  27812  pntlemg  27813  pntlemh  27814  pntlemr  27817  pntlemk  27821  pntlemo  27822  ostth2lem1  27833  finsumvtxdg2ssteplem4  29956  upgrwlkdvdelem  30149  wwlksnextwrd  30313  wwlksnextinj  30315  clwlkclwwlklem2a1  30410  clwlkclwwlklem2a4  30415  clwlkclwwlklem3  30419  clwwlkext2edg  30474  clwwlknonex2lem1  30525  clwwlknonex2lem2  30526  2clwwlk2clwwlk  30772  numclwwlk1lem2foalem  30773  numclwwlk1lem2fo  30780  numclwwlk2lem1  30798  numclwlk2lem2f  30799  numclwwlk2  30803  ex-ind-dvds  30883  nrt2irr  30895  binom2subadd  33156  quad3d  33164  2exple2exp  33248  wrdt2ind  33339  archirngz  33573  archiabllem2c  33579  fldext2rspun  34136  constrrtcc  34189  constrelextdg2  34201  constraddcl  34216  constrrecl  34223  constrresqrtcl  34231  2sqr3nconstr  34235  cos9thpiminplylem1  34236  cos9thpiminplylem2  34237  cos9thpiminplylem3  34238  cos9thpiminply  34242  cos9thpinconstrlem1  34243  cos9thpinconstrlem2  34244  cos9thpinconstr  34245  sqsscirc1  34362  dya2icoseg  34732  dya2iocucvr  34739  oddpwdc  34809  eulerpartlemgs2  34835  fibp1  34856  signslema  35014  itgexpif  35058  vtsprod  35091  hgt750lemd  35100  logdivsqrle  35102  subfacp1lem1  35708  subfacp1lem5  35713  dnibndlem10  37133  knoppcnlem10  37148  knoppndvlem2  37159  knoppndvlem7  37164  knoppndvlem9  37166  knoppndvlem10  37167  knoppndvlem16  37173  irrdifflemf  38026  qdiff  38028  itg2addnclem  38379  dvasin  38412  areacirclem1  38416  areacirclem3  38418  isbnd2  38492  lcmineqlem21  42874  3lexlogpow2ineq2  42884  dvrelog2b  42891  dvrelogpow2b  42893  aks4d1p1p4  42896  aks4d1p1p6  42898  aks4d1p1p7  42899  aks4d1p1p5  42900  aks4d1p9  42913  posbezout  42925  2np3bcnp1  42969  2ap1caineq  42970  oddnumth  43130  nicomachus  43131  sumcubes  43132  ef11d  43158  cxpi11d  43162  tan3rdpi  43171  readvrec2  43180  remul02  43224  remul01  43226  dffltz  43424  fltne  43434  flt4lem5e  43446  cu3addd  43470  rmspecsqrtnq  43691  rmxluc  43721  rmyluc2  43723  rmydbl  43725  jm2.18  43773  jm2.22  43780  jm2.25  43784  jm2.27c  43792  jm3.1lem2  43803  sqrtcval  44425  imo72b2lem0  44949  refsum2cnlem1  45815  oddfl  46055  xralrple2  46128  infleinflem2  46144  sumnnodd  46404  0ellimcdiv  46421  coseq0  46636  sinmulcos  46637  coskpi2  46638  sinaover2ne0  46640  cosknegpi  46641  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  itgsinexp  46727  stoweidlem1  46773  stoweidlem62  46834  wallispilem4  46840  wallispilem5  46841  wallispi  46842  wallispi2lem1  46843  wallispi2lem2  46844  wallispi2  46845  stirlinglem1  46846  stirlinglem3  46848  stirlinglem4  46849  stirlinglem5  46850  stirlinglem6  46851  stirlinglem7  46852  stirlinglem8  46853  stirlinglem10  46855  stirlinglem11  46856  stirlinglem13  46858  stirlinglem14  46859  stirlinglem15  46860  dirker2re  46864  dirkerdenne0  46865  dirkerval2  46866  dirkerre  46867  dirkertrigeqlem1  46870  dirkertrigeqlem2  46871  dirkertrigeqlem3  46872  dirkertrigeq  46873  dirkeritg  46874  dirkercncflem1  46875  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem43  46922  fourierdlem44  46923  fourierdlem56  46934  fourierdlem57  46935  fourierdlem58  46936  fourierdlem62  46940  fourierdlem66  46944  fourierdlem68  46946  fourierdlem72  46950  fourierdlem76  46954  fourierdlem79  46957  fourierdlem80  46958  fourierdlem83  46961  fourierdlem95  46973  fourierdlem104  46982  fourierdlem112  46990  fouriercnp  46998  fourierswlem  47002  sge0ad2en  47203  hoicvrrex  47328  hoiqssbllem2  47395  sin3t  47666  cos3t  47667  sin5tlem1  47668  sin5tlem3  47670  sin5tlem4  47671  sin5t  47673  2tceilhalfelfzo1  48131  minusmodnep2tmod  48154  modmkpkne  48162  modm2nep1  48167  modm1nem2  48170  fmtnoodd  48343  sqrtpwpw2p  48348  fmtnorec2lem  48352  fmtnodvds  48354  goldbachthlem2  48356  fmtnoprmfac1lem  48374  fmtnoprmfac2  48377  fmtnofac1  48380  2pwp1prm  48399  mod42tp1mod8  48412  sfprmdvdsmersenne  48413  lighneallem2  48416  lighneallem4  48420  proththd  48424  nprmdvdsfacm1lem1  48430  ppivalnn4  48437  quad1  48443  requad01  48444  requad1  48445  requad2  48446  dfodd6  48460  dfeven4  48461  enege  48468  onego  48469  dfeven2  48472  oddflALTV  48486  opoeALTV  48506  opeoALTV  48507  nn0onn0exALTV  48522  nn0enn0exALTV  48523  nnennexALTV  48524  mogoldbblem  48543  perfectALTV  48546  fppr2odd  48554  sgoldbeven3prm  48606  gpg3nbgrvtx0  48899  gpg3kgrtriexlem2  48907  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  pgnbgreunbgrlem2lem3  48939  0nodd  48992  2nodd  48994  2zlidl  49062  2zrngamgm  49067  2zrngagrp  49071  2zrngmmgm  49074  2zrngnmlid  49077  nn0onn0ex  49360  nn0enn0ex  49361  nnennex  49362  nnpw2even  49366  fldivexpfllog2  49402  blenpw2m1  49416  nnpw2blen  49417  blennn0em1  49428  dig2nn1st  49442  dig2bits  49451  dignn0flhalflem1  49452  dignn0flhalflem2  49453  dignn0ehalf  49454  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  itcovalt2lem2lem2  49511  ackval2  49519  ackval3  49520  itschlc0yqe  49597  itsclc0yqsollem1  49599  itsclc0yqsol  49601  itsclc0xyqsolr  49606  itsclquadb  49613  2itscplem1  49615  2itscplem3  49617  itscnhlinecirc02plem1  49619