Theorem 2cnd 12240

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  2c2 12217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225

This theorem is referenced by:  subhalfhalf  12392  cnm2m1cnm3  12411  xp1d2m1eqxm1d2  12412  zeo2  12597  ge2halflem1  13044  fzosplitprm1  13714  2tnp1ge0ge0  13767  flhalf  13768  2txmodxeq0  13872  mulbinom2  14164  binom3  14165  zesq  14167  expmulnbnd  14176  discr  14181  sqoddm1div8  14184  mulsubdivbinom2  14203  swrds2m  14883  amgm2  15312  bhmafibid1cn  15408  bhmafibid2cn  15409  iseraltlem2  15625  iseralt  15627  trirecip  15805  geo2sum  15815  bpolydiflem  15996  ege2le3  16032  tanval3  16078  sinhval  16098  tanhlt1  16104  sqrt2irrlem  16192  sqrt2irr  16193  even2n  16288  oddm1even  16289  oddp1even  16290  mod2eq1n2dvds  16293  ltoddhalfle  16307  m1exp1  16322  nn0enne  16323  flodddiv4  16361  flodddiv4t2lthalf  16364  bitsp1e  16378  bitsp1o  16379  bitsfzo  16381  bitsmod  16382  bitsinv1lem  16387  sadadd2lem2  16396  sadcaddlem  16403  bitsuz  16420  bitsshft  16421  prmdiv  16731  vfermltlALT  16749  iserodd  16782  4sqlem7  16891  4sqlem10  16894  4sqlem19  16910  prmgaplem7  17004  2expltfac  17039  smndex2dlinvh  18820  efgredlemg  19648  frgpnabllem1  19779  ablsimpgfindlem1  20015  metnrmlem3  24726  iihalf1cn  24802  iihalf1cnOLD  24803  iihalf2cn  24805  iihalf2cnOLD  24806  pcoass  24900  cphipval2  25117  csbren  25275  trirn  25276  minveclem2  25302  ovolunlem1a  25373  uniioombllem5  25464  uniioombl  25466  dyaddisjlem  25472  mbfi1fseqlem5  25596  mbfi1fseqlem6  25597  dvsincos  25861  lhop1  25895  cosargd  26493  dvcnsqrt  26629  root1id  26640  ssscongptld  26708  chordthmlem  26718  chordthmlem2  26719  chordthmlem4  26721  heron  26724  dcubic1  26731  mcubic  26733  cubic2  26734  quartlem4  26746  quart  26747  cosasin  26790  cosatan  26807  atantayl  26823  atantayl2  26824  atantayl3  26825  log2tlbnd  26831  cxp2limlem  26862  divsqrtsumlem  26866  lgamgulmlem2  26916  lgamgulmlem4  26918  lgamucov  26924  ftalem2  26960  basellem2  26968  basellem3  26969  basellem5  26971  basellem8  26974  logfaclbnd  27109  perfectlem2  27117  perfect  27118  bcp1ctr  27166  bposlem1  27171  bposlem2  27172  lgslem1  27184  lgsqrlem2  27234  gausslemma2dlem1a  27252  gausslemma2dlem3  27255  gausslemma2dlem4  27256  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  lgsquadlem2  27268  lgsquad2lem1  27271  2lgslem1a1  27276  2lgslem1a2  27277  2lgslem1b  27279  2lgslem1c  27280  2lgslem3a1  27287  2lgslem3d1  27290  2sq2  27320  addsq2nreurex  27331  chebbnd1lem3  27358  chto1ub  27363  dchrisumlem2  27377  dchrisum0flblem2  27396  dchrisum0fno1  27398  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2  27405  logdivsum  27420  mulog2sumlem2  27422  vmalogdivsum2  27425  log2sumbnd  27431  selberglem2  27433  chpdifbndlem1  27440  selberg3lem1  27444  selberg3  27446  selberg4lem1  27447  selberg4  27448  selberg4r  27457  selberg34r  27458  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntpbnd1a  27472  pntpbnd2  27474  pntibndlem2  27478  pntlemb  27484  pntlemg  27485  pntlemh  27486  pntlemr  27489  pntlemk  27493  pntlemo  27494  ostth2lem1  27505  finsumvtxdg2ssteplem4  29452  upgrwlkdvdelem  29639  wwlksnextwrd  29800  wwlksnextinj  29802  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a4  29899  clwlkclwwlklem3  29903  clwwlkext2edg  29958  clwwlknonex2lem1  30009  clwwlknonex2lem2  30010  2clwwlk2clwwlk  30252  numclwwlk1lem2foalem  30253  numclwwlk1lem2fo  30260  numclwwlk2lem1  30278  numclwlk2lem2f  30279  numclwwlk2  30283  ex-ind-dvds  30363  nrt2irr  30375  binom2subadd  32638  quad3d  32646  2exple2exp  32743  wrdt2ind  32848  archirngz  33116  archiabllem2c  33122  fldext2rspun  33650  constrrtcc  33698  constrelextdg2  33710  constraddcl  33725  constrrecl  33732  constrresqrtcl  33740  2sqr3nconstr  33744  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cos9thpinconstr  33754  sqsscirc1  33871  dya2icoseg  34241  dya2iocucvr  34248  oddpwdc  34318  eulerpartlemgs2  34344  fibp1  34365  signslema  34526  itgexpif  34570  vtsprod  34603  hgt750lemd  34612  logdivsqrle  34614  subfacp1lem1  35139  subfacp1lem5  35144  dnibndlem10  36448  knoppcnlem10  36463  knoppndvlem2  36474  knoppndvlem7  36479  knoppndvlem9  36481  knoppndvlem10  36482  knoppndvlem16  36488  irrdifflemf  37286  itg2addnclem  37638  dvasin  37671  areacirclem1  37675  areacirclem3  37677  isbnd2  37750  lcmineqlem21  42010  3lexlogpow2ineq2  42020  dvrelog2b  42027  dvrelogpow2b  42029  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p9  42049  posbezout  42061  2np3bcnp1  42105  2ap1caineq  42106  oddnumth  42272  nicomachus  42273  sumcubes  42274  ef11d  42300  cxpi11d  42304  tan3rdpi  42313  readvrec2  42322  remul02  42366  remul01  42368  dffltz  42595  fltne  42605  flt4lem5e  42617  cu3addd  42642  rmspecsqrtnq  42867  rmxluc  42898  rmyluc2  42900  rmydbl  42902  jm2.18  42950  jm2.22  42957  jm2.25  42961  jm2.27c  42969  jm3.1lem2  42980  sqrtcval  43603  imo72b2lem0  44127  refsum2cnlem1  45004  oddfl  45249  xralrple2  45323  infleinflem2  45340  sumnnodd  45601  0ellimcdiv  45620  coseq0  45835  sinmulcos  45836  coskpi2  45837  sinaover2ne0  45839  cosknegpi  45840  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  itgsinexp  45926  stoweidlem1  45972  stoweidlem62  46033  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem6  46050  stirlinglem7  46051  stirlinglem8  46052  stirlinglem10  46054  stirlinglem11  46055  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  dirker2re  46063  dirkerdenne0  46064  dirkerval2  46065  dirkerre  46066  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkertrigeq  46072  dirkeritg  46073  dirkercncflem1  46074  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem43  46121  fourierdlem44  46122  fourierdlem56  46133  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem66  46143  fourierdlem68  46145  fourierdlem72  46149  fourierdlem76  46153  fourierdlem79  46156  fourierdlem80  46157  fourierdlem83  46160  fourierdlem95  46172  fourierdlem104  46181  fourierdlem112  46189  fouriercnp  46197  fourierswlem  46201  sge0ad2en  46402  hoicvrrex  46527  hoiqssbllem2  46594  2tceilhalfelfzo1  47306  minusmodnep2tmod  47327  modmkpkne  47335  modm2nep1  47340  modm1nem2  47343  fmtnoodd  47507  sqrtpwpw2p  47512  fmtnorec2lem  47516  fmtnodvds  47518  goldbachthlem2  47520  fmtnoprmfac1lem  47538  fmtnoprmfac2  47541  fmtnofac1  47544  2pwp1prm  47563  mod42tp1mod8  47576  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem4  47584  proththd  47588  quad1  47594  requad01  47595  requad1  47596  requad2  47597  dfodd6  47611  dfeven4  47612  enege  47619  onego  47620  dfeven2  47623  oddflALTV  47637  opoeALTV  47657  opeoALTV  47658  nn0onn0exALTV  47673  nn0enn0exALTV  47674  nnennexALTV  47675  mogoldbblem  47694  perfectALTV  47697  fppr2odd  47705  sgoldbeven3prm  47757  gpg3nbgrvtx0  48040  gpg3kgrtriexlem2  48048  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  0nodd  48131  2nodd  48133  2zlidl  48201  2zrngamgm  48206  2zrngagrp  48210  2zrngmmgm  48213  2zrngnmlid  48216  nn0onn0ex  48485  nn0enn0ex  48486  nnennex  48487  nnpw2even  48491  fldivexpfllog2  48527  blenpw2m1  48541  nnpw2blen  48542  blennn0em1  48553  dig2nn1st  48567  dig2bits  48576  dignn0flhalflem1  48577  dignn0flhalflem2  48578  dignn0ehalf  48579  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  itcovalt2lem2lem2  48636  ackval2  48644  ackval3  48645  itschlc0yqe  48722  itsclc0yqsollem1  48724  itsclc0yqsol  48726  itsclc0xyqsolr  48731  itsclquadb  48738  2itscplem1  48740  2itscplem3  48742  itscnhlinecirc02plem1  48744