Theorem 2cnd 12203

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  2c2 12180

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12188

This theorem is referenced by:  subhalfhalf  12355  cnm2m1cnm3  12374  xp1d2m1eqxm1d2  12375  zeo2  12560  ge2halflem1  13007  fzosplitprm1  13678  2tnp1ge0ge0  13733  flhalf  13734  2txmodxeq0  13838  mulbinom2  14130  binom3  14131  zesq  14133  expmulnbnd  14142  discr  14147  sqoddm1div8  14150  mulsubdivbinom2  14169  swrds2m  14848  amgm2  15277  bhmafibid1cn  15373  bhmafibid2cn  15374  iseraltlem2  15590  iseralt  15592  trirecip  15770  geo2sum  15780  bpolydiflem  15961  ege2le3  15997  tanval3  16043  sinhval  16063  tanhlt1  16069  sqrt2irrlem  16157  sqrt2irr  16158  even2n  16253  oddm1even  16254  oddp1even  16255  mod2eq1n2dvds  16258  ltoddhalfle  16272  m1exp1  16287  nn0enne  16288  flodddiv4  16326  flodddiv4t2lthalf  16329  bitsp1e  16343  bitsp1o  16344  bitsfzo  16346  bitsmod  16347  bitsinv1lem  16352  sadadd2lem2  16361  sadcaddlem  16368  bitsuz  16385  bitsshft  16386  prmdiv  16696  vfermltlALT  16714  iserodd  16747  4sqlem7  16856  4sqlem10  16859  4sqlem19  16875  prmgaplem7  16969  2expltfac  17004  smndex2dlinvh  18825  efgredlemg  19654  frgpnabllem1  19785  ablsimpgfindlem1  20021  metnrmlem3  24777  iihalf1cn  24853  iihalf1cnOLD  24854  iihalf2cn  24856  iihalf2cnOLD  24857  pcoass  24951  cphipval2  25168  csbren  25326  trirn  25327  minveclem2  25353  ovolunlem1a  25424  uniioombllem5  25515  uniioombl  25517  dyaddisjlem  25523  mbfi1fseqlem5  25647  mbfi1fseqlem6  25648  dvsincos  25912  lhop1  25946  cosargd  26544  dvcnsqrt  26680  root1id  26691  ssscongptld  26759  chordthmlem  26769  chordthmlem2  26770  chordthmlem4  26772  heron  26775  dcubic1  26782  mcubic  26784  cubic2  26785  quartlem4  26797  quart  26798  cosasin  26841  cosatan  26858  atantayl  26874  atantayl2  26875  atantayl3  26876  log2tlbnd  26882  cxp2limlem  26913  divsqrtsumlem  26917  lgamgulmlem2  26967  lgamgulmlem4  26969  lgamucov  26975  ftalem2  27011  basellem2  27019  basellem3  27020  basellem5  27022  basellem8  27025  logfaclbnd  27160  perfectlem2  27168  perfect  27169  bcp1ctr  27217  bposlem1  27222  bposlem2  27223  lgslem1  27235  lgsqrlem2  27285  gausslemma2dlem1a  27303  gausslemma2dlem3  27306  gausslemma2dlem4  27307  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgsquadlem1  27318  lgsquadlem2  27319  lgsquad2lem1  27322  2lgslem1a1  27327  2lgslem1a2  27328  2lgslem1b  27330  2lgslem1c  27331  2lgslem3a1  27338  2lgslem3d1  27341  2sq2  27371  addsq2nreurex  27382  chebbnd1lem3  27409  chto1ub  27414  dchrisumlem2  27428  dchrisum0flblem2  27447  dchrisum0fno1  27449  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2  27456  logdivsum  27471  mulog2sumlem2  27473  vmalogdivsum2  27476  log2sumbnd  27482  selberglem2  27484  chpdifbndlem1  27491  selberg3lem1  27495  selberg3  27497  selberg4lem1  27498  selberg4  27499  selberg4r  27508  selberg34r  27509  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntpbnd1a  27523  pntpbnd2  27525  pntibndlem2  27529  pntlemb  27535  pntlemg  27536  pntlemh  27537  pntlemr  27540  pntlemk  27544  pntlemo  27545  ostth2lem1  27556  finsumvtxdg2ssteplem4  29527  upgrwlkdvdelem  29714  wwlksnextwrd  29875  wwlksnextinj  29877  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a4  29977  clwlkclwwlklem3  29981  clwwlkext2edg  30036  clwwlknonex2lem1  30087  clwwlknonex2lem2  30088  2clwwlk2clwwlk  30330  numclwwlk1lem2foalem  30331  numclwwlk1lem2fo  30338  numclwwlk2lem1  30356  numclwlk2lem2f  30357  numclwwlk2  30361  ex-ind-dvds  30441  nrt2irr  30453  binom2subadd  32725  quad3d  32733  2exple2exp  32828  wrdt2ind  32934  archirngz  33158  archiabllem2c  33164  fldext2rspun  33695  constrrtcc  33748  constrelextdg2  33760  constraddcl  33775  constrrecl  33782  constrresqrtcl  33790  2sqr3nconstr  33794  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  cos9thpiminply  33801  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  cos9thpinconstr  33804  sqsscirc1  33921  dya2icoseg  34290  dya2iocucvr  34297  oddpwdc  34367  eulerpartlemgs2  34393  fibp1  34414  signslema  34575  itgexpif  34619  vtsprod  34652  hgt750lemd  34661  logdivsqrle  34663  subfacp1lem1  35223  subfacp1lem5  35228  dnibndlem10  36529  knoppcnlem10  36544  knoppndvlem2  36555  knoppndvlem7  36560  knoppndvlem9  36562  knoppndvlem10  36563  knoppndvlem16  36569  irrdifflemf  37367  itg2addnclem  37719  dvasin  37752  areacirclem1  37756  areacirclem3  37758  isbnd2  37831  lcmineqlem21  42090  3lexlogpow2ineq2  42100  dvrelog2b  42107  dvrelogpow2b  42109  aks4d1p1p4  42112  aks4d1p1p6  42114  aks4d1p1p7  42115  aks4d1p1p5  42116  aks4d1p9  42129  posbezout  42141  2np3bcnp1  42185  2ap1caineq  42186  oddnumth  42352  nicomachus  42353  sumcubes  42354  ef11d  42380  cxpi11d  42384  tan3rdpi  42393  readvrec2  42402  remul02  42446  remul01  42448  dffltz  42675  fltne  42685  flt4lem5e  42697  cu3addd  42722  rmspecsqrtnq  42947  rmxluc  42977  rmyluc2  42979  rmydbl  42981  jm2.18  43029  jm2.22  43036  jm2.25  43040  jm2.27c  43048  jm3.1lem2  43059  sqrtcval  43682  imo72b2lem0  44206  refsum2cnlem1  45082  oddfl  45327  xralrple2  45401  infleinflem2  45417  sumnnodd  45678  0ellimcdiv  45695  coseq0  45910  sinmulcos  45911  coskpi2  45912  sinaover2ne0  45914  cosknegpi  45915  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  itgsinexp  46001  stoweidlem1  46047  stoweidlem62  46108  wallispilem4  46114  wallispilem5  46115  wallispi  46116  wallispi2lem1  46117  wallispi2lem2  46118  wallispi2  46119  stirlinglem1  46120  stirlinglem3  46122  stirlinglem4  46123  stirlinglem5  46124  stirlinglem6  46125  stirlinglem7  46126  stirlinglem8  46127  stirlinglem10  46129  stirlinglem11  46130  stirlinglem13  46132  stirlinglem14  46133  stirlinglem15  46134  dirker2re  46138  dirkerdenne0  46139  dirkerval2  46140  dirkerre  46141  dirkertrigeqlem1  46144  dirkertrigeqlem2  46145  dirkertrigeqlem3  46146  dirkertrigeq  46147  dirkeritg  46148  dirkercncflem1  46149  dirkercncflem2  46150  dirkercncflem4  46152  fourierdlem43  46196  fourierdlem44  46197  fourierdlem56  46208  fourierdlem57  46209  fourierdlem58  46210  fourierdlem62  46214  fourierdlem66  46218  fourierdlem68  46220  fourierdlem72  46224  fourierdlem76  46228  fourierdlem79  46231  fourierdlem80  46232  fourierdlem83  46235  fourierdlem95  46247  fourierdlem104  46256  fourierdlem112  46264  fouriercnp  46272  fourierswlem  46276  sge0ad2en  46477  hoicvrrex  46602  hoiqssbllem2  46669  2tceilhalfelfzo1  47371  minusmodnep2tmod  47392  modmkpkne  47400  modm2nep1  47405  modm1nem2  47408  fmtnoodd  47572  sqrtpwpw2p  47577  fmtnorec2lem  47581  fmtnodvds  47583  goldbachthlem2  47585  fmtnoprmfac1lem  47603  fmtnoprmfac2  47606  fmtnofac1  47609  2pwp1prm  47628  mod42tp1mod8  47641  sfprmdvdsmersenne  47642  lighneallem2  47645  lighneallem4  47649  proththd  47653  quad1  47659  requad01  47660  requad1  47661  requad2  47662  dfodd6  47676  dfeven4  47677  enege  47684  onego  47685  dfeven2  47688  oddflALTV  47702  opoeALTV  47722  opeoALTV  47723  nn0onn0exALTV  47738  nn0enn0exALTV  47739  nnennexALTV  47740  mogoldbblem  47759  perfectALTV  47762  fppr2odd  47770  sgoldbeven3prm  47822  gpg3nbgrvtx0  48115  gpg3kgrtriexlem2  48123  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  pgnbgreunbgrlem2lem3  48155  0nodd  48209  2nodd  48211  2zlidl  48279  2zrngamgm  48284  2zrngagrp  48288  2zrngmmgm  48291  2zrngnmlid  48294  nn0onn0ex  48563  nn0enn0ex  48564  nnennex  48565  nnpw2even  48569  fldivexpfllog2  48605  blenpw2m1  48619  nnpw2blen  48620  blennn0em1  48631  dig2nn1st  48645  dig2bits  48654  dignn0flhalflem1  48655  dignn0flhalflem2  48656  dignn0ehalf  48657  nn0sumshdiglemA  48659  nn0sumshdiglemB  48660  itcovalt2lem2lem2  48714  ackval2  48722  ackval3  48723  itschlc0yqe  48800  itsclc0yqsollem1  48802  itsclc0yqsol  48804  itsclc0xyqsolr  48809  itsclquadb  48816  2itscplem1  48818  2itscplem3  48820  itscnhlinecirc02plem1  48822