Theorem 2cnd 12272

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11090  2c2 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11150  ax-addcl 11152

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-2 12257

This theorem is referenced by:  subhalfhalf  12428  cnm2m1cnm3  12447  xp1d2m1eqxm1d2  12448  zeo2  12631  fzosplitprm1  13724  2tnp1ge0ge0  13776  flhalf  13777  2txmodxeq0  13878  mulbinom2  14168  binom3  14169  zesq  14171  expmulnbnd  14180  discr  14185  sqoddm1div8  14188  mulsubdivbinom2  14204  swrds2m  14874  amgm2  15298  bhmafibid1cn  15392  bhmafibid2cn  15393  iseraltlem2  15611  iseralt  15613  trirecip  15791  geo2sum  15801  bpolydiflem  15980  ege2le3  16015  tanval3  16059  sinhval  16079  tanhlt1  16085  sqrt2irrlem  16173  sqrt2irr  16174  even2n  16267  oddm1even  16268  oddp1even  16269  mod2eq1n2dvds  16272  ltoddhalfle  16286  m1exp1  16301  nn0enne  16302  flodddiv4  16338  flodddiv4t2lthalf  16341  bitsp1e  16355  bitsp1o  16356  bitsfzo  16358  bitsmod  16359  bitsinv1lem  16364  sadadd2lem2  16373  sadcaddlem  16380  bitsuz  16397  bitsshft  16398  prmdiv  16700  vfermltlALT  16717  iserodd  16750  4sqlem7  16859  4sqlem10  16862  4sqlem19  16878  prmgaplem7  16972  2expltfac  17008  smndex2dlinvh  18773  efgredlemg  19574  frgpnabllem1  19701  ablsimpgfindlem1  19936  metnrmlem3  24306  iihalf1cn  24377  iihalf2cn  24379  pcoass  24469  cphipval2  24687  csbren  24845  trirn  24846  minveclem2  24872  ovolunlem1a  24942  uniioombllem5  25033  uniioombl  25035  dyaddisjlem  25041  mbfi1fseqlem5  25166  mbfi1fseqlem6  25167  dvsincos  25427  lhop1  25460  cosargd  26045  dvcnsqrt  26179  root1id  26189  ssscongptld  26254  chordthmlem  26264  chordthmlem2  26265  chordthmlem4  26267  heron  26270  dcubic1  26277  mcubic  26279  cubic2  26280  quartlem4  26292  quart  26293  cosasin  26336  cosatan  26353  atantayl  26369  atantayl2  26370  atantayl3  26371  log2tlbnd  26377  cxp2limlem  26407  divsqrtsumlem  26411  lgamgulmlem2  26461  lgamgulmlem4  26463  lgamucov  26469  ftalem2  26505  basellem2  26513  basellem3  26514  basellem5  26516  basellem8  26519  logfaclbnd  26652  perfectlem2  26660  perfect  26661  bcp1ctr  26709  bposlem1  26714  bposlem2  26715  lgslem1  26727  lgsqrlem2  26777  gausslemma2dlem1a  26795  gausslemma2dlem3  26798  gausslemma2dlem4  26799  lgseisenlem1  26805  lgseisenlem2  26806  lgseisenlem3  26807  lgseisenlem4  26808  lgsquadlem1  26810  lgsquadlem2  26811  lgsquad2lem1  26814  2lgslem1a1  26819  2lgslem1a2  26820  2lgslem1b  26822  2lgslem1c  26823  2lgslem3a1  26830  2lgslem3d1  26833  2sq2  26863  addsq2nreurex  26874  chebbnd1lem3  26901  chto1ub  26906  dchrisumlem2  26920  dchrisum0flblem2  26939  dchrisum0fno1  26941  dchrisum0lem1b  26945  dchrisum0lem1  26946  dchrisum0lem2  26948  logdivsum  26963  mulog2sumlem2  26965  vmalogdivsum2  26968  log2sumbnd  26974  selberglem2  26976  chpdifbndlem1  26983  selberg3lem1  26987  selberg3  26989  selberg4lem1  26990  selberg4  26991  selberg4r  27000  selberg34r  27001  pntrlog2bndlem3  27009  pntrlog2bndlem4  27010  pntrlog2bndlem5  27011  pntrlog2bndlem6  27013  pntpbnd1a  27015  pntpbnd2  27017  pntibndlem2  27021  pntlemb  27027  pntlemg  27028  pntlemh  27029  pntlemr  27032  pntlemk  27036  pntlemo  27037  ostth2lem1  27048  finsumvtxdg2ssteplem4  28670  upgrwlkdvdelem  28858  wwlksnextwrd  29016  wwlksnextinj  29018  clwlkclwwlklem2a1  29110  clwlkclwwlklem2a4  29115  clwlkclwwlklem3  29119  clwwlkext2edg  29174  clwwlknonex2lem1  29225  clwwlknonex2lem2  29226  2clwwlk2clwwlk  29468  numclwwlk1lem2foalem  29469  numclwwlk1lem2fo  29476  numclwwlk2lem1  29494  numclwlk2lem2f  29495  numclwwlk2  29499  ex-ind-dvds  29579  wrdt2ind  31988  archirngz  32206  archiabllem2c  32212  sqsscirc1  32719  dya2icoseg  33107  dya2iocucvr  33114  oddpwdc  33184  eulerpartlemgs2  33210  fibp1  33231  signslema  33404  itgexpif  33449  vtsprod  33482  hgt750lemd  33491  logdivsqrle  33493  subfacp1lem1  34001  subfacp1lem5  34006  dnibndlem10  35167  knoppndvlem2  35193  knoppndvlem7  35198  knoppndvlem9  35200  knoppndvlem10  35201  knoppndvlem16  35207  irrdifflemf  36010  itg2addnclem  36343  dvasin  36376  areacirclem1  36380  areacirclem3  36382  isbnd2  36456  lcmineqlem21  40719  3lexlogpow2ineq2  40729  dvrelog2b  40736  dvrelogpow2b  40738  aks4d1p1p4  40741  aks4d1p1p6  40743  aks4d1p1p7  40744  aks4d1p1p5  40745  aks4d1p9  40758  2np3bcnp1  40765  2ap1caineq  40766  remul02  41060  remul01  41062  dffltz  41158  fltne  41168  flt4lem5e  41180  cu3addd  41189  rmspecsqrtnq  41415  rmxluc  41446  rmyluc2  41448  rmydbl  41450  jm2.18  41498  jm2.22  41505  jm2.25  41509  jm2.27c  41517  jm3.1lem2  41528  sqrtcval  42163  imo72b2lem0  42688  refsum2cnlem1  43492  oddfl  43760  xralrple2  43837  infleinflem2  43854  sumnnodd  44119  0ellimcdiv  44138  coseq0  44353  sinmulcos  44354  coskpi2  44355  sinaover2ne0  44357  cosknegpi  44358  ioodvbdlimc1lem2  44421  ioodvbdlimc2lem  44423  itgsinexp  44444  stoweidlem1  44490  stoweidlem62  44551  wallispilem4  44557  wallispilem5  44558  wallispi  44559  wallispi2lem1  44560  wallispi2lem2  44561  wallispi2  44562  stirlinglem1  44563  stirlinglem3  44565  stirlinglem4  44566  stirlinglem5  44567  stirlinglem6  44568  stirlinglem7  44569  stirlinglem8  44570  stirlinglem10  44572  stirlinglem11  44573  stirlinglem13  44575  stirlinglem14  44576  stirlinglem15  44577  dirker2re  44581  dirkerdenne0  44582  dirkerval2  44583  dirkerre  44584  dirkertrigeqlem1  44587  dirkertrigeqlem2  44588  dirkertrigeqlem3  44589  dirkertrigeq  44590  dirkeritg  44591  dirkercncflem1  44592  dirkercncflem2  44593  dirkercncflem4  44595  fourierdlem43  44639  fourierdlem44  44640  fourierdlem56  44651  fourierdlem57  44652  fourierdlem58  44653  fourierdlem62  44657  fourierdlem66  44661  fourierdlem68  44663  fourierdlem72  44667  fourierdlem76  44671  fourierdlem79  44674  fourierdlem80  44675  fourierdlem83  44678  fourierdlem95  44690  fourierdlem104  44699  fourierdlem112  44707  fouriercnp  44715  fourierswlem  44719  sge0ad2en  44920  hoicvrrex  45045  hoiqssbllem2  45112  fmtnoodd  45973  sqrtpwpw2p  45978  fmtnorec2lem  45982  fmtnodvds  45984  goldbachthlem2  45986  fmtnoprmfac1lem  46004  fmtnoprmfac2  46007  fmtnofac1  46010  2pwp1prm  46029  mod42tp1mod8  46042  sfprmdvdsmersenne  46043  lighneallem2  46046  lighneallem4  46050  proththd  46054  quad1  46060  requad01  46061  requad1  46062  requad2  46063  dfodd6  46077  dfeven4  46078  enege  46085  onego  46086  dfeven2  46089  oddflALTV  46103  opoeALTV  46123  opeoALTV  46124  nn0onn0exALTV  46139  nn0enn0exALTV  46140  nnennexALTV  46141  mogoldbblem  46160  perfectALTV  46163  fppr2odd  46171  sgoldbeven3prm  46223  0nodd  46352  2nodd  46354  2zlidl  46480  2zrngamgm  46485  2zrngagrp  46489  2zrngmmgm  46492  2zrngnmlid  46495  nn0onn0ex  46857  nn0enn0ex  46858  nnennex  46859  nnpw2even  46863  fldivexpfllog2  46899  blenpw2m1  46913  nnpw2blen  46914  blennn0em1  46925  dig2nn1st  46939  dig2bits  46948  dignn0flhalflem1  46949  dignn0flhalflem2  46950  dignn0ehalf  46951  nn0sumshdiglemA  46953  nn0sumshdiglemB  46954  itcovalt2lem2lem2  47008  ackval2  47016  ackval3  47017  itschlc0yqe  47094  itsclc0yqsollem1  47096  itsclc0yqsol  47098  itsclc0xyqsolr  47103  itsclquadb  47110  2itscplem1  47112  2itscplem3  47114  itscnhlinecirc02plem1  47116