Theorem 2cnd 12250

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11027  2c2 12227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235

This theorem is referenced by:  subhalfhalf  12402  cnm2m1cnm3  12421  xp1d2m1eqxm1d2  12422  zeo2  12607  ge2halflem1  13050  fzosplitprm1  13724  2tnp1ge0ge0  13779  flhalf  13780  2txmodxeq0  13884  mulbinom2  14176  binom3  14177  zesq  14179  expmulnbnd  14188  discr  14193  sqoddm1div8  14196  mulsubdivbinom2  14215  swrds2m  14894  amgm2  15323  bhmafibid1cn  15419  bhmafibid2cn  15420  iseraltlem2  15636  iseralt  15638  trirecip  15819  geo2sum  15829  bpolydiflem  16010  ege2le3  16046  tanval3  16092  sinhval  16112  tanhlt1  16118  sqrt2irrlem  16206  sqrt2irr  16207  even2n  16302  oddm1even  16303  oddp1even  16304  mod2eq1n2dvds  16307  ltoddhalfle  16321  m1exp1  16336  nn0enne  16337  flodddiv4  16375  flodddiv4t2lthalf  16378  bitsp1e  16392  bitsp1o  16393  bitsfzo  16395  bitsmod  16396  bitsinv1lem  16401  sadadd2lem2  16410  sadcaddlem  16417  bitsuz  16434  bitsshft  16435  prmdiv  16746  vfermltlALT  16764  iserodd  16797  4sqlem7  16906  4sqlem10  16909  4sqlem19  16925  prmgaplem7  17019  2expltfac  17054  smndex2dlinvh  18879  efgredlemg  19708  frgpnabllem1  19839  ablsimpgfindlem1  20075  metnrmlem3  24845  iihalf1cn  24917  iihalf2cn  24919  pcoass  25009  cphipval2  25226  csbren  25384  trirn  25385  minveclem2  25411  ovolunlem1a  25481  uniioombllem5  25572  uniioombl  25574  dyaddisjlem  25580  mbfi1fseqlem5  25704  mbfi1fseqlem6  25705  dvsincos  25966  lhop1  25999  cosargd  26590  dvcnsqrt  26726  root1id  26736  ssscongptld  26804  chordthmlem  26814  chordthmlem2  26815  chordthmlem4  26817  heron  26820  dcubic1  26827  mcubic  26829  cubic2  26830  quartlem4  26842  quart  26843  cosasin  26886  cosatan  26903  atantayl  26919  atantayl2  26920  atantayl3  26921  log2tlbnd  26927  cxp2limlem  26957  divsqrtsumlem  26961  lgamgulmlem2  27011  lgamgulmlem4  27013  lgamucov  27019  ftalem2  27055  basellem2  27063  basellem3  27064  basellem5  27066  basellem8  27069  logfaclbnd  27203  perfectlem2  27211  perfect  27212  bcp1ctr  27260  bposlem1  27265  bposlem2  27266  lgslem1  27278  lgsqrlem2  27328  gausslemma2dlem1a  27346  gausslemma2dlem3  27349  gausslemma2dlem4  27350  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquadlem2  27362  lgsquad2lem1  27365  2lgslem1a1  27370  2lgslem1a2  27371  2lgslem1b  27373  2lgslem1c  27374  2lgslem3a1  27381  2lgslem3d1  27384  2sq2  27414  addsq2nreurex  27425  chebbnd1lem3  27452  chto1ub  27457  dchrisumlem2  27471  dchrisum0flblem2  27490  dchrisum0fno1  27492  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2  27499  logdivsum  27514  mulog2sumlem2  27516  vmalogdivsum2  27519  log2sumbnd  27525  selberglem2  27527  chpdifbndlem1  27534  selberg3lem1  27538  selberg3  27540  selberg4lem1  27541  selberg4  27542  selberg4r  27551  selberg34r  27552  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntpbnd1a  27566  pntpbnd2  27568  pntibndlem2  27572  pntlemb  27578  pntlemg  27579  pntlemh  27580  pntlemr  27583  pntlemk  27587  pntlemo  27588  ostth2lem1  27599  finsumvtxdg2ssteplem4  29635  upgrwlkdvdelem  29822  wwlksnextwrd  29983  wwlksnextinj  29985  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem3  30089  clwwlkext2edg  30144  clwwlknonex2lem1  30195  clwwlknonex2lem2  30196  2clwwlk2clwwlk  30438  numclwwlk1lem2foalem  30439  numclwwlk1lem2fo  30446  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwwlk2  30469  ex-ind-dvds  30549  nrt2irr  30561  binom2subadd  32833  quad3d  32841  2exple2exp  32937  wrdt2ind  33032  archirngz  33270  archiabllem2c  33276  fldext2rspun  33866  constrrtcc  33919  constrelextdg2  33931  constraddcl  33946  constrrecl  33953  constrresqrtcl  33961  2sqr3nconstr  33965  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  sqsscirc1  34092  dya2icoseg  34461  dya2iocucvr  34468  oddpwdc  34538  eulerpartlemgs2  34564  fibp1  34585  signslema  34746  itgexpif  34790  vtsprod  34823  hgt750lemd  34832  logdivsqrle  34834  subfacp1lem1  35407  subfacp1lem5  35412  dnibndlem10  36793  knoppcnlem10  36808  knoppndvlem2  36819  knoppndvlem7  36824  knoppndvlem9  36826  knoppndvlem10  36827  knoppndvlem16  36833  irrdifflemf  37685  qdiff  37687  itg2addnclem  38038  dvasin  38071  areacirclem1  38075  areacirclem3  38077  isbnd2  38150  lcmineqlem21  42534  3lexlogpow2ineq2  42544  dvrelog2b  42551  dvrelogpow2b  42553  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p9  42573  posbezout  42585  2np3bcnp1  42629  2ap1caineq  42630  oddnumth  42788  nicomachus  42789  sumcubes  42790  ef11d  42816  cxpi11d  42820  tan3rdpi  42829  readvrec2  42838  remul02  42882  remul01  42884  dffltz  43084  fltne  43094  flt4lem5e  43106  cu3addd  43130  rmspecsqrtnq  43351  rmxluc  43381  rmyluc2  43383  rmydbl  43385  jm2.18  43433  jm2.22  43440  jm2.25  43444  jm2.27c  43452  jm3.1lem2  43463  sqrtcval  44085  imo72b2lem0  44609  refsum2cnlem1  45485  oddfl  45726  xralrple2  45799  infleinflem2  45815  sumnnodd  46075  0ellimcdiv  46092  coseq0  46307  sinmulcos  46308  coskpi2  46309  sinaover2ne0  46311  cosknegpi  46312  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  itgsinexp  46398  stoweidlem1  46444  stoweidlem62  46505  wallispilem4  46511  wallispilem5  46512  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirker2re  46535  dirkerdenne0  46536  dirkerval2  46537  dirkerre  46538  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkeritg  46545  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem43  46593  fourierdlem44  46594  fourierdlem56  46605  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem66  46615  fourierdlem68  46617  fourierdlem72  46621  fourierdlem76  46625  fourierdlem79  46628  fourierdlem80  46629  fourierdlem83  46632  fourierdlem95  46644  fourierdlem104  46653  fourierdlem112  46661  fouriercnp  46669  fourierswlem  46673  sge0ad2en  46874  hoicvrrex  46999  hoiqssbllem2  47066  sin3t  47334  cos3t  47335  sin5tlem1  47336  sin5tlem3  47338  sin5tlem4  47339  sin5t  47341  2tceilhalfelfzo1  47799  minusmodnep2tmod  47822  modmkpkne  47830  modm2nep1  47835  modm1nem2  47838  fmtnoodd  48011  sqrtpwpw2p  48016  fmtnorec2lem  48020  fmtnodvds  48022  goldbachthlem2  48024  fmtnoprmfac1lem  48042  fmtnoprmfac2  48045  fmtnofac1  48048  2pwp1prm  48067  mod42tp1mod8  48080  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem4  48088  proththd  48092  nprmdvdsfacm1lem1  48098  ppivalnn4  48105  quad1  48111  requad01  48112  requad1  48113  requad2  48114  dfodd6  48128  dfeven4  48129  enege  48136  onego  48137  dfeven2  48140  oddflALTV  48154  opoeALTV  48174  opeoALTV  48175  nn0onn0exALTV  48190  nn0enn0exALTV  48191  nnennexALTV  48192  mogoldbblem  48211  perfectALTV  48214  fppr2odd  48222  sgoldbeven3prm  48274  gpg3nbgrvtx0  48567  gpg3kgrtriexlem2  48575  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  0nodd  48661  2nodd  48663  2zlidl  48731  2zrngamgm  48736  2zrngagrp  48740  2zrngmmgm  48743  2zrngnmlid  48746  nn0onn0ex  49014  nn0enn0ex  49015  nnennex  49016  nnpw2even  49020  fldivexpfllog2  49056  blenpw2m1  49070  nnpw2blen  49071  blennn0em1  49082  dig2nn1st  49096  dig2bits  49105  dignn0flhalflem1  49106  dignn0flhalflem2  49107  dignn0ehalf  49108  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  itcovalt2lem2lem2  49165  ackval2  49173  ackval3  49174  itschlc0yqe  49251  itsclc0yqsollem1  49253  itsclc0yqsol  49255  itsclc0xyqsolr  49260  itsclquadb  49267  2itscplem1  49269  2itscplem3  49271  itscnhlinecirc02plem1  49273