Theorem 2cnd 11511

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

Syntax hints:   → wi 4   ∈ wcel 2048  ℂcc 10325  2c2 11488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745  ax-1cn 10385  ax-addcl 10387

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840  df-2 11496

This theorem is referenced by:  subhalfhalf  11674  cnm2m1cnm3  11693  xp1d2m1eqxm1d2  11694  zeo2  11875  fzosplitprm1  12955  2tnp1ge0ge0  13007  flhalf  13008  2txmodxeq0  13107  mulbinom2  13392  binom3  13393  zesq  13395  expmulnbnd  13404  discr  13409  sqoddm1div8  13412  mulsubdivbinom2  13430  swrds2m  14155  amgm2  14580  bhmafibid1cn  14674  bhmafibid2cn  14675  iseraltlem2  14890  iseralt  14892  trirecip  15068  geo2sum  15079  bpolydiflem  15258  ege2le3  15293  tanval3  15337  sinhval  15357  tanhlt1  15363  sqrt2irrlem  15451  sqrt2irr  15452  even2n  15541  oddm1even  15542  oddp1even  15543  mod2eq1n2dvds  15546  ltoddhalfle  15560  m1exp1  15577  nn0enne  15578  flodddiv4  15614  flodddiv4t2lthalf  15617  bitsp1e  15631  bitsp1o  15632  bitsfzo  15634  bitsmod  15635  bitsinv1lem  15640  sadadd2lem2  15649  sadcaddlem  15656  bitsuz  15673  bitsshft  15674  prmdiv  15968  vfermltlALT  15985  iserodd  16018  4sqlem7  16126  4sqlem10  16129  4sqlem19  16145  prmgaplem7  16239  2expltfac  16272  efgredlemg  18617  frgpnabllem1  18739  metnrmlem3  23162  iihalf1cn  23229  iihalf2cn  23231  pcoass  23321  cphipval2  23537  csbren  23695  trirn  23696  minveclem2  23722  ovolunlem1a  23790  uniioombllem5  23881  uniioombl  23883  dyaddisjlem  23889  mbfi1fseqlem5  24013  mbfi1fseqlem6  24014  dvsincos  24271  lhop1  24304  cosargd  24882  dvcnsqrt  25016  root1id  25026  ssscongptld  25091  chordthmlem  25101  chordthmlem2  25102  chordthmlem4  25104  heron  25107  dcubic1  25114  mcubic  25116  cubic2  25117  quartlem4  25129  quart  25130  cosasin  25173  cosatan  25190  atantayl  25206  atantayl2  25207  atantayl3  25208  log2tlbnd  25215  cxp2limlem  25245  divsqrtsumlem  25249  lgamgulmlem2  25299  lgamgulmlem4  25301  lgamucov  25307  ftalem2  25343  basellem2  25351  basellem3  25352  basellem5  25354  basellem8  25357  logfaclbnd  25490  perfectlem2  25498  perfect  25499  bcp1ctr  25547  bposlem1  25552  bposlem2  25553  lgslem1  25565  lgsqrlem2  25615  gausslemma2dlem1a  25633  gausslemma2dlem3  25636  gausslemma2dlem4  25637  lgseisenlem1  25643  lgseisenlem2  25644  lgseisenlem3  25645  lgseisenlem4  25646  lgsquadlem1  25648  lgsquadlem2  25649  lgsquad2lem1  25652  2lgslem1a1  25657  2lgslem1a2  25658  2lgslem1b  25660  2lgslem1c  25661  2lgslem3a1  25668  2lgslem3d1  25671  2sq2  25701  addsq2nreurex  25712  chebbnd1lem3  25739  chto1ub  25744  dchrisumlem2  25758  dchrisum0flblem2  25777  dchrisum0fno1  25779  dchrisum0lem1b  25783  dchrisum0lem1  25784  dchrisum0lem2  25786  logdivsum  25801  mulog2sumlem2  25803  vmalogdivsum2  25806  log2sumbnd  25812  selberglem2  25814  chpdifbndlem1  25821  selberg3lem1  25825  selberg3  25827  selberg4lem1  25828  selberg4  25829  selberg4r  25838  selberg34r  25839  pntrlog2bndlem3  25847  pntrlog2bndlem4  25848  pntrlog2bndlem5  25849  pntrlog2bndlem6  25851  pntpbnd1a  25853  pntpbnd2  25855  pntibndlem2  25859  pntlemb  25865  pntlemg  25866  pntlemh  25867  pntlemr  25870  pntlemk  25874  pntlemo  25875  ostth2lem1  25886  finsumvtxdg2ssteplem4  27023  upgrwlkdvdelem  27215  wwlksnextwrd  27378  wwlksnextinj  27380  wwlksnextwrdOLD  27383  wwlksnextinjOLD  27385  clwlkclwwlklem2a1  27488  clwlkclwwlklem2a4  27493  clwlkclwwlklem3  27497  clwwlkext2edg  27569  clwwlknonex2lem1  27625  clwwlknonex2lem2  27626  2clwwlk2clwwlk  27877  2clwwlk2clwwlkOLD  27878  numclwwlk1lem2foalem  27879  numclwwlk1lem2foalemOLD  27880  numclwwlk1lem2fo  27890  numclwwlk1lem2foOLD  27895  numclwwlk2lem1  27919  numclwlk2lem2f  27920  numclwlk2lem2fOLD  27923  numclwwlk2  27928  ex-ind-dvds  28008  archirngz  30440  archiabllem2c  30446  sqsscirc1  30752  dya2icoseg  31137  dya2iocucvr  31144  oddpwdc  31214  eulerpartlemgs2  31240  fibp1  31262  signslema  31439  itgexpif  31486  vtsprod  31519  hgt750lemd  31528  logdivsqrle  31530  subfacp1lem1  31971  subfacp1lem5  31976  dnibndlem10  33286  knoppndvlem2  33312  knoppndvlem7  33317  knoppndvlem9  33319  knoppndvlem10  33320  knoppndvlem16  33326  itg2addnclem  34332  dvasin  34367  areacirclem1  34371  areacirclem3  34373  isbnd2  34451  dffltz  38623  fltne  38624  rmspecsqrtnq  38844  rmxluc  38874  rmyluc2  38876  rmydbl  38878  jm2.18  38926  jm2.22  38933  jm2.25  38937  jm2.27c  38945  jm3.1lem2  38956  imo72b2lem0  39825  ablsimpgfindlem1  39988  refsum2cnlem1  40657  oddfl  40918  xralrple2  40997  infleinflem2  41014  sumnnodd  41288  0ellimcdiv  41307  coseq0  41521  sinmulcos  41522  coskpi2  41523  sinaover2ne0  41525  cosknegpi  41526  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  itgsinexp  41616  stoweidlem1  41663  stoweidlem62  41724  wallispilem4  41730  wallispilem5  41731  wallispi  41732  wallispi2lem1  41733  wallispi2lem2  41734  wallispi2  41735  stirlinglem1  41736  stirlinglem3  41738  stirlinglem4  41739  stirlinglem5  41740  stirlinglem6  41741  stirlinglem7  41742  stirlinglem8  41743  stirlinglem10  41745  stirlinglem11  41746  stirlinglem13  41748  stirlinglem14  41749  stirlinglem15  41750  dirker2re  41754  dirkerdenne0  41755  dirkerval2  41756  dirkerre  41757  dirkertrigeqlem1  41760  dirkertrigeqlem2  41761  dirkertrigeqlem3  41762  dirkertrigeq  41763  dirkeritg  41764  dirkercncflem1  41765  dirkercncflem2  41766  dirkercncflem4  41768  fourierdlem43  41812  fourierdlem44  41813  fourierdlem56  41824  fourierdlem57  41825  fourierdlem58  41826  fourierdlem62  41830  fourierdlem66  41834  fourierdlem68  41836  fourierdlem72  41840  fourierdlem76  41844  fourierdlem79  41847  fourierdlem80  41848  fourierdlem83  41851  fourierdlem95  41863  fourierdlem104  41872  fourierdlem112  41880  fouriercnp  41888  fourierswlem  41892  sge0ad2en  42090  hoicvrrex  42215  hoiqssbllem2  42282  fmtnoodd  43003  sqrtpwpw2p  43008  fmtnorec2lem  43012  fmtnodvds  43014  goldbachthlem2  43016  fmtnoprmfac1lem  43034  fmtnoprmfac2  43037  fmtnofac1  43040  2pwp1prm  43059  mod42tp1mod8  43075  sfprmdvdsmersenne  43076  lighneallem2  43079  lighneallem4  43083  proththd  43087  quad1  43093  requad01  43094  requad1  43095  requad2  43096  dfodd6  43110  dfeven4  43111  enege  43118  onego  43119  dfeven2  43122  oddflALTV  43136  opoeALTV  43156  opeoALTV  43157  nn0onn0exALTV  43172  nn0enn0exALTV  43173  nnennexALTV  43174  mogoldbblem  43193  perfectALTV  43196  fppr2odd  43204  sgoldbeven3prm  43256  0nodd  43385  2nodd  43387  2zlidl  43509  2zrngamgm  43514  2zrngagrp  43518  2zrngmmgm  43521  2zrngnmlid  43524  nn0onn0ex  43891  nn0enn0ex  43892  nnennex  43893  nnpw2even  43897  fldivexpfllog2  43933  blenpw2m1  43947  nnpw2blen  43948  blennn0em1  43959  dig2nn1st  43973  dig2bits  43982  dignn0flhalflem1  43983  dignn0flhalflem2  43984  dignn0ehalf  43985  nn0sumshdiglemA  43987  nn0sumshdiglemB  43988  itschlc0yqe  44055  itsclc0yqsollem1  44057  itsclc0yqsol  44059  itsclc0xyqsolr  44064  itsclquadb  44071  2itscplem1  44073  2itscplem3  44075  itscnhlinecirc02plem1  44077