Theorem 2cnd 11718

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 10538  2c2 11695

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796  ax-1cn 10598  ax-addcl 10600

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896  df-2 11703

This theorem is referenced by:  subhalfhalf  11874  cnm2m1cnm3  11893  xp1d2m1eqxm1d2  11894  zeo2  12072  fzosplitprm1  13150  2tnp1ge0ge0  13202  flhalf  13203  2txmodxeq0  13302  mulbinom2  13587  binom3  13588  zesq  13590  expmulnbnd  13599  discr  13604  sqoddm1div8  13607  mulsubdivbinom2  13625  swrds2m  14306  amgm2  14732  bhmafibid1cn  14826  bhmafibid2cn  14827  iseraltlem2  15042  iseralt  15044  trirecip  15221  geo2sum  15232  bpolydiflem  15411  ege2le3  15446  tanval3  15490  sinhval  15510  tanhlt1  15516  sqrt2irrlem  15604  sqrt2irr  15605  even2n  15694  oddm1even  15695  oddp1even  15696  mod2eq1n2dvds  15699  ltoddhalfle  15713  m1exp1  15730  nn0enne  15731  flodddiv4  15767  flodddiv4t2lthalf  15770  bitsp1e  15784  bitsp1o  15785  bitsfzo  15787  bitsmod  15788  bitsinv1lem  15793  sadadd2lem2  15802  sadcaddlem  15809  bitsuz  15826  bitsshft  15827  prmdiv  16125  vfermltlALT  16142  iserodd  16175  4sqlem7  16283  4sqlem10  16286  4sqlem19  16302  prmgaplem7  16396  2expltfac  16429  smndex2dlinvh  18085  efgredlemg  18871  frgpnabllem1  18996  ablsimpgfindlem1  19232  metnrmlem3  23472  iihalf1cn  23539  iihalf2cn  23541  pcoass  23631  cphipval2  23847  csbren  24005  trirn  24006  minveclem2  24032  ovolunlem1a  24100  uniioombllem5  24191  uniioombl  24193  dyaddisjlem  24199  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  dvsincos  24581  lhop1  24614  cosargd  25194  dvcnsqrt  25328  root1id  25338  ssscongptld  25403  chordthmlem  25413  chordthmlem2  25414  chordthmlem4  25416  heron  25419  dcubic1  25426  mcubic  25428  cubic2  25429  quartlem4  25441  quart  25442  cosasin  25485  cosatan  25502  atantayl  25518  atantayl2  25519  atantayl3  25520  log2tlbnd  25526  cxp2limlem  25556  divsqrtsumlem  25560  lgamgulmlem2  25610  lgamgulmlem4  25612  lgamucov  25618  ftalem2  25654  basellem2  25662  basellem3  25663  basellem5  25665  basellem8  25668  logfaclbnd  25801  perfectlem2  25809  perfect  25810  bcp1ctr  25858  bposlem1  25863  bposlem2  25864  lgslem1  25876  lgsqrlem2  25926  gausslemma2dlem1a  25944  gausslemma2dlem3  25947  gausslemma2dlem4  25948  lgseisenlem1  25954  lgseisenlem2  25955  lgseisenlem3  25956  lgseisenlem4  25957  lgsquadlem1  25959  lgsquadlem2  25960  lgsquad2lem1  25963  2lgslem1a1  25968  2lgslem1a2  25969  2lgslem1b  25971  2lgslem1c  25972  2lgslem3a1  25979  2lgslem3d1  25982  2sq2  26012  addsq2nreurex  26023  chebbnd1lem3  26050  chto1ub  26055  dchrisumlem2  26069  dchrisum0flblem2  26088  dchrisum0fno1  26090  dchrisum0lem1b  26094  dchrisum0lem1  26095  dchrisum0lem2  26097  logdivsum  26112  mulog2sumlem2  26114  vmalogdivsum2  26117  log2sumbnd  26123  selberglem2  26125  chpdifbndlem1  26132  selberg3lem1  26136  selberg3  26138  selberg4lem1  26139  selberg4  26140  selberg4r  26149  selberg34r  26150  pntrlog2bndlem3  26158  pntrlog2bndlem4  26159  pntrlog2bndlem5  26160  pntrlog2bndlem6  26162  pntpbnd1a  26164  pntpbnd2  26166  pntibndlem2  26170  pntlemb  26176  pntlemg  26177  pntlemh  26178  pntlemr  26181  pntlemk  26185  pntlemo  26186  ostth2lem1  26197  finsumvtxdg2ssteplem4  27333  upgrwlkdvdelem  27520  wwlksnextwrd  27678  wwlksnextinj  27680  clwlkclwwlklem2a1  27773  clwlkclwwlklem2a4  27778  clwlkclwwlklem3  27782  clwwlkext2edg  27838  clwwlknonex2lem1  27889  clwwlknonex2lem2  27890  2clwwlk2clwwlk  28132  numclwwlk1lem2foalem  28133  numclwwlk1lem2fo  28140  numclwwlk2lem1  28158  numclwlk2lem2f  28159  numclwwlk2  28163  ex-ind-dvds  28243  wrdt2ind  30631  archirngz  30822  archiabllem2c  30828  sqsscirc1  31155  dya2icoseg  31539  dya2iocucvr  31546  oddpwdc  31616  eulerpartlemgs2  31642  fibp1  31663  signslema  31836  itgexpif  31881  vtsprod  31914  hgt750lemd  31923  logdivsqrle  31925  subfacp1lem1  32430  subfacp1lem5  32435  dnibndlem10  33830  knoppndvlem2  33856  knoppndvlem7  33861  knoppndvlem9  33863  knoppndvlem10  33864  knoppndvlem16  33870  itg2addnclem  34947  dvasin  34982  areacirclem1  34986  areacirclem3  34988  isbnd2  35065  remul02  39241  remul01  39243  dffltz  39277  fltne  39278  cu3addd  39283  rmspecsqrtnq  39509  rmxluc  39539  rmyluc2  39541  rmydbl  39543  jm2.18  39591  jm2.22  39598  jm2.25  39602  jm2.27c  39610  jm3.1lem2  39621  imo72b2lem0  40522  refsum2cnlem1  41300  oddfl  41549  xralrple2  41628  infleinflem2  41645  sumnnodd  41917  0ellimcdiv  41936  coseq0  42151  sinmulcos  42152  coskpi2  42153  sinaover2ne0  42155  cosknegpi  42156  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  itgsinexp  42246  stoweidlem1  42293  stoweidlem62  42354  wallispilem4  42360  wallispilem5  42361  wallispi  42362  wallispi2lem1  42363  wallispi2lem2  42364  wallispi2  42365  stirlinglem1  42366  stirlinglem3  42368  stirlinglem4  42369  stirlinglem5  42370  stirlinglem6  42371  stirlinglem7  42372  stirlinglem8  42373  stirlinglem10  42375  stirlinglem11  42376  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  dirker2re  42384  dirkerdenne0  42385  dirkerval2  42386  dirkerre  42387  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkeritg  42394  dirkercncflem1  42395  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem43  42442  fourierdlem44  42443  fourierdlem56  42454  fourierdlem57  42455  fourierdlem58  42456  fourierdlem62  42460  fourierdlem66  42464  fourierdlem68  42466  fourierdlem72  42470  fourierdlem76  42474  fourierdlem79  42477  fourierdlem80  42478  fourierdlem83  42481  fourierdlem95  42493  fourierdlem104  42502  fourierdlem112  42510  fouriercnp  42518  fourierswlem  42522  sge0ad2en  42720  hoicvrrex  42845  hoiqssbllem2  42912  fmtnoodd  43702  sqrtpwpw2p  43707  fmtnorec2lem  43711  fmtnodvds  43713  goldbachthlem2  43715  fmtnoprmfac1lem  43733  fmtnoprmfac2  43736  fmtnofac1  43739  2pwp1prm  43758  mod42tp1mod8  43774  sfprmdvdsmersenne  43775  lighneallem2  43778  lighneallem4  43782  proththd  43786  quad1  43792  requad01  43793  requad1  43794  requad2  43795  dfodd6  43809  dfeven4  43810  enege  43817  onego  43818  dfeven2  43821  oddflALTV  43835  opoeALTV  43855  opeoALTV  43856  nn0onn0exALTV  43871  nn0enn0exALTV  43872  nnennexALTV  43873  mogoldbblem  43892  perfectALTV  43895  fppr2odd  43903  sgoldbeven3prm  43955  0nodd  44084  2nodd  44086  2zlidl  44212  2zrngamgm  44217  2zrngagrp  44221  2zrngmmgm  44224  2zrngnmlid  44227  nn0onn0ex  44590  nn0enn0ex  44591  nnennex  44592  nnpw2even  44596  fldivexpfllog2  44632  blenpw2m1  44646  nnpw2blen  44647  blennn0em1  44658  dig2nn1st  44672  dig2bits  44681  dignn0flhalflem1  44682  dignn0flhalflem2  44683  dignn0ehalf  44684  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  itschlc0yqe  44754  itsclc0yqsollem1  44756  itsclc0yqsol  44758  itsclc0xyqsolr  44763  itsclquadb  44770  2itscplem1  44772  2itscplem3  44774  itscnhlinecirc02plem1  44776