Theorem 2cnd 12296

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℂcc 11071  2c2 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-2 12280

This theorem is referenced by:  subhalfhalf  12455  cnm2m1cnm3  12474  xp1d2m1eqxm1d2  12475  zeo2  12660  ge2halflem1  13110  fzosplitprm1  13784  2tnp1ge0ge0  13839  flhalf  13840  2txmodxeq0  13944  mulbinom2  14236  binom3  14237  zesq  14239  expmulnbnd  14248  discr  14253  sqoddm1div8  14256  mulsubdivbinom2  14275  swrds2m  14954  amgm2  15397  bhmafibid1cn  15493  bhmafibid2cn  15494  iseraltlem2  15710  iseralt  15712  trirecip  15893  geo2sum  15903  bpolydiflem  16084  ege2le3  16120  tanval3  16166  sinhval  16186  tanhlt1  16192  sqrt2irrlem  16280  sqrt2irr  16281  even2n  16376  oddm1even  16377  oddp1even  16378  mod2eq1n2dvds  16381  ltoddhalfle  16395  m1exp1  16410  nn0enne  16411  flodddiv4  16449  flodddiv4t2lthalf  16452  bitsp1e  16466  bitsp1o  16467  bitsfzo  16469  bitsmod  16470  bitsinv1lem  16475  sadadd2lem2  16484  sadcaddlem  16491  bitsuz  16508  bitsshft  16509  prmdiv  16820  vfermltlALT  16838  iserodd  16871  4sqlem7  16980  4sqlem10  16983  4sqlem19  16999  prmgaplem7  17093  2expltfac  17128  smndex2dlinvh  18954  efgredlemg  19782  frgpnabllem1  19913  ablsimpgfindlem1  20149  metnrmlem3  24919  iihalf1cn  24991  iihalf2cn  24993  pcoass  25083  cphipval2  25300  csbren  25458  trirn  25459  minveclem2  25485  ovolunlem1a  25555  uniioombllem5  25646  uniioombl  25648  dyaddisjlem  25654  mbfi1fseqlem5  25778  mbfi1fseqlem6  25779  dvsincos  26040  lhop1  26073  cosargd  26670  dvcnsqrt  26806  root1id  26816  ssscongptld  26884  chordthmlem  26894  chordthmlem2  26895  chordthmlem4  26897  heron  26900  dcubic1  26907  mcubic  26909  cubic2  26910  quartlem4  26922  quart  26923  cosasin  26966  cosatan  26983  atantayl  26999  atantayl2  27000  atantayl3  27001  log2tlbnd  27007  cxp2limlem  27037  divsqrtsumlem  27041  lgamgulmlem2  27091  lgamgulmlem4  27093  lgamucov  27099  ftalem2  27135  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  logfaclbnd  27283  perfectlem2  27291  perfect  27292  bcp1ctr  27340  bposlem1  27345  bposlem2  27346  lgslem1  27358  lgsqrlem2  27408  gausslemma2dlem1a  27426  gausslemma2dlem3  27429  gausslemma2dlem4  27430  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgseisenlem4  27439  lgsquadlem1  27441  lgsquadlem2  27442  lgsquad2lem1  27445  2lgslem1a1  27450  2lgslem1a2  27451  2lgslem1b  27453  2lgslem1c  27454  2lgslem3a1  27461  2lgslem3d1  27464  2sq2  27494  addsq2nreurex  27505  chebbnd1lem3  27532  chto1ub  27537  dchrisumlem2  27551  dchrisum0flblem2  27570  dchrisum0fno1  27572  dchrisum0lem1b  27576  dchrisum0lem1  27577  dchrisum0lem2  27579  logdivsum  27594  mulog2sumlem2  27596  vmalogdivsum2  27599  log2sumbnd  27605  selberglem2  27607  chpdifbndlem1  27614  selberg3lem1  27618  selberg3  27620  selberg4lem1  27621  selberg4  27622  selberg4r  27631  selberg34r  27632  pntrlog2bndlem3  27640  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  pntrlog2bndlem6  27644  pntpbnd1a  27646  pntpbnd2  27648  pntibndlem2  27652  pntlemb  27658  pntlemg  27659  pntlemh  27660  pntlemr  27663  pntlemk  27667  pntlemo  27668  ostth2lem1  27679  finsumvtxdg2ssteplem4  29746  upgrwlkdvdelem  29933  wwlksnextwrd  30094  wwlksnextinj  30096  clwlkclwwlklem2a1  30191  clwlkclwwlklem2a4  30196  clwlkclwwlklem3  30200  clwwlkext2edg  30255  clwwlknonex2lem1  30306  clwwlknonex2lem2  30307  2clwwlk2clwwlk  30549  numclwwlk1lem2foalem  30550  numclwwlk1lem2fo  30557  numclwwlk2lem1  30575  numclwlk2lem2f  30576  numclwwlk2  30580  ex-ind-dvds  30660  nrt2irr  30672  binom2subadd  32940  quad3d  32948  2exple2exp  33033  wrdt2ind  33128  archirngz  33366  archiabllem2c  33372  fldext2rspun  33976  constrrtcc  34029  constrelextdg2  34041  constraddcl  34056  constrrecl  34063  constrresqrtcl  34071  2sqr3nconstr  34075  cos9thpiminplylem1  34076  cos9thpiminplylem2  34077  cos9thpiminplylem3  34078  cos9thpiminply  34082  cos9thpinconstrlem1  34083  cos9thpinconstrlem2  34084  cos9thpinconstr  34085  sqsscirc1  34202  dya2icoseg  34571  dya2iocucvr  34578  oddpwdc  34648  eulerpartlemgs2  34674  fibp1  34695  signslema  34853  itgexpif  34897  vtsprod  34930  hgt750lemd  34939  logdivsqrle  34941  subfacp1lem1  35526  subfacp1lem5  35531  dnibndlem10  36922  knoppcnlem10  36937  knoppndvlem2  36948  knoppndvlem7  36953  knoppndvlem9  36955  knoppndvlem10  36956  knoppndvlem16  36962  irrdifflemf  37814  qdiff  37816  itg2addnclem  38167  dvasin  38200  areacirclem1  38204  areacirclem3  38206  isbnd2  38279  lcmineqlem21  42663  3lexlogpow2ineq2  42673  dvrelog2b  42680  dvrelogpow2b  42682  aks4d1p1p4  42685  aks4d1p1p6  42687  aks4d1p1p7  42688  aks4d1p1p5  42689  aks4d1p9  42702  posbezout  42714  2np3bcnp1  42758  2ap1caineq  42759  oddnumth  42917  nicomachus  42918  sumcubes  42919  ef11d  42945  cxpi11d  42949  tan3rdpi  42958  readvrec2  42967  remul02  43011  remul01  43013  dffltz  43213  fltne  43223  flt4lem5e  43235  cu3addd  43259  rmspecsqrtnq  43480  rmxluc  43510  rmyluc2  43512  rmydbl  43514  jm2.18  43562  jm2.22  43569  jm2.25  43573  jm2.27c  43581  jm3.1lem2  43592  sqrtcval  44214  imo72b2lem0  44738  refsum2cnlem1  45614  oddfl  45854  xralrple2  45927  infleinflem2  45943  sumnnodd  46203  0ellimcdiv  46220  coseq0  46435  sinmulcos  46436  coskpi2  46437  sinaover2ne0  46439  cosknegpi  46440  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  itgsinexp  46526  stoweidlem1  46572  stoweidlem62  46633  wallispilem4  46639  wallispilem5  46640  wallispi  46641  wallispi2lem1  46642  wallispi2lem2  46643  wallispi2  46644  stirlinglem1  46645  stirlinglem3  46647  stirlinglem4  46648  stirlinglem5  46649  stirlinglem6  46650  stirlinglem7  46651  stirlinglem8  46652  stirlinglem10  46654  stirlinglem11  46655  stirlinglem13  46657  stirlinglem14  46658  stirlinglem15  46659  dirker2re  46663  dirkerdenne0  46664  dirkerval2  46665  dirkerre  46666  dirkertrigeqlem1  46669  dirkertrigeqlem2  46670  dirkertrigeqlem3  46671  dirkertrigeq  46672  dirkeritg  46673  dirkercncflem1  46674  dirkercncflem2  46675  dirkercncflem4  46677  fourierdlem43  46721  fourierdlem44  46722  fourierdlem56  46733  fourierdlem57  46734  fourierdlem58  46735  fourierdlem62  46739  fourierdlem66  46743  fourierdlem68  46745  fourierdlem72  46749  fourierdlem76  46753  fourierdlem79  46756  fourierdlem80  46757  fourierdlem83  46760  fourierdlem95  46772  fourierdlem104  46781  fourierdlem112  46789  fouriercnp  46797  fourierswlem  46801  sge0ad2en  47002  hoicvrrex  47127  hoiqssbllem2  47194  sin3t  47462  cos3t  47463  sin5tlem1  47464  sin5tlem3  47466  sin5tlem4  47467  sin5t  47469  2tceilhalfelfzo1  47927  minusmodnep2tmod  47950  modmkpkne  47958  modm2nep1  47963  modm1nem2  47966  fmtnoodd  48139  sqrtpwpw2p  48144  fmtnorec2lem  48148  fmtnodvds  48150  goldbachthlem2  48152  fmtnoprmfac1lem  48170  fmtnoprmfac2  48173  fmtnofac1  48176  2pwp1prm  48195  mod42tp1mod8  48208  sfprmdvdsmersenne  48209  lighneallem2  48212  lighneallem4  48216  proththd  48220  nprmdvdsfacm1lem1  48226  ppivalnn4  48233  quad1  48239  requad01  48240  requad1  48241  requad2  48242  dfodd6  48256  dfeven4  48257  enege  48264  onego  48265  dfeven2  48268  oddflALTV  48282  opoeALTV  48302  opeoALTV  48303  nn0onn0exALTV  48318  nn0enn0exALTV  48319  nnennexALTV  48320  mogoldbblem  48339  perfectALTV  48342  fppr2odd  48350  sgoldbeven3prm  48402  gpg3nbgrvtx0  48695  gpg3kgrtriexlem2  48703  pgnbgreunbgrlem2lem1  48733  pgnbgreunbgrlem2lem2  48734  pgnbgreunbgrlem2lem3  48735  0nodd  48789  2nodd  48791  2zlidl  48859  2zrngamgm  48864  2zrngagrp  48868  2zrngmmgm  48871  2zrngnmlid  48874  nn0onn0ex  49142  nn0enn0ex  49143  nnennex  49144  nnpw2even  49148  fldivexpfllog2  49184  blenpw2m1  49198  nnpw2blen  49199  blennn0em1  49210  dig2nn1st  49224  dig2bits  49233  dignn0flhalflem1  49234  dignn0flhalflem2  49235  dignn0ehalf  49236  nn0sumshdiglemA  49238  nn0sumshdiglemB  49239  itcovalt2lem2lem2  49293  ackval2  49301  ackval3  49302  itschlc0yqe  49379  itsclc0yqsollem1  49381  itsclc0yqsol  49383  itsclc0xyqsolr  49388  itsclquadb  49395  2itscplem1  49397  2itscplem3  49399  itscnhlinecirc02plem1  49401