Theorem 2cnd 12221

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  2c2 12198

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 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206

This theorem is referenced by:  subhalfhalf  12373  cnm2m1cnm3  12392  xp1d2m1eqxm1d2  12393  zeo2  12577  ge2halflem1  13020  fzosplitprm1  13692  2tnp1ge0ge0  13747  flhalf  13748  2txmodxeq0  13852  mulbinom2  14144  binom3  14145  zesq  14147  expmulnbnd  14156  discr  14161  sqoddm1div8  14164  mulsubdivbinom2  14183  swrds2m  14862  amgm2  15291  bhmafibid1cn  15387  bhmafibid2cn  15388  iseraltlem2  15604  iseralt  15606  trirecip  15784  geo2sum  15794  bpolydiflem  15975  ege2le3  16011  tanval3  16057  sinhval  16077  tanhlt1  16083  sqrt2irrlem  16171  sqrt2irr  16172  even2n  16267  oddm1even  16268  oddp1even  16269  mod2eq1n2dvds  16272  ltoddhalfle  16286  m1exp1  16301  nn0enne  16302  flodddiv4  16340  flodddiv4t2lthalf  16343  bitsp1e  16357  bitsp1o  16358  bitsfzo  16360  bitsmod  16361  bitsinv1lem  16366  sadadd2lem2  16375  sadcaddlem  16382  bitsuz  16399  bitsshft  16400  prmdiv  16710  vfermltlALT  16728  iserodd  16761  4sqlem7  16870  4sqlem10  16873  4sqlem19  16889  prmgaplem7  16983  2expltfac  17018  smndex2dlinvh  18840  efgredlemg  19669  frgpnabllem1  19800  ablsimpgfindlem1  20036  metnrmlem3  24804  iihalf1cn  24880  iihalf1cnOLD  24881  iihalf2cn  24883  iihalf2cnOLD  24884  pcoass  24978  cphipval2  25195  csbren  25353  trirn  25354  minveclem2  25380  ovolunlem1a  25451  uniioombllem5  25542  uniioombl  25544  dyaddisjlem  25550  mbfi1fseqlem5  25674  mbfi1fseqlem6  25675  dvsincos  25939  lhop1  25973  cosargd  26571  dvcnsqrt  26707  root1id  26718  ssscongptld  26786  chordthmlem  26796  chordthmlem2  26797  chordthmlem4  26799  heron  26802  dcubic1  26809  mcubic  26811  cubic2  26812  quartlem4  26824  quart  26825  cosasin  26868  cosatan  26885  atantayl  26901  atantayl2  26902  atantayl3  26903  log2tlbnd  26909  cxp2limlem  26940  divsqrtsumlem  26944  lgamgulmlem2  26994  lgamgulmlem4  26996  lgamucov  27002  ftalem2  27038  basellem2  27046  basellem3  27047  basellem5  27049  basellem8  27052  logfaclbnd  27187  perfectlem2  27195  perfect  27196  bcp1ctr  27244  bposlem1  27249  bposlem2  27250  lgslem1  27262  lgsqrlem2  27312  gausslemma2dlem1a  27330  gausslemma2dlem3  27333  gausslemma2dlem4  27334  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgsquadlem1  27345  lgsquadlem2  27346  lgsquad2lem1  27349  2lgslem1a1  27354  2lgslem1a2  27355  2lgslem1b  27357  2lgslem1c  27358  2lgslem3a1  27365  2lgslem3d1  27368  2sq2  27398  addsq2nreurex  27409  chebbnd1lem3  27436  chto1ub  27441  dchrisumlem2  27455  dchrisum0flblem2  27474  dchrisum0fno1  27476  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2  27483  logdivsum  27498  mulog2sumlem2  27500  vmalogdivsum2  27503  log2sumbnd  27509  selberglem2  27511  chpdifbndlem1  27518  selberg3lem1  27522  selberg3  27524  selberg4lem1  27525  selberg4  27526  selberg4r  27535  selberg34r  27536  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntpbnd1a  27550  pntpbnd2  27552  pntibndlem2  27556  pntlemb  27562  pntlemg  27563  pntlemh  27564  pntlemr  27567  pntlemk  27571  pntlemo  27572  ostth2lem1  27583  finsumvtxdg2ssteplem4  29571  upgrwlkdvdelem  29758  wwlksnextwrd  29919  wwlksnextinj  29921  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a4  30021  clwlkclwwlklem3  30025  clwwlkext2edg  30080  clwwlknonex2lem1  30131  clwwlknonex2lem2  30132  2clwwlk2clwwlk  30374  numclwwlk1lem2foalem  30375  numclwwlk1lem2fo  30382  numclwwlk2lem1  30400  numclwlk2lem2f  30401  numclwwlk2  30405  ex-ind-dvds  30485  nrt2irr  30497  binom2subadd  32770  quad3d  32778  2exple2exp  32875  wrdt2ind  32984  archirngz  33220  archiabllem2c  33226  fldext2rspun  33788  constrrtcc  33841  constrelextdg2  33853  constraddcl  33868  constrrecl  33875  constrresqrtcl  33883  2sqr3nconstr  33887  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  cos9thpiminply  33894  cos9thpinconstrlem1  33895  cos9thpinconstrlem2  33896  cos9thpinconstr  33897  sqsscirc1  34014  dya2icoseg  34383  dya2iocucvr  34390  oddpwdc  34460  eulerpartlemgs2  34486  fibp1  34507  signslema  34668  itgexpif  34712  vtsprod  34745  hgt750lemd  34754  logdivsqrle  34756  subfacp1lem1  35322  subfacp1lem5  35327  dnibndlem10  36630  knoppcnlem10  36645  knoppndvlem2  36656  knoppndvlem7  36661  knoppndvlem9  36663  knoppndvlem10  36664  knoppndvlem16  36670  irrdifflemf  37469  itg2addnclem  37811  dvasin  37844  areacirclem1  37848  areacirclem3  37850  isbnd2  37923  lcmineqlem21  42242  3lexlogpow2ineq2  42252  dvrelog2b  42259  dvrelogpow2b  42261  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p9  42281  posbezout  42293  2np3bcnp1  42337  2ap1caineq  42338  oddnumth  42508  nicomachus  42509  sumcubes  42510  ef11d  42536  cxpi11d  42540  tan3rdpi  42549  readvrec2  42558  remul02  42602  remul01  42604  dffltz  42819  fltne  42829  flt4lem5e  42841  cu3addd  42865  rmspecsqrtnq  43090  rmxluc  43120  rmyluc2  43122  rmydbl  43124  jm2.18  43172  jm2.22  43179  jm2.25  43183  jm2.27c  43191  jm3.1lem2  43202  sqrtcval  43824  imo72b2lem0  44348  refsum2cnlem1  45224  oddfl  45468  xralrple2  45541  infleinflem2  45557  sumnnodd  45818  0ellimcdiv  45835  coseq0  46050  sinmulcos  46051  coskpi2  46052  sinaover2ne0  46054  cosknegpi  46055  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  itgsinexp  46141  stoweidlem1  46187  stoweidlem62  46248  wallispilem4  46254  wallispilem5  46255  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem1  46260  stirlinglem3  46262  stirlinglem4  46263  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem8  46267  stirlinglem10  46269  stirlinglem11  46270  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  dirker2re  46278  dirkerdenne0  46279  dirkerval2  46280  dirkerre  46281  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkeritg  46288  dirkercncflem1  46289  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem43  46336  fourierdlem44  46337  fourierdlem56  46348  fourierdlem57  46349  fourierdlem58  46350  fourierdlem62  46354  fourierdlem66  46358  fourierdlem68  46360  fourierdlem72  46364  fourierdlem76  46368  fourierdlem79  46371  fourierdlem80  46372  fourierdlem83  46375  fourierdlem95  46387  fourierdlem104  46396  fourierdlem112  46404  fouriercnp  46412  fourierswlem  46416  sge0ad2en  46617  hoicvrrex  46742  hoiqssbllem2  46809  2tceilhalfelfzo1  47520  minusmodnep2tmod  47541  modmkpkne  47549  modm2nep1  47554  modm1nem2  47557  fmtnoodd  47721  sqrtpwpw2p  47726  fmtnorec2lem  47730  fmtnodvds  47732  goldbachthlem2  47734  fmtnoprmfac1lem  47752  fmtnoprmfac2  47755  fmtnofac1  47758  2pwp1prm  47777  mod42tp1mod8  47790  sfprmdvdsmersenne  47791  lighneallem2  47794  lighneallem4  47798  proththd  47802  quad1  47808  requad01  47809  requad1  47810  requad2  47811  dfodd6  47825  dfeven4  47826  enege  47833  onego  47834  dfeven2  47837  oddflALTV  47851  opoeALTV  47871  opeoALTV  47872  nn0onn0exALTV  47887  nn0enn0exALTV  47888  nnennexALTV  47889  mogoldbblem  47908  perfectALTV  47911  fppr2odd  47919  sgoldbeven3prm  47971  gpg3nbgrvtx0  48264  gpg3kgrtriexlem2  48272  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  0nodd  48358  2nodd  48360  2zlidl  48428  2zrngamgm  48433  2zrngagrp  48437  2zrngmmgm  48440  2zrngnmlid  48443  nn0onn0ex  48711  nn0enn0ex  48712  nnennex  48713  nnpw2even  48717  fldivexpfllog2  48753  blenpw2m1  48767  nnpw2blen  48768  blennn0em1  48779  dig2nn1st  48793  dig2bits  48802  dignn0flhalflem1  48803  dignn0flhalflem2  48804  dignn0ehalf  48805  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  itcovalt2lem2lem2  48862  ackval2  48870  ackval3  48871  itschlc0yqe  48948  itsclc0yqsollem1  48950  itsclc0yqsol  48952  itsclc0xyqsolr  48957  itsclquadb  48964  2itscplem1  48966  2itscplem3  48968  itscnhlinecirc02plem1  48970