Theorem 2cnd 12371

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356

This theorem is referenced by:  subhalfhalf  12527  cnm2m1cnm3  12546  xp1d2m1eqxm1d2  12547  zeo2  12730  fzosplitprm1  13827  2tnp1ge0ge0  13880  flhalf  13881  2txmodxeq0  13982  mulbinom2  14272  binom3  14273  zesq  14275  expmulnbnd  14284  discr  14289  sqoddm1div8  14292  mulsubdivbinom2  14311  swrds2m  14990  amgm2  15418  bhmafibid1cn  15512  bhmafibid2cn  15513  iseraltlem2  15731  iseralt  15733  trirecip  15911  geo2sum  15921  bpolydiflem  16102  ege2le3  16138  tanval3  16182  sinhval  16202  tanhlt1  16208  sqrt2irrlem  16296  sqrt2irr  16297  even2n  16390  oddm1even  16391  oddp1even  16392  mod2eq1n2dvds  16395  ltoddhalfle  16409  m1exp1  16424  nn0enne  16425  flodddiv4  16461  flodddiv4t2lthalf  16464  bitsp1e  16478  bitsp1o  16479  bitsfzo  16481  bitsmod  16482  bitsinv1lem  16487  sadadd2lem2  16496  sadcaddlem  16503  bitsuz  16520  bitsshft  16521  prmdiv  16832  vfermltlALT  16849  iserodd  16882  4sqlem7  16991  4sqlem10  16994  4sqlem19  17010  prmgaplem7  17104  2expltfac  17140  smndex2dlinvh  18952  efgredlemg  19784  frgpnabllem1  19915  ablsimpgfindlem1  20151  metnrmlem3  24902  iihalf1cn  24978  iihalf1cnOLD  24979  iihalf2cn  24981  iihalf2cnOLD  24982  pcoass  25076  cphipval2  25294  csbren  25452  trirn  25453  minveclem2  25479  ovolunlem1a  25550  uniioombllem5  25641  uniioombl  25643  dyaddisjlem  25649  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  dvsincos  26039  lhop1  26073  cosargd  26668  dvcnsqrt  26804  root1id  26815  ssscongptld  26883  chordthmlem  26893  chordthmlem2  26894  chordthmlem4  26896  heron  26899  dcubic1  26906  mcubic  26908  cubic2  26909  quartlem4  26921  quart  26922  cosasin  26965  cosatan  26982  atantayl  26998  atantayl2  26999  atantayl3  27000  log2tlbnd  27006  cxp2limlem  27037  divsqrtsumlem  27041  lgamgulmlem2  27091  lgamgulmlem4  27093  lgamucov  27099  ftalem2  27135  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  logfaclbnd  27284  perfectlem2  27292  perfect  27293  bcp1ctr  27341  bposlem1  27346  bposlem2  27347  lgslem1  27359  lgsqrlem2  27409  gausslemma2dlem1a  27427  gausslemma2dlem3  27430  gausslemma2dlem4  27431  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem1  27446  2lgslem1a1  27451  2lgslem1a2  27452  2lgslem1b  27454  2lgslem1c  27455  2lgslem3a1  27462  2lgslem3d1  27465  2sq2  27495  addsq2nreurex  27506  chebbnd1lem3  27533  chto1ub  27538  dchrisumlem2  27552  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2  27580  logdivsum  27595  mulog2sumlem2  27597  vmalogdivsum2  27600  log2sumbnd  27606  selberglem2  27608  chpdifbndlem1  27615  selberg3lem1  27619  selberg3  27621  selberg4lem1  27622  selberg4  27623  selberg4r  27632  selberg34r  27633  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2  27653  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemr  27664  pntlemk  27668  pntlemo  27669  ostth2lem1  27680  finsumvtxdg2ssteplem4  29584  upgrwlkdvdelem  29772  wwlksnextwrd  29930  wwlksnextinj  29932  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem3  30033  clwwlkext2edg  30088  clwwlknonex2lem1  30139  clwwlknonex2lem2  30140  2clwwlk2clwwlk  30382  numclwwlk1lem2foalem  30383  numclwwlk1lem2fo  30390  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwwlk2  30413  ex-ind-dvds  30493  nrt2irr  30505  quad3d  32757  wrdt2ind  32920  archirngz  33169  archiabllem2c  33175  fldext2chn  33719  constrrtcc  33726  constrelextdg2  33737  sqsscirc1  33854  dya2icoseg  34242  dya2iocucvr  34249  oddpwdc  34319  eulerpartlemgs2  34345  fibp1  34366  signslema  34539  itgexpif  34583  vtsprod  34616  hgt750lemd  34625  logdivsqrle  34627  subfacp1lem1  35147  subfacp1lem5  35152  dnibndlem10  36453  knoppcnlem10  36468  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem9  36486  knoppndvlem10  36487  knoppndvlem16  36493  irrdifflemf  37291  itg2addnclem  37631  dvasin  37664  areacirclem1  37668  areacirclem3  37670  isbnd2  37743  lcmineqlem21  42006  3lexlogpow2ineq2  42016  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p9  42045  posbezout  42057  2np3bcnp1  42101  2ap1caineq  42102  oddnumth  42299  nicomachus  42300  sumcubes  42301  ef11d  42327  cxpi11d  42331  tan3rdpi  42338  remul02  42381  remul01  42383  dffltz  42589  fltne  42599  flt4lem5e  42611  cu3addd  42636  rmspecsqrtnq  42862  rmxluc  42893  rmyluc2  42895  rmydbl  42897  jm2.18  42945  jm2.22  42952  jm2.25  42956  jm2.27c  42964  jm3.1lem2  42975  sqrtcval  43603  imo72b2lem0  44127  refsum2cnlem1  44937  oddfl  45192  xralrple2  45269  infleinflem2  45286  sumnnodd  45551  0ellimcdiv  45570  coseq0  45785  sinmulcos  45786  coskpi2  45787  sinaover2ne0  45789  cosknegpi  45790  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  itgsinexp  45876  stoweidlem1  45922  stoweidlem62  45983  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  dirker2re  46013  dirkerdenne0  46014  dirkerval2  46015  dirkerre  46016  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem43  46071  fourierdlem44  46072  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem66  46093  fourierdlem68  46095  fourierdlem72  46099  fourierdlem76  46103  fourierdlem79  46106  fourierdlem80  46107  fourierdlem83  46110  fourierdlem95  46122  fourierdlem104  46131  fourierdlem112  46139  fouriercnp  46147  fourierswlem  46151  sge0ad2en  46352  hoicvrrex  46477  hoiqssbllem2  46544  fmtnoodd  47407  sqrtpwpw2p  47412  fmtnorec2lem  47416  fmtnodvds  47418  goldbachthlem2  47420  fmtnoprmfac1lem  47438  fmtnoprmfac2  47441  fmtnofac1  47444  2pwp1prm  47463  mod42tp1mod8  47476  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem4  47484  proththd  47488  quad1  47494  requad01  47495  requad1  47496  requad2  47497  dfodd6  47511  dfeven4  47512  enege  47519  onego  47520  dfeven2  47523  oddflALTV  47537  opoeALTV  47557  opeoALTV  47558  nn0onn0exALTV  47573  nn0enn0exALTV  47574  nnennexALTV  47575  mogoldbblem  47594  perfectALTV  47597  fppr2odd  47605  sgoldbeven3prm  47657  0nodd  47893  2nodd  47895  2zlidl  47963  2zrngamgm  47968  2zrngagrp  47972  2zrngmmgm  47975  2zrngnmlid  47978  nn0onn0ex  48257  nn0enn0ex  48258  nnennex  48259  nnpw2even  48263  fldivexpfllog2  48299  blenpw2m1  48313  nnpw2blen  48314  blennn0em1  48325  dig2nn1st  48339  dig2bits  48348  dignn0flhalflem1  48349  dignn0flhalflem2  48350  dignn0ehalf  48351  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  itcovalt2lem2lem2  48408  ackval2  48416  ackval3  48417  itschlc0yqe  48494  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itsclc0xyqsolr  48503  itsclquadb  48510  2itscplem1  48512  2itscplem3  48514  itscnhlinecirc02plem1  48516