Theorem 2cnd 12287

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11105  2c2 12264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-addcl 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12272

This theorem is referenced by:  subhalfhalf  12443  cnm2m1cnm3  12462  xp1d2m1eqxm1d2  12463  zeo2  12646  fzosplitprm1  13739  2tnp1ge0ge0  13791  flhalf  13792  2txmodxeq0  13893  mulbinom2  14183  binom3  14184  zesq  14186  expmulnbnd  14195  discr  14200  sqoddm1div8  14203  mulsubdivbinom2  14219  swrds2m  14889  amgm2  15313  bhmafibid1cn  15407  bhmafibid2cn  15408  iseraltlem2  15626  iseralt  15628  trirecip  15806  geo2sum  15816  bpolydiflem  15995  ege2le3  16030  tanval3  16074  sinhval  16094  tanhlt1  16100  sqrt2irrlem  16188  sqrt2irr  16189  even2n  16282  oddm1even  16283  oddp1even  16284  mod2eq1n2dvds  16287  ltoddhalfle  16301  m1exp1  16316  nn0enne  16317  flodddiv4  16353  flodddiv4t2lthalf  16356  bitsp1e  16370  bitsp1o  16371  bitsfzo  16373  bitsmod  16374  bitsinv1lem  16379  sadadd2lem2  16388  sadcaddlem  16395  bitsuz  16412  bitsshft  16413  prmdiv  16715  vfermltlALT  16732  iserodd  16765  4sqlem7  16874  4sqlem10  16877  4sqlem19  16893  prmgaplem7  16987  2expltfac  17023  smndex2dlinvh  18795  efgredlemg  19605  frgpnabllem1  19736  ablsimpgfindlem1  19972  metnrmlem3  24369  iihalf1cn  24440  iihalf2cn  24442  pcoass  24532  cphipval2  24750  csbren  24908  trirn  24909  minveclem2  24935  ovolunlem1a  25005  uniioombllem5  25096  uniioombl  25098  dyaddisjlem  25104  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  dvsincos  25490  lhop1  25523  cosargd  26108  dvcnsqrt  26242  root1id  26252  ssscongptld  26317  chordthmlem  26327  chordthmlem2  26328  chordthmlem4  26330  heron  26333  dcubic1  26340  mcubic  26342  cubic2  26343  quartlem4  26355  quart  26356  cosasin  26399  cosatan  26416  atantayl  26432  atantayl2  26433  atantayl3  26434  log2tlbnd  26440  cxp2limlem  26470  divsqrtsumlem  26474  lgamgulmlem2  26524  lgamgulmlem4  26526  lgamucov  26532  ftalem2  26568  basellem2  26576  basellem3  26577  basellem5  26579  basellem8  26582  logfaclbnd  26715  perfectlem2  26723  perfect  26724  bcp1ctr  26772  bposlem1  26777  bposlem2  26778  lgslem1  26790  lgsqrlem2  26840  gausslemma2dlem1a  26858  gausslemma2dlem3  26861  gausslemma2dlem4  26862  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgseisenlem4  26871  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem1  26877  2lgslem1a1  26882  2lgslem1a2  26883  2lgslem1b  26885  2lgslem1c  26886  2lgslem3a1  26893  2lgslem3d1  26896  2sq2  26926  addsq2nreurex  26937  chebbnd1lem3  26964  chto1ub  26969  dchrisumlem2  26983  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2  27011  logdivsum  27026  mulog2sumlem2  27028  vmalogdivsum2  27031  log2sumbnd  27037  selberglem2  27039  chpdifbndlem1  27046  selberg3lem1  27050  selberg3  27052  selberg4lem1  27053  selberg4  27054  selberg4r  27063  selberg34r  27064  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem2  27084  pntlemb  27090  pntlemg  27091  pntlemh  27092  pntlemr  27095  pntlemk  27099  pntlemo  27100  ostth2lem1  27111  finsumvtxdg2ssteplem4  28795  upgrwlkdvdelem  28983  wwlksnextwrd  29141  wwlksnextinj  29143  clwlkclwwlklem2a1  29235  clwlkclwwlklem2a4  29240  clwlkclwwlklem3  29244  clwwlkext2edg  29299  clwwlknonex2lem1  29350  clwwlknonex2lem2  29351  2clwwlk2clwwlk  29593  numclwwlk1lem2foalem  29594  numclwwlk1lem2fo  29601  numclwwlk2lem1  29619  numclwlk2lem2f  29620  numclwwlk2  29624  ex-ind-dvds  29704  wrdt2ind  32105  archirngz  32323  archiabllem2c  32329  sqsscirc1  32877  dya2icoseg  33265  dya2iocucvr  33272  oddpwdc  33342  eulerpartlemgs2  33368  fibp1  33389  signslema  33562  itgexpif  33607  vtsprod  33640  hgt750lemd  33649  logdivsqrle  33651  subfacp1lem1  34159  subfacp1lem5  34164  gg-iihalf1cn  35156  gg-iihalf2cn  35157  dnibndlem10  35352  knoppndvlem2  35378  knoppndvlem7  35383  knoppndvlem9  35385  knoppndvlem10  35386  knoppndvlem16  35392  irrdifflemf  36195  itg2addnclem  36528  dvasin  36561  areacirclem1  36565  areacirclem3  36567  isbnd2  36640  lcmineqlem21  40903  3lexlogpow2ineq2  40913  dvrelog2b  40920  dvrelogpow2b  40922  aks4d1p1p4  40925  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p9  40942  2np3bcnp1  40949  2ap1caineq  40950  oddnumth  41205  nicomachus  41206  sumcubes  41207  remul02  41275  remul01  41277  dffltz  41373  fltne  41383  flt4lem5e  41395  cu3addd  41404  rmspecsqrtnq  41630  rmxluc  41661  rmyluc2  41663  rmydbl  41665  jm2.18  41713  jm2.22  41720  jm2.25  41724  jm2.27c  41732  jm3.1lem2  41743  sqrtcval  42378  imo72b2lem0  42903  refsum2cnlem1  43707  oddfl  43974  xralrple2  44051  infleinflem2  44068  sumnnodd  44333  0ellimcdiv  44352  coseq0  44567  sinmulcos  44568  coskpi2  44569  sinaover2ne0  44571  cosknegpi  44572  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  itgsinexp  44658  stoweidlem1  44704  stoweidlem62  44765  wallispilem4  44771  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem6  44782  stirlinglem7  44783  stirlinglem8  44784  stirlinglem10  44786  stirlinglem11  44787  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  dirker2re  44795  dirkerdenne0  44796  dirkerval2  44797  dirkerre  44798  dirkertrigeqlem1  44801  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkeritg  44805  dirkercncflem1  44806  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem43  44853  fourierdlem44  44854  fourierdlem56  44865  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fourierdlem66  44875  fourierdlem68  44877  fourierdlem72  44881  fourierdlem76  44885  fourierdlem79  44888  fourierdlem80  44889  fourierdlem83  44892  fourierdlem95  44904  fourierdlem104  44913  fourierdlem112  44921  fouriercnp  44929  fourierswlem  44933  sge0ad2en  45134  hoicvrrex  45259  hoiqssbllem2  45326  fmtnoodd  46188  sqrtpwpw2p  46193  fmtnorec2lem  46197  fmtnodvds  46199  goldbachthlem2  46201  fmtnoprmfac1lem  46219  fmtnoprmfac2  46222  fmtnofac1  46225  2pwp1prm  46244  mod42tp1mod8  46257  sfprmdvdsmersenne  46258  lighneallem2  46261  lighneallem4  46265  proththd  46269  quad1  46275  requad01  46276  requad1  46277  requad2  46278  dfodd6  46292  dfeven4  46293  enege  46300  onego  46301  dfeven2  46304  oddflALTV  46318  opoeALTV  46338  opeoALTV  46339  nn0onn0exALTV  46354  nn0enn0exALTV  46355  nnennexALTV  46356  mogoldbblem  46375  perfectALTV  46378  fppr2odd  46386  sgoldbeven3prm  46438  0nodd  46567  2nodd  46569  2zlidl  46786  2zrngamgm  46791  2zrngagrp  46795  2zrngmmgm  46798  2zrngnmlid  46801  nn0onn0ex  47163  nn0enn0ex  47164  nnennex  47165  nnpw2even  47169  fldivexpfllog2  47205  blenpw2m1  47219  nnpw2blen  47220  blennn0em1  47231  dig2nn1st  47245  dig2bits  47254  dignn0flhalflem1  47255  dignn0flhalflem2  47256  dignn0ehalf  47257  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  itcovalt2lem2lem2  47314  ackval2  47322  ackval3  47323  itschlc0yqe  47400  itsclc0yqsollem1  47402  itsclc0yqsol  47404  itsclc0xyqsolr  47409  itsclquadb  47416  2itscplem1  47418  2itscplem3  47420  itscnhlinecirc02plem1  47422