Theorem 2cnd 12316

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  2c2 12293

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-2 12301

This theorem is referenced by:  subhalfhalf  12473  cnm2m1cnm3  12492  xp1d2m1eqxm1d2  12493  zeo2  12678  ge2halflem1  13122  fzosplitprm1  13791  2tnp1ge0ge0  13844  flhalf  13845  2txmodxeq0  13947  mulbinom2  14239  binom3  14240  zesq  14242  expmulnbnd  14251  discr  14256  sqoddm1div8  14259  mulsubdivbinom2  14278  swrds2m  14958  amgm2  15386  bhmafibid1cn  15480  bhmafibid2cn  15481  iseraltlem2  15697  iseralt  15699  trirecip  15877  geo2sum  15887  bpolydiflem  16068  ege2le3  16104  tanval3  16150  sinhval  16170  tanhlt1  16176  sqrt2irrlem  16264  sqrt2irr  16265  even2n  16359  oddm1even  16360  oddp1even  16361  mod2eq1n2dvds  16364  ltoddhalfle  16378  m1exp1  16393  nn0enne  16394  flodddiv4  16432  flodddiv4t2lthalf  16435  bitsp1e  16449  bitsp1o  16450  bitsfzo  16452  bitsmod  16453  bitsinv1lem  16458  sadadd2lem2  16467  sadcaddlem  16474  bitsuz  16491  bitsshft  16492  prmdiv  16802  vfermltlALT  16820  iserodd  16853  4sqlem7  16962  4sqlem10  16965  4sqlem19  16981  prmgaplem7  17075  2expltfac  17110  smndex2dlinvh  18893  efgredlemg  19721  frgpnabllem1  19852  ablsimpgfindlem1  20088  metnrmlem3  24799  iihalf1cn  24875  iihalf1cnOLD  24876  iihalf2cn  24878  iihalf2cnOLD  24879  pcoass  24973  cphipval2  25191  csbren  25349  trirn  25350  minveclem2  25376  ovolunlem1a  25447  uniioombllem5  25538  uniioombl  25540  dyaddisjlem  25546  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  dvsincos  25935  lhop1  25969  cosargd  26567  dvcnsqrt  26703  root1id  26714  ssscongptld  26782  chordthmlem  26792  chordthmlem2  26793  chordthmlem4  26795  heron  26798  dcubic1  26805  mcubic  26807  cubic2  26808  quartlem4  26820  quart  26821  cosasin  26864  cosatan  26881  atantayl  26897  atantayl2  26898  atantayl3  26899  log2tlbnd  26905  cxp2limlem  26936  divsqrtsumlem  26940  lgamgulmlem2  26990  lgamgulmlem4  26992  lgamucov  26998  ftalem2  27034  basellem2  27042  basellem3  27043  basellem5  27045  basellem8  27048  logfaclbnd  27183  perfectlem2  27191  perfect  27192  bcp1ctr  27240  bposlem1  27245  bposlem2  27246  lgslem1  27258  lgsqrlem2  27308  gausslemma2dlem1a  27326  gausslemma2dlem3  27329  gausslemma2dlem4  27330  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem1  27345  2lgslem1a1  27350  2lgslem1a2  27351  2lgslem1b  27353  2lgslem1c  27354  2lgslem3a1  27361  2lgslem3d1  27364  2sq2  27394  addsq2nreurex  27405  chebbnd1lem3  27432  chto1ub  27437  dchrisumlem2  27451  dchrisum0flblem2  27470  dchrisum0fno1  27472  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2  27479  logdivsum  27494  mulog2sumlem2  27496  vmalogdivsum2  27499  log2sumbnd  27505  selberglem2  27507  chpdifbndlem1  27514  selberg3lem1  27518  selberg3  27520  selberg4lem1  27521  selberg4  27522  selberg4r  27531  selberg34r  27532  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2  27552  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemr  27563  pntlemk  27567  pntlemo  27568  ostth2lem1  27579  finsumvtxdg2ssteplem4  29474  upgrwlkdvdelem  29664  wwlksnextwrd  29825  wwlksnextinj  29827  clwlkclwwlklem2a1  29919  clwlkclwwlklem2a4  29924  clwlkclwwlklem3  29928  clwwlkext2edg  29983  clwwlknonex2lem1  30034  clwwlknonex2lem2  30035  2clwwlk2clwwlk  30277  numclwwlk1lem2foalem  30278  numclwwlk1lem2fo  30285  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwwlk2  30308  ex-ind-dvds  30388  nrt2irr  30400  binom2subadd  32665  quad3d  32673  2exple2exp  32770  wrdt2ind  32875  archirngz  33133  archiabllem2c  33139  fldext2rspun  33669  constrrtcc  33715  constrelextdg2  33727  constraddcl  33742  constrrecl  33749  constrresqrtcl  33757  2sqr3nconstr  33761  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  cos9thpinconstrlem1  33769  sqsscirc1  33885  dya2icoseg  34255  dya2iocucvr  34262  oddpwdc  34332  eulerpartlemgs2  34358  fibp1  34379  signslema  34540  itgexpif  34584  vtsprod  34617  hgt750lemd  34626  logdivsqrle  34628  subfacp1lem1  35147  subfacp1lem5  35152  dnibndlem10  36451  knoppcnlem10  36466  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem9  36484  knoppndvlem10  36485  knoppndvlem16  36491  irrdifflemf  37289  itg2addnclem  37641  dvasin  37674  areacirclem1  37678  areacirclem3  37680  isbnd2  37753  lcmineqlem21  42008  3lexlogpow2ineq2  42018  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p9  42047  posbezout  42059  2np3bcnp1  42103  2ap1caineq  42104  oddnumth  42307  nicomachus  42308  sumcubes  42309  ef11d  42335  cxpi11d  42339  tan3rdpi  42346  readvrec2  42351  remul02  42395  remul01  42397  dffltz  42604  fltne  42614  flt4lem5e  42626  cu3addd  42651  rmspecsqrtnq  42876  rmxluc  42907  rmyluc2  42909  rmydbl  42911  jm2.18  42959  jm2.22  42966  jm2.25  42970  jm2.27c  42978  jm3.1lem2  42989  sqrtcval  43612  imo72b2lem0  44136  refsum2cnlem1  45009  oddfl  45254  xralrple2  45329  infleinflem2  45346  sumnnodd  45607  0ellimcdiv  45626  coseq0  45841  sinmulcos  45842  coskpi2  45843  sinaover2ne0  45845  cosknegpi  45846  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  itgsinexp  45932  stoweidlem1  45978  stoweidlem62  46039  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  dirker2re  46069  dirkerdenne0  46070  dirkerval2  46071  dirkerre  46072  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkeritg  46079  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem43  46127  fourierdlem44  46128  fourierdlem56  46139  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem66  46149  fourierdlem68  46151  fourierdlem72  46155  fourierdlem76  46159  fourierdlem79  46162  fourierdlem80  46163  fourierdlem83  46166  fourierdlem95  46178  fourierdlem104  46187  fourierdlem112  46195  fouriercnp  46203  fourierswlem  46207  sge0ad2en  46408  hoicvrrex  46533  hoiqssbllem2  46600  2tceilhalfelfzo1  47309  minusmodnep2tmod  47330  fmtnoodd  47495  sqrtpwpw2p  47500  fmtnorec2lem  47504  fmtnodvds  47506  goldbachthlem2  47508  fmtnoprmfac1lem  47526  fmtnoprmfac2  47529  fmtnofac1  47532  2pwp1prm  47551  mod42tp1mod8  47564  sfprmdvdsmersenne  47565  lighneallem2  47568  lighneallem4  47572  proththd  47576  quad1  47582  requad01  47583  requad1  47584  requad2  47585  dfodd6  47599  dfeven4  47600  enege  47607  onego  47608  dfeven2  47611  oddflALTV  47625  opoeALTV  47645  opeoALTV  47646  nn0onn0exALTV  47661  nn0enn0exALTV  47662  nnennexALTV  47663  mogoldbblem  47682  perfectALTV  47685  fppr2odd  47693  sgoldbeven3prm  47745  gpg3nbgrvtx0  48026  gpg3kgrtriexlem2  48034  0nodd  48093  2nodd  48095  2zlidl  48163  2zrngamgm  48168  2zrngagrp  48172  2zrngmmgm  48175  2zrngnmlid  48178  nn0onn0ex  48451  nn0enn0ex  48452  nnennex  48453  nnpw2even  48457  fldivexpfllog2  48493  blenpw2m1  48507  nnpw2blen  48508  blennn0em1  48519  dig2nn1st  48533  dig2bits  48542  dignn0flhalflem1  48543  dignn0flhalflem2  48544  dignn0ehalf  48545  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  itcovalt2lem2lem2  48602  ackval2  48610  ackval3  48611  itschlc0yqe  48688  itsclc0yqsollem1  48690  itsclc0yqsol  48692  itsclc0xyqsolr  48697  itsclquadb  48704  2itscplem1  48706  2itscplem3  48708  itscnhlinecirc02plem1  48710