Theorem 2cnd 12206

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  2c2 12183

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12191

This theorem is referenced by:  subhalfhalf  12358  cnm2m1cnm3  12377  xp1d2m1eqxm1d2  12378  zeo2  12563  ge2halflem1  13010  fzosplitprm1  13680  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  18791  efgredlemg  19621  frgpnabllem1  19752  ablsimpgfindlem1  19988  metnrmlem3  24748  iihalf1cn  24824  iihalf1cnOLD  24825  iihalf2cn  24827  iihalf2cnOLD  24828  pcoass  24922  cphipval2  25139  csbren  25297  trirn  25298  minveclem2  25324  ovolunlem1a  25395  uniioombllem5  25486  uniioombl  25488  dyaddisjlem  25494  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  dvsincos  25883  lhop1  25917  cosargd  26515  dvcnsqrt  26651  root1id  26662  ssscongptld  26730  chordthmlem  26740  chordthmlem2  26741  chordthmlem4  26743  heron  26746  dcubic1  26753  mcubic  26755  cubic2  26756  quartlem4  26768  quart  26769  cosasin  26812  cosatan  26829  atantayl  26845  atantayl2  26846  atantayl3  26847  log2tlbnd  26853  cxp2limlem  26884  divsqrtsumlem  26888  lgamgulmlem2  26938  lgamgulmlem4  26940  lgamucov  26946  ftalem2  26982  basellem2  26990  basellem3  26991  basellem5  26993  basellem8  26996  logfaclbnd  27131  perfectlem2  27139  perfect  27140  bcp1ctr  27188  bposlem1  27193  bposlem2  27194  lgslem1  27206  lgsqrlem2  27256  gausslemma2dlem1a  27274  gausslemma2dlem3  27277  gausslemma2dlem4  27278  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquadlem2  27290  lgsquad2lem1  27293  2lgslem1a1  27298  2lgslem1a2  27299  2lgslem1b  27301  2lgslem1c  27302  2lgslem3a1  27309  2lgslem3d1  27312  2sq2  27342  addsq2nreurex  27353  chebbnd1lem3  27380  chto1ub  27385  dchrisumlem2  27399  dchrisum0flblem2  27418  dchrisum0fno1  27420  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2  27427  logdivsum  27442  mulog2sumlem2  27444  vmalogdivsum2  27447  log2sumbnd  27453  selberglem2  27455  chpdifbndlem1  27462  selberg3lem1  27466  selberg3  27468  selberg4lem1  27469  selberg4  27470  selberg4r  27479  selberg34r  27480  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntpbnd1a  27494  pntpbnd2  27496  pntibndlem2  27500  pntlemb  27506  pntlemg  27507  pntlemh  27508  pntlemr  27511  pntlemk  27515  pntlemo  27516  ostth2lem1  27527  finsumvtxdg2ssteplem4  29494  upgrwlkdvdelem  29681  wwlksnextwrd  29842  wwlksnextinj  29844  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a4  29941  clwlkclwwlklem3  29945  clwwlkext2edg  30000  clwwlknonex2lem1  30051  clwwlknonex2lem2  30052  2clwwlk2clwwlk  30294  numclwwlk1lem2foalem  30295  numclwwlk1lem2fo  30302  numclwwlk2lem1  30320  numclwlk2lem2f  30321  numclwwlk2  30325  ex-ind-dvds  30405  nrt2irr  30417  binom2subadd  32685  quad3d  32693  2exple2exp  32790  wrdt2ind  32895  archirngz  33131  archiabllem2c  33137  fldext2rspun  33649  constrrtcc  33702  constrelextdg2  33714  constraddcl  33729  constrrecl  33736  constrresqrtcl  33744  2sqr3nconstr  33748  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  cos9thpinconstr  33758  sqsscirc1  33875  dya2icoseg  34245  dya2iocucvr  34252  oddpwdc  34322  eulerpartlemgs2  34348  fibp1  34369  signslema  34530  itgexpif  34574  vtsprod  34607  hgt750lemd  34616  logdivsqrle  34618  subfacp1lem1  35152  subfacp1lem5  35157  dnibndlem10  36461  knoppcnlem10  36476  knoppndvlem2  36487  knoppndvlem7  36492  knoppndvlem9  36494  knoppndvlem10  36495  knoppndvlem16  36501  irrdifflemf  37299  itg2addnclem  37651  dvasin  37684  areacirclem1  37688  areacirclem3  37690  isbnd2  37763  lcmineqlem21  42022  3lexlogpow2ineq2  42032  dvrelog2b  42039  dvrelogpow2b  42041  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p9  42061  posbezout  42073  2np3bcnp1  42117  2ap1caineq  42118  oddnumth  42284  nicomachus  42285  sumcubes  42286  ef11d  42312  cxpi11d  42316  tan3rdpi  42325  readvrec2  42334  remul02  42378  remul01  42380  dffltz  42607  fltne  42617  flt4lem5e  42629  cu3addd  42654  rmspecsqrtnq  42879  rmxluc  42909  rmyluc2  42911  rmydbl  42913  jm2.18  42961  jm2.22  42968  jm2.25  42972  jm2.27c  42980  jm3.1lem2  42991  sqrtcval  43614  imo72b2lem0  44138  refsum2cnlem1  45015  oddfl  45260  xralrple2  45334  infleinflem2  45350  sumnnodd  45611  0ellimcdiv  45630  coseq0  45845  sinmulcos  45846  coskpi2  45847  sinaover2ne0  45849  cosknegpi  45850  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  itgsinexp  45936  stoweidlem1  45982  stoweidlem62  46043  wallispilem4  46049  wallispilem5  46050  wallispi  46051  wallispi2lem1  46052  wallispi2lem2  46053  wallispi2  46054  stirlinglem1  46055  stirlinglem3  46057  stirlinglem4  46058  stirlinglem5  46059  stirlinglem6  46060  stirlinglem7  46061  stirlinglem8  46062  stirlinglem10  46064  stirlinglem11  46065  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  dirker2re  46073  dirkerdenne0  46074  dirkerval2  46075  dirkerre  46076  dirkertrigeqlem1  46079  dirkertrigeqlem2  46080  dirkertrigeqlem3  46081  dirkertrigeq  46082  dirkeritg  46083  dirkercncflem1  46084  dirkercncflem2  46085  dirkercncflem4  46087  fourierdlem43  46131  fourierdlem44  46132  fourierdlem56  46143  fourierdlem57  46144  fourierdlem58  46145  fourierdlem62  46149  fourierdlem66  46153  fourierdlem68  46155  fourierdlem72  46159  fourierdlem76  46163  fourierdlem79  46166  fourierdlem80  46167  fourierdlem83  46170  fourierdlem95  46182  fourierdlem104  46191  fourierdlem112  46199  fouriercnp  46207  fourierswlem  46211  sge0ad2en  46412  hoicvrrex  46537  hoiqssbllem2  46604  2tceilhalfelfzo1  47316  minusmodnep2tmod  47337  modmkpkne  47345  modm2nep1  47350  modm1nem2  47353  fmtnoodd  47517  sqrtpwpw2p  47522  fmtnorec2lem  47526  fmtnodvds  47528  goldbachthlem2  47530  fmtnoprmfac1lem  47548  fmtnoprmfac2  47551  fmtnofac1  47554  2pwp1prm  47573  mod42tp1mod8  47586  sfprmdvdsmersenne  47587  lighneallem2  47590  lighneallem4  47594  proththd  47598  quad1  47604  requad01  47605  requad1  47606  requad2  47607  dfodd6  47621  dfeven4  47622  enege  47629  onego  47630  dfeven2  47633  oddflALTV  47647  opoeALTV  47667  opeoALTV  47668  nn0onn0exALTV  47683  nn0enn0exALTV  47684  nnennexALTV  47685  mogoldbblem  47704  perfectALTV  47707  fppr2odd  47715  sgoldbeven3prm  47767  gpg3nbgrvtx0  48060  gpg3kgrtriexlem2  48068  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  0nodd  48154  2nodd  48156  2zlidl  48224  2zrngamgm  48229  2zrngagrp  48233  2zrngmmgm  48236  2zrngnmlid  48239  nn0onn0ex  48508  nn0enn0ex  48509  nnennex  48510  nnpw2even  48514  fldivexpfllog2  48550  blenpw2m1  48564  nnpw2blen  48565  blennn0em1  48576  dig2nn1st  48590  dig2bits  48599  dignn0flhalflem1  48600  dignn0flhalflem2  48601  dignn0ehalf  48602  nn0sumshdiglemA  48604  nn0sumshdiglemB  48605  itcovalt2lem2lem2  48659  ackval2  48667  ackval3  48668  itschlc0yqe  48745  itsclc0yqsollem1  48747  itsclc0yqsol  48749  itsclc0xyqsolr  48754  itsclquadb  48761  2itscplem1  48763  2itscplem3  48765  itscnhlinecirc02plem1  48767