Theorem 2cnd 11981

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  2c2 11958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-2 11966

This theorem is referenced by:  subhalfhalf  12137  cnm2m1cnm3  12156  xp1d2m1eqxm1d2  12157  zeo2  12337  fzosplitprm1  13425  2tnp1ge0ge0  13477  flhalf  13478  2txmodxeq0  13579  mulbinom2  13866  binom3  13867  zesq  13869  expmulnbnd  13878  discr  13883  sqoddm1div8  13886  mulsubdivbinom2  13904  swrds2m  14582  amgm2  15009  bhmafibid1cn  15103  bhmafibid2cn  15104  iseraltlem2  15322  iseralt  15324  trirecip  15503  geo2sum  15513  bpolydiflem  15692  ege2le3  15727  tanval3  15771  sinhval  15791  tanhlt1  15797  sqrt2irrlem  15885  sqrt2irr  15886  even2n  15979  oddm1even  15980  oddp1even  15981  mod2eq1n2dvds  15984  ltoddhalfle  15998  m1exp1  16013  nn0enne  16014  flodddiv4  16050  flodddiv4t2lthalf  16053  bitsp1e  16067  bitsp1o  16068  bitsfzo  16070  bitsmod  16071  bitsinv1lem  16076  sadadd2lem2  16085  sadcaddlem  16092  bitsuz  16109  bitsshft  16110  prmdiv  16414  vfermltlALT  16431  iserodd  16464  4sqlem7  16573  4sqlem10  16576  4sqlem19  16592  prmgaplem7  16686  2expltfac  16722  smndex2dlinvh  18471  efgredlemg  19263  frgpnabllem1  19389  ablsimpgfindlem1  19625  metnrmlem3  23930  iihalf1cn  24001  iihalf2cn  24003  pcoass  24093  cphipval2  24310  csbren  24468  trirn  24469  minveclem2  24495  ovolunlem1a  24565  uniioombllem5  24656  uniioombl  24658  dyaddisjlem  24664  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  dvsincos  25050  lhop1  25083  cosargd  25668  dvcnsqrt  25802  root1id  25812  ssscongptld  25877  chordthmlem  25887  chordthmlem2  25888  chordthmlem4  25890  heron  25893  dcubic1  25900  mcubic  25902  cubic2  25903  quartlem4  25915  quart  25916  cosasin  25959  cosatan  25976  atantayl  25992  atantayl2  25993  atantayl3  25994  log2tlbnd  26000  cxp2limlem  26030  divsqrtsumlem  26034  lgamgulmlem2  26084  lgamgulmlem4  26086  lgamucov  26092  ftalem2  26128  basellem2  26136  basellem3  26137  basellem5  26139  basellem8  26142  logfaclbnd  26275  perfectlem2  26283  perfect  26284  bcp1ctr  26332  bposlem1  26337  bposlem2  26338  lgslem1  26350  lgsqrlem2  26400  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  gausslemma2dlem4  26422  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad2lem1  26437  2lgslem1a1  26442  2lgslem1a2  26443  2lgslem1b  26445  2lgslem1c  26446  2lgslem3a1  26453  2lgslem3d1  26456  2sq2  26486  addsq2nreurex  26497  chebbnd1lem3  26524  chto1ub  26529  dchrisumlem2  26543  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2  26571  logdivsum  26586  mulog2sumlem2  26588  vmalogdivsum2  26591  log2sumbnd  26597  selberglem2  26599  chpdifbndlem1  26606  selberg3lem1  26610  selberg3  26612  selberg4lem1  26613  selberg4  26614  selberg4r  26623  selberg34r  26624  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem2  26644  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemr  26655  pntlemk  26659  pntlemo  26660  ostth2lem1  26671  finsumvtxdg2ssteplem4  27818  upgrwlkdvdelem  28005  wwlksnextwrd  28163  wwlksnextinj  28165  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a4  28262  clwlkclwwlklem3  28266  clwwlkext2edg  28321  clwwlknonex2lem1  28372  clwwlknonex2lem2  28373  2clwwlk2clwwlk  28615  numclwwlk1lem2foalem  28616  numclwwlk1lem2fo  28623  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwwlk2  28646  ex-ind-dvds  28726  wrdt2ind  31127  archirngz  31345  archiabllem2c  31351  sqsscirc1  31760  dya2icoseg  32144  dya2iocucvr  32151  oddpwdc  32221  eulerpartlemgs2  32247  fibp1  32268  signslema  32441  itgexpif  32486  vtsprod  32519  hgt750lemd  32528  logdivsqrle  32530  subfacp1lem1  33041  subfacp1lem5  33046  dnibndlem10  34594  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem9  34627  knoppndvlem10  34628  knoppndvlem16  34634  irrdifflemf  35423  itg2addnclem  35755  dvasin  35788  areacirclem1  35792  areacirclem3  35794  isbnd2  35868  lcmineqlem21  39985  3lexlogpow2ineq2  39995  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p9  40024  2np3bcnp1  40028  2ap1caineq  40029  remul02  40309  remul01  40311  dffltz  40387  fltne  40397  flt4lem5e  40409  cu3addd  40418  rmspecsqrtnq  40644  rmxluc  40674  rmyluc2  40676  rmydbl  40678  jm2.18  40726  jm2.22  40733  jm2.25  40737  jm2.27c  40745  jm3.1lem2  40756  sqrtcval  41138  imo72b2lem0  41665  refsum2cnlem1  42469  oddfl  42705  xralrple2  42783  infleinflem2  42800  sumnnodd  43061  0ellimcdiv  43080  coseq0  43295  sinmulcos  43296  coskpi2  43297  sinaover2ne0  43299  cosknegpi  43300  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  itgsinexp  43386  stoweidlem1  43432  stoweidlem62  43493  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  dirker2re  43523  dirkerdenne0  43524  dirkerval2  43525  dirkerre  43526  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkeritg  43533  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem43  43581  fourierdlem44  43582  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem66  43603  fourierdlem68  43605  fourierdlem72  43609  fourierdlem76  43613  fourierdlem79  43616  fourierdlem80  43617  fourierdlem83  43620  fourierdlem95  43632  fourierdlem104  43641  fourierdlem112  43649  fouriercnp  43657  fourierswlem  43661  sge0ad2en  43859  hoicvrrex  43984  hoiqssbllem2  44051  fmtnoodd  44873  sqrtpwpw2p  44878  fmtnorec2lem  44882  fmtnodvds  44884  goldbachthlem2  44886  fmtnoprmfac1lem  44904  fmtnoprmfac2  44907  fmtnofac1  44910  2pwp1prm  44929  mod42tp1mod8  44942  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem4  44950  proththd  44954  quad1  44960  requad01  44961  requad1  44962  requad2  44963  dfodd6  44977  dfeven4  44978  enege  44985  onego  44986  dfeven2  44989  oddflALTV  45003  opoeALTV  45023  opeoALTV  45024  nn0onn0exALTV  45039  nn0enn0exALTV  45040  nnennexALTV  45041  mogoldbblem  45060  perfectALTV  45063  fppr2odd  45071  sgoldbeven3prm  45123  0nodd  45252  2nodd  45254  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  2zrngnmlid  45395  nn0onn0ex  45757  nn0enn0ex  45758  nnennex  45759  nnpw2even  45763  fldivexpfllog2  45799  blenpw2m1  45813  nnpw2blen  45814  blennn0em1  45825  dig2nn1st  45839  dig2bits  45848  dignn0flhalflem1  45849  dignn0flhalflem2  45850  dignn0ehalf  45851  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  itcovalt2lem2lem2  45908  ackval2  45916  ackval3  45917  itschlc0yqe  45994  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itsclc0xyqsolr  46003  itsclquadb  46010  2itscplem1  46012  2itscplem3  46014  itscnhlinecirc02plem1  46016