Theorem 2cnd 12290

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12275

This theorem is referenced by:  subhalfhalf  12446  cnm2m1cnm3  12465  xp1d2m1eqxm1d2  12466  zeo2  12649  fzosplitprm1  13742  2tnp1ge0ge0  13794  flhalf  13795  2txmodxeq0  13896  mulbinom2  14186  binom3  14187  zesq  14189  expmulnbnd  14198  discr  14203  sqoddm1div8  14206  mulsubdivbinom2  14222  swrds2m  14892  amgm2  15316  bhmafibid1cn  15410  bhmafibid2cn  15411  iseraltlem2  15629  iseralt  15631  trirecip  15809  geo2sum  15819  bpolydiflem  15998  ege2le3  16033  tanval3  16077  sinhval  16097  tanhlt1  16103  sqrt2irrlem  16191  sqrt2irr  16192  even2n  16285  oddm1even  16286  oddp1even  16287  mod2eq1n2dvds  16290  ltoddhalfle  16304  m1exp1  16319  nn0enne  16320  flodddiv4  16356  flodddiv4t2lthalf  16359  bitsp1e  16373  bitsp1o  16374  bitsfzo  16376  bitsmod  16377  bitsinv1lem  16382  sadadd2lem2  16391  sadcaddlem  16398  bitsuz  16415  bitsshft  16416  prmdiv  16718  vfermltlALT  16735  iserodd  16768  4sqlem7  16877  4sqlem10  16880  4sqlem19  16896  prmgaplem7  16990  2expltfac  17026  smndex2dlinvh  18798  efgredlemg  19610  frgpnabllem1  19741  ablsimpgfindlem1  19977  metnrmlem3  24377  iihalf1cn  24448  iihalf2cn  24450  pcoass  24540  cphipval2  24758  csbren  24916  trirn  24917  minveclem2  24943  ovolunlem1a  25013  uniioombllem5  25104  uniioombl  25106  dyaddisjlem  25112  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  dvsincos  25498  lhop1  25531  cosargd  26116  dvcnsqrt  26252  root1id  26262  ssscongptld  26327  chordthmlem  26337  chordthmlem2  26338  chordthmlem4  26340  heron  26343  dcubic1  26350  mcubic  26352  cubic2  26353  quartlem4  26365  quart  26366  cosasin  26409  cosatan  26426  atantayl  26442  atantayl2  26443  atantayl3  26444  log2tlbnd  26450  cxp2limlem  26480  divsqrtsumlem  26484  lgamgulmlem2  26534  lgamgulmlem4  26536  lgamucov  26542  ftalem2  26578  basellem2  26586  basellem3  26587  basellem5  26589  basellem8  26592  logfaclbnd  26725  perfectlem2  26733  perfect  26734  bcp1ctr  26782  bposlem1  26787  bposlem2  26788  lgslem1  26800  lgsqrlem2  26850  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  gausslemma2dlem4  26872  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem1  26887  2lgslem1a1  26892  2lgslem1a2  26893  2lgslem1b  26895  2lgslem1c  26896  2lgslem3a1  26903  2lgslem3d1  26906  2sq2  26936  addsq2nreurex  26947  chebbnd1lem3  26974  chto1ub  26979  dchrisumlem2  26993  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2  27021  logdivsum  27036  mulog2sumlem2  27038  vmalogdivsum2  27041  log2sumbnd  27047  selberglem2  27049  chpdifbndlem1  27056  selberg3lem1  27060  selberg3  27062  selberg4lem1  27063  selberg4  27064  selberg4r  27073  selberg34r  27074  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemb  27100  pntlemg  27101  pntlemh  27102  pntlemr  27105  pntlemk  27109  pntlemo  27110  ostth2lem1  27121  finsumvtxdg2ssteplem4  28805  upgrwlkdvdelem  28993  wwlksnextwrd  29151  wwlksnextinj  29153  clwlkclwwlklem2a1  29245  clwlkclwwlklem2a4  29250  clwlkclwwlklem3  29254  clwwlkext2edg  29309  clwwlknonex2lem1  29360  clwwlknonex2lem2  29361  2clwwlk2clwwlk  29603  numclwwlk1lem2foalem  29604  numclwwlk1lem2fo  29611  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwwlk2  29634  ex-ind-dvds  29714  nrt2irr  29726  wrdt2ind  32117  archirngz  32335  archiabllem2c  32341  sqsscirc1  32888  dya2icoseg  33276  dya2iocucvr  33283  oddpwdc  33353  eulerpartlemgs2  33379  fibp1  33400  signslema  33573  itgexpif  33618  vtsprod  33651  hgt750lemd  33660  logdivsqrle  33662  subfacp1lem1  34170  subfacp1lem5  34175  gg-iihalf1cn  35167  gg-iihalf2cn  35168  dnibndlem10  35363  knoppndvlem2  35389  knoppndvlem7  35394  knoppndvlem9  35396  knoppndvlem10  35397  knoppndvlem16  35403  irrdifflemf  36206  itg2addnclem  36539  dvasin  36572  areacirclem1  36576  areacirclem3  36578  isbnd2  36651  lcmineqlem21  40914  3lexlogpow2ineq2  40924  dvrelog2b  40931  dvrelogpow2b  40933  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p9  40953  2np3bcnp1  40960  2ap1caineq  40961  oddnumth  41209  nicomachus  41210  sumcubes  41211  remul02  41278  remul01  41280  dffltz  41376  fltne  41386  flt4lem5e  41398  cu3addd  41418  rmspecsqrtnq  41644  rmxluc  41675  rmyluc2  41677  rmydbl  41679  jm2.18  41727  jm2.22  41734  jm2.25  41738  jm2.27c  41746  jm3.1lem2  41757  sqrtcval  42392  imo72b2lem0  42917  refsum2cnlem1  43721  oddfl  43987  xralrple2  44064  infleinflem2  44081  sumnnodd  44346  0ellimcdiv  44365  coseq0  44580  sinmulcos  44581  coskpi2  44582  sinaover2ne0  44584  cosknegpi  44585  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  itgsinexp  44671  stoweidlem1  44717  stoweidlem62  44778  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  dirker2re  44808  dirkerdenne0  44809  dirkerval2  44810  dirkerre  44811  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkeritg  44818  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem43  44866  fourierdlem44  44867  fourierdlem56  44878  fourierdlem57  44879  fourierdlem58  44880  fourierdlem62  44884  fourierdlem66  44888  fourierdlem68  44890  fourierdlem72  44894  fourierdlem76  44898  fourierdlem79  44901  fourierdlem80  44902  fourierdlem83  44905  fourierdlem95  44917  fourierdlem104  44926  fourierdlem112  44934  fouriercnp  44942  fourierswlem  44946  sge0ad2en  45147  hoicvrrex  45272  hoiqssbllem2  45339  fmtnoodd  46201  sqrtpwpw2p  46206  fmtnorec2lem  46210  fmtnodvds  46212  goldbachthlem2  46214  fmtnoprmfac1lem  46232  fmtnoprmfac2  46235  fmtnofac1  46238  2pwp1prm  46257  mod42tp1mod8  46270  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem4  46278  proththd  46282  quad1  46288  requad01  46289  requad1  46290  requad2  46291  dfodd6  46305  dfeven4  46306  enege  46313  onego  46314  dfeven2  46317  oddflALTV  46331  opoeALTV  46351  opeoALTV  46352  nn0onn0exALTV  46367  nn0enn0exALTV  46368  nnennexALTV  46369  mogoldbblem  46388  perfectALTV  46391  fppr2odd  46399  sgoldbeven3prm  46451  0nodd  46580  2nodd  46582  2zlidl  46832  2zrngamgm  46837  2zrngagrp  46841  2zrngmmgm  46844  2zrngnmlid  46847  nn0onn0ex  47209  nn0enn0ex  47210  nnennex  47211  nnpw2even  47215  fldivexpfllog2  47251  blenpw2m1  47265  nnpw2blen  47266  blennn0em1  47277  dig2nn1st  47291  dig2bits  47300  dignn0flhalflem1  47301  dignn0flhalflem2  47302  dignn0ehalf  47303  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  itcovalt2lem2lem2  47360  ackval2  47368  ackval3  47369  itschlc0yqe  47446  itsclc0yqsollem1  47448  itsclc0yqsol  47450  itsclc0xyqsolr  47455  itsclquadb  47462  2itscplem1  47464  2itscplem3  47466  itscnhlinecirc02plem1  47468