Theorem 2cnd 12223

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208

This theorem is referenced by:  subhalfhalf  12375  cnm2m1cnm3  12394  xp1d2m1eqxm1d2  12395  zeo2  12579  ge2halflem1  13022  fzosplitprm1  13694  2tnp1ge0ge0  13749  flhalf  13750  2txmodxeq0  13854  mulbinom2  14146  binom3  14147  zesq  14149  expmulnbnd  14158  discr  14163  sqoddm1div8  14166  mulsubdivbinom2  14185  swrds2m  14864  amgm2  15293  bhmafibid1cn  15389  bhmafibid2cn  15390  iseraltlem2  15606  iseralt  15608  trirecip  15786  geo2sum  15796  bpolydiflem  15977  ege2le3  16013  tanval3  16059  sinhval  16079  tanhlt1  16085  sqrt2irrlem  16173  sqrt2irr  16174  even2n  16269  oddm1even  16270  oddp1even  16271  mod2eq1n2dvds  16274  ltoddhalfle  16288  m1exp1  16303  nn0enne  16304  flodddiv4  16342  flodddiv4t2lthalf  16345  bitsp1e  16359  bitsp1o  16360  bitsfzo  16362  bitsmod  16363  bitsinv1lem  16368  sadadd2lem2  16377  sadcaddlem  16384  bitsuz  16401  bitsshft  16402  prmdiv  16712  vfermltlALT  16730  iserodd  16763  4sqlem7  16872  4sqlem10  16875  4sqlem19  16891  prmgaplem7  16985  2expltfac  17020  smndex2dlinvh  18842  efgredlemg  19671  frgpnabllem1  19802  ablsimpgfindlem1  20038  metnrmlem3  24806  iihalf1cn  24882  iihalf1cnOLD  24883  iihalf2cn  24885  iihalf2cnOLD  24886  pcoass  24980  cphipval2  25197  csbren  25355  trirn  25356  minveclem2  25382  ovolunlem1a  25453  uniioombllem5  25544  uniioombl  25546  dyaddisjlem  25552  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  dvsincos  25941  lhop1  25975  cosargd  26573  dvcnsqrt  26709  root1id  26720  ssscongptld  26788  chordthmlem  26798  chordthmlem2  26799  chordthmlem4  26801  heron  26804  dcubic1  26811  mcubic  26813  cubic2  26814  quartlem4  26826  quart  26827  cosasin  26870  cosatan  26887  atantayl  26903  atantayl2  26904  atantayl3  26905  log2tlbnd  26911  cxp2limlem  26942  divsqrtsumlem  26946  lgamgulmlem2  26996  lgamgulmlem4  26998  lgamucov  27004  ftalem2  27040  basellem2  27048  basellem3  27049  basellem5  27051  basellem8  27054  logfaclbnd  27189  perfectlem2  27197  perfect  27198  bcp1ctr  27246  bposlem1  27251  bposlem2  27252  lgslem1  27264  lgsqrlem2  27314  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  gausslemma2dlem4  27336  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem1  27351  2lgslem1a1  27356  2lgslem1a2  27357  2lgslem1b  27359  2lgslem1c  27360  2lgslem3a1  27367  2lgslem3d1  27370  2sq2  27400  addsq2nreurex  27411  chebbnd1lem3  27438  chto1ub  27443  dchrisumlem2  27457  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2  27485  logdivsum  27500  mulog2sumlem2  27502  vmalogdivsum2  27505  log2sumbnd  27511  selberglem2  27513  chpdifbndlem1  27520  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selberg4  27528  selberg4r  27537  selberg34r  27538  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem2  27558  pntlemb  27564  pntlemg  27565  pntlemh  27566  pntlemr  27569  pntlemk  27573  pntlemo  27574  ostth2lem1  27585  finsumvtxdg2ssteplem4  29622  upgrwlkdvdelem  29809  wwlksnextwrd  29970  wwlksnextinj  29972  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a4  30072  clwlkclwwlklem3  30076  clwwlkext2edg  30131  clwwlknonex2lem1  30182  clwwlknonex2lem2  30183  2clwwlk2clwwlk  30425  numclwwlk1lem2foalem  30426  numclwwlk1lem2fo  30433  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwwlk2  30456  ex-ind-dvds  30536  nrt2irr  30548  binom2subadd  32821  quad3d  32829  2exple2exp  32926  wrdt2ind  33035  archirngz  33271  archiabllem2c  33277  fldext2rspun  33839  constrrtcc  33892  constrelextdg2  33904  constraddcl  33919  constrrecl  33926  constrresqrtcl  33934  2sqr3nconstr  33938  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  sqsscirc1  34065  dya2icoseg  34434  dya2iocucvr  34441  oddpwdc  34511  eulerpartlemgs2  34537  fibp1  34558  signslema  34719  itgexpif  34763  vtsprod  34796  hgt750lemd  34805  logdivsqrle  34807  subfacp1lem1  35373  subfacp1lem5  35378  dnibndlem10  36687  knoppcnlem10  36702  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem9  36720  knoppndvlem10  36721  knoppndvlem16  36727  irrdifflemf  37530  itg2addnclem  37872  dvasin  37905  areacirclem1  37909  areacirclem3  37911  isbnd2  37984  lcmineqlem21  42303  3lexlogpow2ineq2  42313  dvrelog2b  42320  dvrelogpow2b  42322  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p9  42342  posbezout  42354  2np3bcnp1  42398  2ap1caineq  42399  oddnumth  42566  nicomachus  42567  sumcubes  42568  ef11d  42594  cxpi11d  42598  tan3rdpi  42607  readvrec2  42616  remul02  42660  remul01  42662  dffltz  42877  fltne  42887  flt4lem5e  42899  cu3addd  42923  rmspecsqrtnq  43148  rmxluc  43178  rmyluc2  43180  rmydbl  43182  jm2.18  43230  jm2.22  43237  jm2.25  43241  jm2.27c  43249  jm3.1lem2  43260  sqrtcval  43882  imo72b2lem0  44406  refsum2cnlem1  45282  oddfl  45526  xralrple2  45599  infleinflem2  45615  sumnnodd  45876  0ellimcdiv  45893  coseq0  46108  sinmulcos  46109  coskpi2  46110  sinaover2ne0  46112  cosknegpi  46113  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  itgsinexp  46199  stoweidlem1  46245  stoweidlem62  46306  wallispilem4  46312  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  stirlinglem11  46328  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirker2re  46336  dirkerdenne0  46337  dirkerval2  46338  dirkerre  46339  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkeritg  46346  dirkercncflem1  46347  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem43  46394  fourierdlem44  46395  fourierdlem56  46406  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem66  46416  fourierdlem68  46418  fourierdlem72  46422  fourierdlem76  46426  fourierdlem79  46429  fourierdlem80  46430  fourierdlem83  46433  fourierdlem95  46445  fourierdlem104  46454  fourierdlem112  46462  fouriercnp  46470  fourierswlem  46474  sge0ad2en  46675  hoicvrrex  46800  hoiqssbllem2  46867  2tceilhalfelfzo1  47578  minusmodnep2tmod  47599  modmkpkne  47607  modm2nep1  47612  modm1nem2  47615  fmtnoodd  47779  sqrtpwpw2p  47784  fmtnorec2lem  47788  fmtnodvds  47790  goldbachthlem2  47792  fmtnoprmfac1lem  47810  fmtnoprmfac2  47813  fmtnofac1  47816  2pwp1prm  47835  mod42tp1mod8  47848  sfprmdvdsmersenne  47849  lighneallem2  47852  lighneallem4  47856  proththd  47860  quad1  47866  requad01  47867  requad1  47868  requad2  47869  dfodd6  47883  dfeven4  47884  enege  47891  onego  47892  dfeven2  47895  oddflALTV  47909  opoeALTV  47929  opeoALTV  47930  nn0onn0exALTV  47945  nn0enn0exALTV  47946  nnennexALTV  47947  mogoldbblem  47966  perfectALTV  47969  fppr2odd  47977  sgoldbeven3prm  48029  gpg3nbgrvtx0  48322  gpg3kgrtriexlem2  48330  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  0nodd  48416  2nodd  48418  2zlidl  48486  2zrngamgm  48491  2zrngagrp  48495  2zrngmmgm  48498  2zrngnmlid  48501  nn0onn0ex  48769  nn0enn0ex  48770  nnennex  48771  nnpw2even  48775  fldivexpfllog2  48811  blenpw2m1  48825  nnpw2blen  48826  blennn0em1  48837  dig2nn1st  48851  dig2bits  48860  dignn0flhalflem1  48861  dignn0flhalflem2  48862  dignn0ehalf  48863  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  itcovalt2lem2lem2  48920  ackval2  48928  ackval3  48929  itschlc0yqe  49006  itsclc0yqsollem1  49008  itsclc0yqsol  49010  itsclc0xyqsolr  49015  itsclquadb  49022  2itscplem1  49024  2itscplem3  49026  itscnhlinecirc02plem1  49028