Theorem 2cnd 12240

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  2c2 12217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225

This theorem is referenced by:  subhalfhalf  12392  cnm2m1cnm3  12411  xp1d2m1eqxm1d2  12412  zeo2  12597  ge2halflem1  13044  fzosplitprm1  13714  2tnp1ge0ge0  13767  flhalf  13768  2txmodxeq0  13872  mulbinom2  14164  binom3  14165  zesq  14167  expmulnbnd  14176  discr  14181  sqoddm1div8  14184  mulsubdivbinom2  14203  swrds2m  14883  amgm2  15312  bhmafibid1cn  15408  bhmafibid2cn  15409  iseraltlem2  15625  iseralt  15627  trirecip  15805  geo2sum  15815  bpolydiflem  15996  ege2le3  16032  tanval3  16078  sinhval  16098  tanhlt1  16104  sqrt2irrlem  16192  sqrt2irr  16193  even2n  16288  oddm1even  16289  oddp1even  16290  mod2eq1n2dvds  16293  ltoddhalfle  16307  m1exp1  16322  nn0enne  16323  flodddiv4  16361  flodddiv4t2lthalf  16364  bitsp1e  16378  bitsp1o  16379  bitsfzo  16381  bitsmod  16382  bitsinv1lem  16387  sadadd2lem2  16396  sadcaddlem  16403  bitsuz  16420  bitsshft  16421  prmdiv  16731  vfermltlALT  16749  iserodd  16782  4sqlem7  16891  4sqlem10  16894  4sqlem19  16910  prmgaplem7  17004  2expltfac  17039  smndex2dlinvh  18826  efgredlemg  19656  frgpnabllem1  19787  ablsimpgfindlem1  20023  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  29529  upgrwlkdvdelem  29716  wwlksnextwrd  29877  wwlksnextinj  29879  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a4  29976  clwlkclwwlklem3  29980  clwwlkext2edg  30035  clwwlknonex2lem1  30086  clwwlknonex2lem2  30087  2clwwlk2clwwlk  30329  numclwwlk1lem2foalem  30330  numclwwlk1lem2fo  30337  numclwwlk2lem1  30355  numclwlk2lem2f  30356  numclwwlk2  30360  ex-ind-dvds  30440  nrt2irr  30452  binom2subadd  32715  quad3d  32723  2exple2exp  32820  wrdt2ind  32925  archirngz  33158  archiabllem2c  33164  fldext2rspun  33670  constrrtcc  33718  constrelextdg2  33730  constraddcl  33745  constrrecl  33752  constrresqrtcl  33760  2sqr3nconstr  33764  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpiminply  33771  cos9thpinconstrlem1  33772  cos9thpinconstrlem2  33773  cos9thpinconstr  33774  sqsscirc1  33891  dya2icoseg  34261  dya2iocucvr  34268  oddpwdc  34338  eulerpartlemgs2  34364  fibp1  34385  signslema  34546  itgexpif  34590  vtsprod  34623  hgt750lemd  34632  logdivsqrle  34634  subfacp1lem1  35159  subfacp1lem5  35164  dnibndlem10  36468  knoppcnlem10  36483  knoppndvlem2  36494  knoppndvlem7  36499  knoppndvlem9  36501  knoppndvlem10  36502  knoppndvlem16  36508  irrdifflemf  37306  itg2addnclem  37658  dvasin  37691  areacirclem1  37695  areacirclem3  37697  isbnd2  37770  lcmineqlem21  42030  3lexlogpow2ineq2  42040  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p9  42069  posbezout  42081  2np3bcnp1  42125  2ap1caineq  42126  oddnumth  42292  nicomachus  42293  sumcubes  42294  ef11d  42320  cxpi11d  42324  tan3rdpi  42333  readvrec2  42342  remul02  42386  remul01  42388  dffltz  42615  fltne  42625  flt4lem5e  42637  cu3addd  42662  rmspecsqrtnq  42887  rmxluc  42918  rmyluc2  42920  rmydbl  42922  jm2.18  42970  jm2.22  42977  jm2.25  42981  jm2.27c  42989  jm3.1lem2  43000  sqrtcval  43623  imo72b2lem0  44147  refsum2cnlem1  45024  oddfl  45269  xralrple2  45343  infleinflem2  45360  sumnnodd  45621  0ellimcdiv  45640  coseq0  45855  sinmulcos  45856  coskpi2  45857  sinaover2ne0  45859  cosknegpi  45860  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  itgsinexp  45946  stoweidlem1  45992  stoweidlem62  46053  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem4  46068  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem8  46072  stirlinglem10  46074  stirlinglem11  46075  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  dirker2re  46083  dirkerdenne0  46084  dirkerval2  46085  dirkerre  46086  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkeritg  46093  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem43  46141  fourierdlem44  46142  fourierdlem56  46153  fourierdlem57  46154  fourierdlem58  46155  fourierdlem62  46159  fourierdlem66  46163  fourierdlem68  46165  fourierdlem72  46169  fourierdlem76  46173  fourierdlem79  46176  fourierdlem80  46177  fourierdlem83  46180  fourierdlem95  46192  fourierdlem104  46201  fourierdlem112  46209  fouriercnp  46217  fourierswlem  46221  sge0ad2en  46422  hoicvrrex  46547  hoiqssbllem2  46614  2tceilhalfelfzo1  47326  minusmodnep2tmod  47347  modmkpkne  47355  modm2nep1  47360  modm1nem2  47363  fmtnoodd  47527  sqrtpwpw2p  47532  fmtnorec2lem  47536  fmtnodvds  47538  goldbachthlem2  47540  fmtnoprmfac1lem  47558  fmtnoprmfac2  47561  fmtnofac1  47564  2pwp1prm  47583  mod42tp1mod8  47596  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem4  47604  proththd  47608  quad1  47614  requad01  47615  requad1  47616  requad2  47617  dfodd6  47631  dfeven4  47632  enege  47639  onego  47640  dfeven2  47643  oddflALTV  47657  opoeALTV  47677  opeoALTV  47678  nn0onn0exALTV  47693  nn0enn0exALTV  47694  nnennexALTV  47695  mogoldbblem  47714  perfectALTV  47717  fppr2odd  47725  sgoldbeven3prm  47777  gpg3nbgrvtx0  48060  gpg3kgrtriexlem2  48068  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  0nodd  48151  2nodd  48153  2zlidl  48221  2zrngamgm  48226  2zrngagrp  48230  2zrngmmgm  48233  2zrngnmlid  48236  nn0onn0ex  48505  nn0enn0ex  48506  nnennex  48507  nnpw2even  48511  fldivexpfllog2  48547  blenpw2m1  48561  nnpw2blen  48562  blennn0em1  48573  dig2nn1st  48587  dig2bits  48596  dignn0flhalflem1  48597  dignn0flhalflem2  48598  dignn0ehalf  48599  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  itcovalt2lem2lem2  48656  ackval2  48664  ackval3  48665  itschlc0yqe  48742  itsclc0yqsollem1  48744  itsclc0yqsol  48746  itsclc0xyqsolr  48751  itsclquadb  48758  2itscplem1  48760  2itscplem3  48762  itscnhlinecirc02plem1  48764