Theorem 2cnd 12428

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11205  2c2 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-addcl 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-2 12412

This theorem is used by:  subhalfhalf  12587  cnm2m1cnm3  12606  xp1d2m1eqxm1d2  12607  zeo2  12793  ge2halflem1  13244  fzosplitprm1  13920  2tnp1ge0ge0  13976  flhalf  13977  2txmodxeq0  14081  mulbinom2  14374  binom3  14375  zesq  14377  expmulnbnd  14386  discr  14391  sqoddm1div8  14394  mulsubdivbinom2  14413  swrds2m  15101  amgm2  15546  bhmafibid1cn  15642  bhmafibid2cn  15643  iseraltlem2  15859  iseralt  15861  trirecip  16041  geo2sum  16051  bpolydiflem  16229  bpoly4  16234  ege2le3  16265  tanval3  16311  sinhval  16331  tanhlt1  16337  sqrt2irrlem  16425  sqrt2irr  16426  even2n  16521  oddm1even  16522  oddp1even  16523  mod2eq1n2dvds  16526  ltoddhalfle  16540  m1exp1  16555  nn0enne  16556  flodddiv4  16594  flodddiv4t2lthalf  16597  bitsp1e  16611  bitsp1o  16612  bitsfzo  16614  bitsmod  16615  bitsinv1lem  16620  sadadd2lem2  16629  sadcaddlem  16636  bitsuz  16653  bitsshft  16654  prmdiv  16971  vfermltlALT  16989  iserodd  17022  4sqlem7  17131  4sqlem10  17134  4sqlem19  17150  prmgaplem7  17244  2expltfac  17279  smndex2dlinvh  19125  efgredlemg  19965  frgpnabllem1  20096  ablsimpgfindlem1  20332  metnrmlem3  25190  iihalf1cn  25262  iihalf2cn  25264  pcoass  25354  cphipval2  25571  csbren  25729  trirn  25730  minveclem2  25756  ovolunlem1a  25826  uniioombllem5  25917  uniioombl  25919  dyaddisjlem  25925  mbfi1fseqlem5  26049  mbfi1fseqlem6  26050  dvsincos  26310  lhop1  26343  cosargd  26945  dvcnsqrt  27081  root1id  27091  ssscongptld  27159  chordthmlem  27169  chordthmlem2  27170  chordthmlem4  27172  heron  27175  dcubic1  27182  mcubic  27184  cubic2  27185  quartlem4  27197  quart  27198  cosasin  27241  cosatan  27258  atantayl  27274  atantayl2  27275  atantayl3  27276  log2tlbnd  27282  cxp2limlem  27312  divsqrtsumlem  27316  lgamgulmlem2  27366  lgamgulmlem4  27368  lgamucov  27374  ftalem2  27410  basellem2  27418  basellem3  27419  basellem5  27421  basellem8  27424  logfaclbnd  27558  perfectlem2  27566  perfect  27567  bcp1ctr  27615  bposlem1  27620  bposlem2  27621  lgslem1  27633  lgsqrlem2  27683  gausslemma2dlem1a  27701  gausslemma2dlem3  27704  gausslemma2dlem4  27705  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisenlem4  27714  lgsquadlem1  27716  lgsquadlem2  27717  lgsquad2lem1  27720  2lgslem1a1  27725  2lgslem1a2  27726  2lgslem1b  27728  2lgslem1c  27729  2lgslem3a1  27736  2lgslem3d1  27739  2sq2  27769  addsq2nreurex  27780  chebbnd1lem3  27807  chto1ub  27812  dchrisumlem2  27826  dchrisum0flblem2  27845  dchrisum0fno1  27847  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2  27854  logdivsum  27869  mulog2sumlem2  27871  vmalogdivsum2  27874  log2sumbnd  27880  selberglem2  27882  chpdifbndlem1  27889  selberg3lem1  27893  selberg3  27895  selberg4lem1  27896  selberg4  27897  selberg4r  27906  selberg34r  27907  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntpbnd1a  27921  pntpbnd2  27923  pntibndlem2  27927  pntlemb  27933  pntlemg  27934  pntlemh  27935  pntlemr  27938  pntlemk  27942  pntlemo  27943  ostth2lem1  27954  fltne  27984  flt4lem5e  27995  finsumvtxdg2ssteplem4  30138  upgrwlkdvdelem  30331  wwlksnextwrd  30495  wwlksnextinj  30497  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a4  30597  clwlkclwwlklem3  30601  clwwlkext2edg  30656  clwwlknonex2lem1  30707  clwwlknonex2lem2  30708  2clwwlk2clwwlk  30960  numclwwlk1lem2foalem  30961  numclwwlk1lem2fo  30968  numclwwlk2lem1  30986  numclwlk2lem2f  30987  numclwwlk2  30991  ex-ind-dvds  31071  nrt2irr  31083  binom2subadd  33383  quad3d  33391  2exple2exp  33475  wrdt2ind  33566  archirngz  33800  archiabllem2c  33806  fldext2rspun  34364  constrrtcc  34417  constrelextdg2  34429  constraddcl  34444  constrrecl  34451  constrresqrtcl  34459  2sqr3nconstr  34463  cos9thpiminplylem1  34464  cos9thpiminplylem2  34465  cos9thpiminplylem3  34466  cos9thpiminply  34470  cos9thpinconstrlem1  34471  cos9thpinconstrlem2  34472  cos9thpinconstr  34473  sqsscirc1  34590  dya2icoseg  34959  dya2iocucvr  34966  omssubadd  34982  oddpwdc  35036  eulerpartlemgs2  35062  fibp1  35083  signslema  35241  itgexpif  35285  vtsprod  35318  hgt750lemd  35327  logdivsqrle  35329  subfacp1lem1  36034  subfacp1lem5  36039  dnibndlem10  37449  knoppcnlem10  37464  knoppndvlem2  37475  knoppndvlem7  37480  knoppndvlem9  37482  knoppndvlem10  37483  knoppndvlem16  37489  irrdifflemf  38355  qdiff  38357  itg2addnclem  38698  dvasin  38731  areacirclem1  38735  areacirclem3  38737  isbnd2  38826  lcmineqlem21  43208  3lexlogpow2ineq2  43218  dvrelog2b  43225  dvrelogpow2b  43227  aks4d1p1p4  43230  aks4d1p1p6  43232  aks4d1p1p7  43233  aks4d1p1p5  43234  aks4d1p9  43247  posbezout  43259  2np3bcnp1  43303  2ap1caineq  43304  oddnumth  43477  nicomachus  43478  sumcubes  43479  ef11d  43499  cxpi11d  43503  tan3rdpi  43512  readvrec2  43521  remul02  43565  remul01  43567  dffltz  43779  cu3addd  43800  rmspecsqrtnq  44022  rmxluc  44052  rmyluc2  44054  rmydbl  44056  jm2.18  44104  jm2.22  44111  jm2.25  44115  jm2.27c  44123  jm3.1lem2  44134  sqrtcval  44750  imo72b2lem0  45274  refsum2cnlem1  46162  oddfl  46402  xralrple2  46474  infleinflem2  46490  sumnnodd  46750  0ellimcdiv  46767  coseq0  46982  sinmulcos  46983  coskpi2  46984  sinaover2ne0  46986  cosknegpi  46987  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  itgsinexp  47073  stoweidlem1  47119  stoweidlem62  47180  wallispilem4  47186  wallispilem5  47187  wallispi  47188  wallispi2lem1  47189  wallispi2lem2  47190  wallispi2  47191  stirlinglem1  47192  stirlinglem3  47194  stirlinglem4  47195  stirlinglem5  47196  stirlinglem6  47197  stirlinglem7  47198  stirlinglem8  47199  stirlinglem10  47201  stirlinglem11  47202  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  dirker2re  47210  dirkerdenne0  47211  dirkerval2  47212  dirkerre  47213  dirkertrigeqlem1  47216  dirkertrigeqlem2  47217  dirkertrigeqlem3  47218  dirkertrigeq  47219  dirkeritg  47220  dirkercncflem1  47221  dirkercncflem2  47222  dirkercncflem4  47224  fourierdlem43  47268  fourierdlem44  47269  fourierdlem56  47280  fourierdlem57  47281  fourierdlem58  47282  fourierdlem62  47286  fourierdlem66  47290  fourierdlem68  47292  fourierdlem72  47296  fourierdlem76  47300  fourierdlem79  47303  fourierdlem80  47304  fourierdlem83  47307  fourierdlem95  47319  fourierdlem104  47328  fourierdlem112  47336  fouriercnp  47344  fourierswlem  47348  sge0ad2en  47549  hoicvrrex  47674  hoiqssbllem2  47741  sin3t  48025  cos3t  48026  sin5tlem1  48027  sin5tlem3  48029  sin5tlem4  48030  sin5t  48032  2tceilhalfelfzo1  48514  minusmodnep2tmod  48537  modmkpkne  48545  modm2nep1  48550  modm1nem2  48553  fmtnoodd  48726  sqrtpwpw2p  48731  fmtnorec2lem  48735  fmtnodvds  48737  goldbachthlem2  48739  fmtnoprmfac1lem  48757  fmtnoprmfac2  48760  fmtnofac1  48763  2pwp1prm  48782  mod42tp1mod8  48795  sfprmdvdsmersenne  48796  lighneallem2  48799  lighneallem4  48803  proththd  48807  nprmdvdsfacm1lem1  48813  ppivalnn4  48820  quad1  48826  requad01  48827  requad1  48828  requad2  48829  dfodd6  48843  dfeven4  48844  enege  48851  onego  48852  dfeven2  48855  oddflALTV  48869  opoeALTV  48889  opeoALTV  48890  nn0onn0exALTV  48905  nn0enn0exALTV  48906  nnennexALTV  48907  mogoldbblem  48926  perfectALTV  48929  fppr2odd  48937  sgoldbeven3prm  48989  gpg3nbgrvtx0  49282  gpg3kgrtriexlem2  49290  pgnbgreunbgrlem2lem1  49320  pgnbgreunbgrlem2lem2  49321  pgnbgreunbgrlem2lem3  49322  0nodd  49375  2nodd  49377  2zlidl  49445  2zrngamgm  49450  2zrngagrp  49454  2zrngmmgm  49457  2zrngnmlid  49460  nn0onn0ex  49743  nn0enn0ex  49744  nnennex  49745  nnpw2even  49749  fldivexpfllog2  49785  blenpw2m1  49799  nnpw2blen  49800  blennn0em1  49811  dig2nn1st  49825  dig2bits  49834  dignn0flhalflem1  49835  dignn0flhalflem2  49836  dignn0ehalf  49837  nn0sumshdiglemA  49839  nn0sumshdiglemB  49840  itcovalt2lem2lem2  49894  ackval2  49902  ackval3  49903  itschlc0yqe  49980  itsclc0yqsollem1  49982  itsclc0yqsol  49984  itsclc0xyqsolr  49989  itsclquadb  49996  2itscplem1  49998  2itscplem3  50000  itscnhlinecirc02plem1  50002