Theorem 2cnd 12253

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  2c2 12230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238

This theorem is referenced by:  subhalfhalf  12405  cnm2m1cnm3  12424  xp1d2m1eqxm1d2  12425  zeo2  12610  ge2halflem1  13053  fzosplitprm1  13727  2tnp1ge0ge0  13782  flhalf  13783  2txmodxeq0  13887  mulbinom2  14179  binom3  14180  zesq  14182  expmulnbnd  14191  discr  14196  sqoddm1div8  14199  mulsubdivbinom2  14218  swrds2m  14897  amgm2  15326  bhmafibid1cn  15422  bhmafibid2cn  15423  iseraltlem2  15639  iseralt  15641  trirecip  15822  geo2sum  15832  bpolydiflem  16013  ege2le3  16049  tanval3  16095  sinhval  16115  tanhlt1  16121  sqrt2irrlem  16209  sqrt2irr  16210  even2n  16305  oddm1even  16306  oddp1even  16307  mod2eq1n2dvds  16310  ltoddhalfle  16324  m1exp1  16339  nn0enne  16340  flodddiv4  16378  flodddiv4t2lthalf  16381  bitsp1e  16395  bitsp1o  16396  bitsfzo  16398  bitsmod  16399  bitsinv1lem  16404  sadadd2lem2  16413  sadcaddlem  16420  bitsuz  16437  bitsshft  16438  prmdiv  16749  vfermltlALT  16767  iserodd  16800  4sqlem7  16909  4sqlem10  16912  4sqlem19  16928  prmgaplem7  17022  2expltfac  17057  smndex2dlinvh  18882  efgredlemg  19711  frgpnabllem1  19842  ablsimpgfindlem1  20078  metnrmlem3  24840  iihalf1cn  24912  iihalf2cn  24914  pcoass  25004  cphipval2  25221  csbren  25379  trirn  25380  minveclem2  25406  ovolunlem1a  25476  uniioombllem5  25567  uniioombl  25569  dyaddisjlem  25575  mbfi1fseqlem5  25699  mbfi1fseqlem6  25700  dvsincos  25961  lhop1  25994  cosargd  26588  dvcnsqrt  26724  root1id  26734  ssscongptld  26802  chordthmlem  26812  chordthmlem2  26813  chordthmlem4  26815  heron  26818  dcubic1  26825  mcubic  26827  cubic2  26828  quartlem4  26840  quart  26841  cosasin  26884  cosatan  26901  atantayl  26917  atantayl2  26918  atantayl3  26919  log2tlbnd  26925  cxp2limlem  26956  divsqrtsumlem  26960  lgamgulmlem2  27010  lgamgulmlem4  27012  lgamucov  27018  ftalem2  27054  basellem2  27062  basellem3  27063  basellem5  27065  basellem8  27068  logfaclbnd  27202  perfectlem2  27210  perfect  27211  bcp1ctr  27259  bposlem1  27264  bposlem2  27265  lgslem1  27277  lgsqrlem2  27327  gausslemma2dlem1a  27345  gausslemma2dlem3  27348  gausslemma2dlem4  27349  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgsquadlem1  27360  lgsquadlem2  27361  lgsquad2lem1  27364  2lgslem1a1  27369  2lgslem1a2  27370  2lgslem1b  27372  2lgslem1c  27373  2lgslem3a1  27380  2lgslem3d1  27383  2sq2  27413  addsq2nreurex  27424  chebbnd1lem3  27451  chto1ub  27456  dchrisumlem2  27470  dchrisum0flblem2  27489  dchrisum0fno1  27491  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2  27498  logdivsum  27513  mulog2sumlem2  27515  vmalogdivsum2  27518  log2sumbnd  27524  selberglem2  27526  chpdifbndlem1  27533  selberg3lem1  27537  selberg3  27539  selberg4lem1  27540  selberg4  27541  selberg4r  27550  selberg34r  27551  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntpbnd1a  27565  pntpbnd2  27567  pntibndlem2  27571  pntlemb  27577  pntlemg  27578  pntlemh  27579  pntlemr  27582  pntlemk  27586  pntlemo  27587  ostth2lem1  27598  finsumvtxdg2ssteplem4  29635  upgrwlkdvdelem  29822  wwlksnextwrd  29983  wwlksnextinj  29985  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem3  30089  clwwlkext2edg  30144  clwwlknonex2lem1  30195  clwwlknonex2lem2  30196  2clwwlk2clwwlk  30438  numclwwlk1lem2foalem  30439  numclwwlk1lem2fo  30446  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwwlk2  30469  ex-ind-dvds  30549  nrt2irr  30561  binom2subadd  32832  quad3d  32840  2exple2exp  32936  wrdt2ind  33031  archirngz  33268  archiabllem2c  33274  fldext2rspun  33845  constrrtcc  33898  constrelextdg2  33910  constraddcl  33925  constrrecl  33932  constrresqrtcl  33940  2sqr3nconstr  33944  cos9thpiminplylem1  33945  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  cos9thpiminply  33951  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  cos9thpinconstr  33954  sqsscirc1  34071  dya2icoseg  34440  dya2iocucvr  34447  oddpwdc  34517  eulerpartlemgs2  34543  fibp1  34564  signslema  34725  itgexpif  34769  vtsprod  34802  hgt750lemd  34811  logdivsqrle  34813  subfacp1lem1  35380  subfacp1lem5  35385  dnibndlem10  36766  knoppcnlem10  36781  knoppndvlem2  36792  knoppndvlem7  36797  knoppndvlem9  36799  knoppndvlem10  36800  knoppndvlem16  36806  irrdifflemf  37658  itg2addnclem  38009  dvasin  38042  areacirclem1  38046  areacirclem3  38048  isbnd2  38121  lcmineqlem21  42505  3lexlogpow2ineq2  42515  dvrelog2b  42522  dvrelogpow2b  42524  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p9  42544  posbezout  42556  2np3bcnp1  42600  2ap1caineq  42601  oddnumth  42760  nicomachus  42761  sumcubes  42762  ef11d  42788  cxpi11d  42792  tan3rdpi  42801  readvrec2  42810  remul02  42854  remul01  42856  dffltz  43084  fltne  43094  flt4lem5e  43106  cu3addd  43130  rmspecsqrtnq  43355  rmxluc  43385  rmyluc2  43387  rmydbl  43389  jm2.18  43437  jm2.22  43444  jm2.25  43448  jm2.27c  43456  jm3.1lem2  43467  sqrtcval  44089  imo72b2lem0  44613  refsum2cnlem1  45489  oddfl  45732  xralrple2  45805  infleinflem2  45821  sumnnodd  46081  0ellimcdiv  46098  coseq0  46313  sinmulcos  46314  coskpi2  46315  sinaover2ne0  46317  cosknegpi  46318  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  itgsinexp  46404  stoweidlem1  46450  stoweidlem62  46511  wallispilem4  46517  wallispilem5  46518  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem1  46523  stirlinglem3  46525  stirlinglem4  46526  stirlinglem5  46527  stirlinglem6  46528  stirlinglem7  46529  stirlinglem8  46530  stirlinglem10  46532  stirlinglem11  46533  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  dirker2re  46541  dirkerdenne0  46542  dirkerval2  46543  dirkerre  46544  dirkertrigeqlem1  46547  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkeritg  46551  dirkercncflem1  46552  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem43  46599  fourierdlem44  46600  fourierdlem56  46611  fourierdlem57  46612  fourierdlem58  46613  fourierdlem62  46617  fourierdlem66  46621  fourierdlem68  46623  fourierdlem72  46627  fourierdlem76  46631  fourierdlem79  46634  fourierdlem80  46635  fourierdlem83  46638  fourierdlem95  46650  fourierdlem104  46659  fourierdlem112  46667  fouriercnp  46675  fourierswlem  46679  sge0ad2en  46880  hoicvrrex  47005  hoiqssbllem2  47072  sin3t  47338  cos3t  47339  sin5tlem1  47340  sin5tlem3  47342  sin5tlem4  47343  sin5t  47345  2tceilhalfelfzo1  47799  minusmodnep2tmod  47822  modmkpkne  47830  modm2nep1  47835  modm1nem2  47838  fmtnoodd  48011  sqrtpwpw2p  48016  fmtnorec2lem  48020  fmtnodvds  48022  goldbachthlem2  48024  fmtnoprmfac1lem  48042  fmtnoprmfac2  48045  fmtnofac1  48048  2pwp1prm  48067  mod42tp1mod8  48080  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem4  48088  proththd  48092  nprmdvdsfacm1lem1  48098  ppivalnn4  48105  quad1  48111  requad01  48112  requad1  48113  requad2  48114  dfodd6  48128  dfeven4  48129  enege  48136  onego  48137  dfeven2  48140  oddflALTV  48154  opoeALTV  48174  opeoALTV  48175  nn0onn0exALTV  48190  nn0enn0exALTV  48191  nnennexALTV  48192  mogoldbblem  48211  perfectALTV  48214  fppr2odd  48222  sgoldbeven3prm  48274  gpg3nbgrvtx0  48567  gpg3kgrtriexlem2  48575  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  0nodd  48661  2nodd  48663  2zlidl  48731  2zrngamgm  48736  2zrngagrp  48740  2zrngmmgm  48743  2zrngnmlid  48746  nn0onn0ex  49014  nn0enn0ex  49015  nnennex  49016  nnpw2even  49020  fldivexpfllog2  49056  blenpw2m1  49070  nnpw2blen  49071  blennn0em1  49082  dig2nn1st  49096  dig2bits  49105  dignn0flhalflem1  49106  dignn0flhalflem2  49107  dignn0ehalf  49108  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  itcovalt2lem2lem2  49165  ackval2  49173  ackval3  49174  itschlc0yqe  49251  itsclc0yqsollem1  49253  itsclc0yqsol  49255  itsclc0xyqsolr  49260  itsclquadb  49267  2itscplem1  49269  2itscplem3  49271  itscnhlinecirc02plem1  49273