Theorem 2cnd 12341

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-2 12326

This theorem is referenced by:  subhalfhalf  12497  cnm2m1cnm3  12516  xp1d2m1eqxm1d2  12517  zeo2  12702  ge2halflem1  13147  fzosplitprm1  13812  2tnp1ge0ge0  13865  flhalf  13866  2txmodxeq0  13968  mulbinom2  14258  binom3  14259  zesq  14261  expmulnbnd  14270  discr  14275  sqoddm1div8  14278  mulsubdivbinom2  14297  swrds2m  14976  amgm2  15404  bhmafibid1cn  15498  bhmafibid2cn  15499  iseraltlem2  15715  iseralt  15717  trirecip  15895  geo2sum  15905  bpolydiflem  16086  ege2le3  16122  tanval3  16166  sinhval  16186  tanhlt1  16192  sqrt2irrlem  16280  sqrt2irr  16281  even2n  16375  oddm1even  16376  oddp1even  16377  mod2eq1n2dvds  16380  ltoddhalfle  16394  m1exp1  16409  nn0enne  16410  flodddiv4  16448  flodddiv4t2lthalf  16451  bitsp1e  16465  bitsp1o  16466  bitsfzo  16468  bitsmod  16469  bitsinv1lem  16474  sadadd2lem2  16483  sadcaddlem  16490  bitsuz  16507  bitsshft  16508  prmdiv  16818  vfermltlALT  16835  iserodd  16868  4sqlem7  16977  4sqlem10  16980  4sqlem19  16996  prmgaplem7  17090  2expltfac  17126  smndex2dlinvh  18942  efgredlemg  19774  frgpnabllem1  19905  ablsimpgfindlem1  20141  metnrmlem3  24896  iihalf1cn  24972  iihalf1cnOLD  24973  iihalf2cn  24975  iihalf2cnOLD  24976  pcoass  25070  cphipval2  25288  csbren  25446  trirn  25447  minveclem2  25473  ovolunlem1a  25544  uniioombllem5  25635  uniioombl  25637  dyaddisjlem  25643  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  dvsincos  26033  lhop1  26067  cosargd  26664  dvcnsqrt  26800  root1id  26811  ssscongptld  26879  chordthmlem  26889  chordthmlem2  26890  chordthmlem4  26892  heron  26895  dcubic1  26902  mcubic  26904  cubic2  26905  quartlem4  26917  quart  26918  cosasin  26961  cosatan  26978  atantayl  26994  atantayl2  26995  atantayl3  26996  log2tlbnd  27002  cxp2limlem  27033  divsqrtsumlem  27037  lgamgulmlem2  27087  lgamgulmlem4  27089  lgamucov  27095  ftalem2  27131  basellem2  27139  basellem3  27140  basellem5  27142  basellem8  27145  logfaclbnd  27280  perfectlem2  27288  perfect  27289  bcp1ctr  27337  bposlem1  27342  bposlem2  27343  lgslem1  27355  lgsqrlem2  27405  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  gausslemma2dlem4  27427  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem1  27442  2lgslem1a1  27447  2lgslem1a2  27448  2lgslem1b  27450  2lgslem1c  27451  2lgslem3a1  27458  2lgslem3d1  27461  2sq2  27491  addsq2nreurex  27502  chebbnd1lem3  27529  chto1ub  27534  dchrisumlem2  27548  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2  27576  logdivsum  27591  mulog2sumlem2  27593  vmalogdivsum2  27596  log2sumbnd  27602  selberglem2  27604  chpdifbndlem1  27611  selberg3lem1  27615  selberg3  27617  selberg4lem1  27618  selberg4  27619  selberg4r  27628  selberg34r  27629  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemr  27660  pntlemk  27664  pntlemo  27665  ostth2lem1  27676  finsumvtxdg2ssteplem4  29580  upgrwlkdvdelem  29768  wwlksnextwrd  29926  wwlksnextinj  29928  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a4  30025  clwlkclwwlklem3  30029  clwwlkext2edg  30084  clwwlknonex2lem1  30135  clwwlknonex2lem2  30136  2clwwlk2clwwlk  30378  numclwwlk1lem2foalem  30379  numclwwlk1lem2fo  30386  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwwlk2  30409  ex-ind-dvds  30489  nrt2irr  30501  quad3d  32760  wrdt2ind  32922  archirngz  33178  archiabllem2c  33184  fldext2chn  33733  constrrtcc  33740  constrelextdg2  33751  sqsscirc1  33868  dya2icoseg  34258  dya2iocucvr  34265  oddpwdc  34335  eulerpartlemgs2  34361  fibp1  34382  signslema  34555  itgexpif  34599  vtsprod  34632  hgt750lemd  34641  logdivsqrle  34643  subfacp1lem1  35163  subfacp1lem5  35168  dnibndlem10  36469  knoppcnlem10  36484  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem9  36502  knoppndvlem10  36503  knoppndvlem16  36509  irrdifflemf  37307  itg2addnclem  37657  dvasin  37690  areacirclem1  37694  areacirclem3  37696  isbnd2  37769  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  42323  nicomachus  42324  sumcubes  42325  ef11d  42353  cxpi11d  42357  tan3rdpi  42364  readvrec2  42369  remul02  42411  remul01  42413  dffltz  42620  fltne  42630  flt4lem5e  42642  cu3addd  42667  rmspecsqrtnq  42893  rmxluc  42924  rmyluc2  42926  rmydbl  42928  jm2.18  42976  jm2.22  42983  jm2.25  42987  jm2.27c  42995  jm3.1lem2  43006  sqrtcval  43630  imo72b2lem0  44154  refsum2cnlem1  44974  oddfl  45227  xralrple2  45303  infleinflem2  45320  sumnnodd  45585  0ellimcdiv  45604  coseq0  45819  sinmulcos  45820  coskpi2  45821  sinaover2ne0  45823  cosknegpi  45824  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  itgsinexp  45910  stoweidlem1  45956  stoweidlem62  46017  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirker2re  46047  dirkerdenne0  46048  dirkerval2  46049  dirkerre  46050  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkeritg  46057  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem43  46105  fourierdlem44  46106  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem66  46127  fourierdlem68  46129  fourierdlem72  46133  fourierdlem76  46137  fourierdlem79  46140  fourierdlem80  46141  fourierdlem83  46144  fourierdlem95  46156  fourierdlem104  46165  fourierdlem112  46173  fouriercnp  46181  fourierswlem  46185  sge0ad2en  46386  hoicvrrex  46511  hoiqssbllem2  46578  minusmodnep2tmod  47292  fmtnoodd  47457  sqrtpwpw2p  47462  fmtnorec2lem  47466  fmtnodvds  47468  goldbachthlem2  47470  fmtnoprmfac1lem  47488  fmtnoprmfac2  47491  fmtnofac1  47494  2pwp1prm  47513  mod42tp1mod8  47526  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem4  47534  proththd  47538  quad1  47544  requad01  47545  requad1  47546  requad2  47547  dfodd6  47561  dfeven4  47562  enege  47569  onego  47570  dfeven2  47573  oddflALTV  47587  opoeALTV  47607  opeoALTV  47608  nn0onn0exALTV  47623  nn0enn0exALTV  47624  nnennexALTV  47625  mogoldbblem  47644  perfectALTV  47647  fppr2odd  47655  sgoldbeven3prm  47707  2tceilhalfelfzo1  47952  gpg3nbgrvtx0  47966  0nodd  48013  2nodd  48015  2zlidl  48083  2zrngamgm  48088  2zrngagrp  48092  2zrngmmgm  48095  2zrngnmlid  48098  nn0onn0ex  48372  nn0enn0ex  48373  nnennex  48374  nnpw2even  48378  fldivexpfllog2  48414  blenpw2m1  48428  nnpw2blen  48429  blennn0em1  48440  dig2nn1st  48454  dig2bits  48463  dignn0flhalflem1  48464  dignn0flhalflem2  48465  dignn0ehalf  48466  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  itcovalt2lem2lem2  48523  ackval2  48531  ackval3  48532  itschlc0yqe  48609  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itsclc0xyqsolr  48618  itsclquadb  48625  2itscplem1  48627  2itscplem3  48629  itscnhlinecirc02plem1  48631