Theorem 2cnd 12235

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  2c2 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220

This theorem is referenced by:  subhalfhalf  12387  cnm2m1cnm3  12406  xp1d2m1eqxm1d2  12407  zeo2  12591  ge2halflem1  13034  fzosplitprm1  13706  2tnp1ge0ge0  13761  flhalf  13762  2txmodxeq0  13866  mulbinom2  14158  binom3  14159  zesq  14161  expmulnbnd  14170  discr  14175  sqoddm1div8  14178  mulsubdivbinom2  14197  swrds2m  14876  amgm2  15305  bhmafibid1cn  15401  bhmafibid2cn  15402  iseraltlem2  15618  iseralt  15620  trirecip  15798  geo2sum  15808  bpolydiflem  15989  ege2le3  16025  tanval3  16071  sinhval  16091  tanhlt1  16097  sqrt2irrlem  16185  sqrt2irr  16186  even2n  16281  oddm1even  16282  oddp1even  16283  mod2eq1n2dvds  16286  ltoddhalfle  16300  m1exp1  16315  nn0enne  16316  flodddiv4  16354  flodddiv4t2lthalf  16357  bitsp1e  16371  bitsp1o  16372  bitsfzo  16374  bitsmod  16375  bitsinv1lem  16380  sadadd2lem2  16389  sadcaddlem  16396  bitsuz  16413  bitsshft  16414  prmdiv  16724  vfermltlALT  16742  iserodd  16775  4sqlem7  16884  4sqlem10  16887  4sqlem19  16903  prmgaplem7  16997  2expltfac  17032  smndex2dlinvh  18854  efgredlemg  19683  frgpnabllem1  19814  ablsimpgfindlem1  20050  metnrmlem3  24818  iihalf1cn  24894  iihalf1cnOLD  24895  iihalf2cn  24897  iihalf2cnOLD  24898  pcoass  24992  cphipval2  25209  csbren  25367  trirn  25368  minveclem2  25394  ovolunlem1a  25465  uniioombllem5  25556  uniioombl  25558  dyaddisjlem  25564  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  dvsincos  25953  lhop1  25987  cosargd  26585  dvcnsqrt  26721  root1id  26732  ssscongptld  26800  chordthmlem  26810  chordthmlem2  26811  chordthmlem4  26813  heron  26816  dcubic1  26823  mcubic  26825  cubic2  26826  quartlem4  26838  quart  26839  cosasin  26882  cosatan  26899  atantayl  26915  atantayl2  26916  atantayl3  26917  log2tlbnd  26923  cxp2limlem  26954  divsqrtsumlem  26958  lgamgulmlem2  27008  lgamgulmlem4  27010  lgamucov  27016  ftalem2  27052  basellem2  27060  basellem3  27061  basellem5  27063  basellem8  27066  logfaclbnd  27201  perfectlem2  27209  perfect  27210  bcp1ctr  27258  bposlem1  27263  bposlem2  27264  lgslem1  27276  lgsqrlem2  27326  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  gausslemma2dlem4  27348  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem1  27363  2lgslem1a1  27368  2lgslem1a2  27369  2lgslem1b  27371  2lgslem1c  27372  2lgslem3a1  27379  2lgslem3d1  27382  2sq2  27412  addsq2nreurex  27423  chebbnd1lem3  27450  chto1ub  27455  dchrisumlem2  27469  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2  27497  logdivsum  27512  mulog2sumlem2  27514  vmalogdivsum2  27517  log2sumbnd  27523  selberglem2  27525  chpdifbndlem1  27532  selberg3lem1  27536  selberg3  27538  selberg4lem1  27539  selberg4  27540  selberg4r  27549  selberg34r  27550  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem2  27570  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemr  27581  pntlemk  27585  pntlemo  27586  ostth2lem1  27597  finsumvtxdg2ssteplem4  29634  upgrwlkdvdelem  29821  wwlksnextwrd  29982  wwlksnextinj  29984  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a4  30084  clwlkclwwlklem3  30088  clwwlkext2edg  30143  clwwlknonex2lem1  30194  clwwlknonex2lem2  30195  2clwwlk2clwwlk  30437  numclwwlk1lem2foalem  30438  numclwwlk1lem2fo  30445  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwwlk2  30468  ex-ind-dvds  30548  nrt2irr  30560  binom2subadd  32832  quad3d  32840  2exple2exp  32937  wrdt2ind  33046  archirngz  33283  archiabllem2c  33289  fldext2rspun  33860  constrrtcc  33913  constrelextdg2  33925  constraddcl  33940  constrrecl  33947  constrresqrtcl  33955  2sqr3nconstr  33959  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  cos9thpinconstr  33969  sqsscirc1  34086  dya2icoseg  34455  dya2iocucvr  34462  oddpwdc  34532  eulerpartlemgs2  34558  fibp1  34579  signslema  34740  itgexpif  34784  vtsprod  34817  hgt750lemd  34826  logdivsqrle  34828  subfacp1lem1  35395  subfacp1lem5  35400  dnibndlem10  36709  knoppcnlem10  36724  knoppndvlem2  36735  knoppndvlem7  36740  knoppndvlem9  36742  knoppndvlem10  36743  knoppndvlem16  36749  irrdifflemf  37580  itg2addnclem  37922  dvasin  37955  areacirclem1  37959  areacirclem3  37961  isbnd2  38034  lcmineqlem21  42419  3lexlogpow2ineq2  42429  dvrelog2b  42436  dvrelogpow2b  42438  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p9  42458  posbezout  42470  2np3bcnp1  42514  2ap1caineq  42515  oddnumth  42681  nicomachus  42682  sumcubes  42683  ef11d  42709  cxpi11d  42713  tan3rdpi  42722  readvrec2  42731  remul02  42775  remul01  42777  dffltz  42992  fltne  43002  flt4lem5e  43014  cu3addd  43038  rmspecsqrtnq  43263  rmxluc  43293  rmyluc2  43295  rmydbl  43297  jm2.18  43345  jm2.22  43352  jm2.25  43356  jm2.27c  43364  jm3.1lem2  43375  sqrtcval  43997  imo72b2lem0  44521  refsum2cnlem1  45397  oddfl  45640  xralrple2  45713  infleinflem2  45729  sumnnodd  45990  0ellimcdiv  46007  coseq0  46222  sinmulcos  46223  coskpi2  46224  sinaover2ne0  46226  cosknegpi  46227  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  itgsinexp  46313  stoweidlem1  46359  stoweidlem62  46420  wallispilem4  46426  wallispilem5  46427  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  stirlinglem4  46435  stirlinglem5  46436  stirlinglem6  46437  stirlinglem7  46438  stirlinglem8  46439  stirlinglem10  46441  stirlinglem11  46442  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  dirker2re  46450  dirkerdenne0  46451  dirkerval2  46452  dirkerre  46453  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkertrigeq  46459  dirkeritg  46460  dirkercncflem1  46461  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem43  46508  fourierdlem44  46509  fourierdlem56  46520  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fourierdlem66  46530  fourierdlem68  46532  fourierdlem72  46536  fourierdlem76  46540  fourierdlem79  46543  fourierdlem80  46544  fourierdlem83  46547  fourierdlem95  46559  fourierdlem104  46568  fourierdlem112  46576  fouriercnp  46584  fourierswlem  46588  sge0ad2en  46789  hoicvrrex  46914  hoiqssbllem2  46981  2tceilhalfelfzo1  47692  minusmodnep2tmod  47713  modmkpkne  47721  modm2nep1  47726  modm1nem2  47729  fmtnoodd  47893  sqrtpwpw2p  47898  fmtnorec2lem  47902  fmtnodvds  47904  goldbachthlem2  47906  fmtnoprmfac1lem  47924  fmtnoprmfac2  47927  fmtnofac1  47930  2pwp1prm  47949  mod42tp1mod8  47962  sfprmdvdsmersenne  47963  lighneallem2  47966  lighneallem4  47970  proththd  47974  quad1  47980  requad01  47981  requad1  47982  requad2  47983  dfodd6  47997  dfeven4  47998  enege  48005  onego  48006  dfeven2  48009  oddflALTV  48023  opoeALTV  48043  opeoALTV  48044  nn0onn0exALTV  48059  nn0enn0exALTV  48060  nnennexALTV  48061  mogoldbblem  48080  perfectALTV  48083  fppr2odd  48091  sgoldbeven3prm  48143  gpg3nbgrvtx0  48436  gpg3kgrtriexlem2  48444  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  0nodd  48530  2nodd  48532  2zlidl  48600  2zrngamgm  48605  2zrngagrp  48609  2zrngmmgm  48612  2zrngnmlid  48615  nn0onn0ex  48883  nn0enn0ex  48884  nnennex  48885  nnpw2even  48889  fldivexpfllog2  48925  blenpw2m1  48939  nnpw2blen  48940  blennn0em1  48951  dig2nn1st  48965  dig2bits  48974  dignn0flhalflem1  48975  dignn0flhalflem2  48976  dignn0ehalf  48977  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  itcovalt2lem2lem2  49034  ackval2  49042  ackval3  49043  itschlc0yqe  49120  itsclc0yqsollem1  49122  itsclc0yqsol  49124  itsclc0xyqsolr  49129  itsclquadb  49136  2itscplem1  49138  2itscplem3  49140  itscnhlinecirc02plem1  49142