Theorem 2cnd 12318

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11097  2c2 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-addcl 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12302

This theorem is referenced by:  subhalfhalf  12477  cnm2m1cnm3  12496  xp1d2m1eqxm1d2  12497  zeo2  12682  ge2halflem1  13132  fzosplitprm1  13806  2tnp1ge0ge0  13861  flhalf  13862  2txmodxeq0  13966  mulbinom2  14258  binom3  14259  zesq  14261  expmulnbnd  14270  discr  14275  sqoddm1div8  14278  mulsubdivbinom2  14297  swrds2m  14977  amgm2  15420  bhmafibid1cn  15516  bhmafibid2cn  15517  iseraltlem2  15733  iseralt  15735  trirecip  15916  geo2sum  15926  bpolydiflem  16107  ege2le3  16143  tanval3  16189  sinhval  16209  tanhlt1  16215  sqrt2irrlem  16303  sqrt2irr  16304  even2n  16399  oddm1even  16400  oddp1even  16401  mod2eq1n2dvds  16404  ltoddhalfle  16418  m1exp1  16433  nn0enne  16434  flodddiv4  16472  flodddiv4t2lthalf  16475  bitsp1e  16489  bitsp1o  16490  bitsfzo  16492  bitsmod  16493  bitsinv1lem  16498  sadadd2lem2  16507  sadcaddlem  16514  bitsuz  16531  bitsshft  16532  prmdiv  16843  vfermltlALT  16861  iserodd  16894  4sqlem7  17003  4sqlem10  17006  4sqlem19  17022  prmgaplem7  17116  2expltfac  17151  smndex2dlinvh  18978  efgredlemg  19811  frgpnabllem1  19942  ablsimpgfindlem1  20178  metnrmlem3  24987  iihalf1cn  25059  iihalf2cn  25061  pcoass  25151  cphipval2  25368  csbren  25526  trirn  25527  minveclem2  25553  ovolunlem1a  25623  uniioombllem5  25714  uniioombl  25716  dyaddisjlem  25722  mbfi1fseqlem5  25846  mbfi1fseqlem6  25847  dvsincos  26108  lhop1  26141  cosargd  26738  dvcnsqrt  26874  root1id  26884  ssscongptld  26952  chordthmlem  26962  chordthmlem2  26963  chordthmlem4  26965  heron  26968  dcubic1  26975  mcubic  26977  cubic2  26978  quartlem4  26990  quart  26991  cosasin  27034  cosatan  27051  atantayl  27067  atantayl2  27068  atantayl3  27069  log2tlbnd  27075  cxp2limlem  27105  divsqrtsumlem  27109  lgamgulmlem2  27159  lgamgulmlem4  27161  lgamucov  27167  ftalem2  27203  basellem2  27211  basellem3  27212  basellem5  27214  basellem8  27217  logfaclbnd  27351  perfectlem2  27359  perfect  27360  bcp1ctr  27408  bposlem1  27413  bposlem2  27414  lgslem1  27426  lgsqrlem2  27476  gausslemma2dlem1a  27494  gausslemma2dlem3  27497  gausslemma2dlem4  27498  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgsquadlem1  27509  lgsquadlem2  27510  lgsquad2lem1  27513  2lgslem1a1  27518  2lgslem1a2  27519  2lgslem1b  27521  2lgslem1c  27522  2lgslem3a1  27529  2lgslem3d1  27532  2sq2  27562  addsq2nreurex  27573  chebbnd1lem3  27600  chto1ub  27605  dchrisumlem2  27619  dchrisum0flblem2  27638  dchrisum0fno1  27640  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2  27647  logdivsum  27662  mulog2sumlem2  27664  vmalogdivsum2  27667  log2sumbnd  27673  selberglem2  27675  chpdifbndlem1  27682  selberg3lem1  27686  selberg3  27688  selberg4lem1  27689  selberg4  27690  selberg4r  27699  selberg34r  27700  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntpbnd1a  27714  pntpbnd2  27716  pntibndlem2  27720  pntlemb  27726  pntlemg  27727  pntlemh  27728  pntlemr  27731  pntlemk  27735  pntlemo  27736  ostth2lem1  27747  finsumvtxdg2ssteplem4  29838  upgrwlkdvdelem  30025  wwlksnextwrd  30186  wwlksnextinj  30188  clwlkclwwlklem2a1  30283  clwlkclwwlklem2a4  30288  clwlkclwwlklem3  30292  clwwlkext2edg  30347  clwwlknonex2lem1  30398  clwwlknonex2lem2  30399  2clwwlk2clwwlk  30641  numclwwlk1lem2foalem  30642  numclwwlk1lem2fo  30649  numclwwlk2lem1  30667  numclwlk2lem2f  30668  numclwwlk2  30672  ex-ind-dvds  30752  nrt2irr  30764  binom2subadd  33026  quad3d  33034  2exple2exp  33118  wrdt2ind  33213  archirngz  33449  archiabllem2c  33455  fldext2rspun  34016  constrrtcc  34069  constrelextdg2  34081  constraddcl  34096  constrrecl  34103  constrresqrtcl  34111  2sqr3nconstr  34115  cos9thpiminplylem1  34116  cos9thpiminplylem2  34117  cos9thpiminplylem3  34118  cos9thpiminply  34122  cos9thpinconstrlem1  34123  cos9thpinconstrlem2  34124  cos9thpinconstr  34125  sqsscirc1  34242  dya2icoseg  34611  dya2iocucvr  34618  oddpwdc  34688  eulerpartlemgs2  34714  fibp1  34735  signslema  34893  itgexpif  34937  vtsprod  34970  hgt750lemd  34979  logdivsqrle  34981  subfacp1lem1  35569  subfacp1lem5  35574  dnibndlem10  36964  knoppcnlem10  36979  knoppndvlem2  36990  knoppndvlem7  36995  knoppndvlem9  36997  knoppndvlem10  36998  knoppndvlem16  37004  irrdifflemf  37856  qdiff  37858  itg2addnclem  38209  dvasin  38242  areacirclem1  38246  areacirclem3  38248  isbnd2  38321  lcmineqlem21  42705  3lexlogpow2ineq2  42715  dvrelog2b  42722  dvrelogpow2b  42724  aks4d1p1p4  42727  aks4d1p1p6  42729  aks4d1p1p7  42730  aks4d1p1p5  42731  aks4d1p9  42744  posbezout  42756  2np3bcnp1  42800  2ap1caineq  42801  oddnumth  42961  nicomachus  42962  sumcubes  42963  ef11d  42989  cxpi11d  42993  tan3rdpi  43002  readvrec2  43011  remul02  43055  remul01  43057  dffltz  43257  fltne  43267  flt4lem5e  43279  cu3addd  43303  rmspecsqrtnq  43524  rmxluc  43554  rmyluc2  43556  rmydbl  43558  jm2.18  43606  jm2.22  43613  jm2.25  43617  jm2.27c  43625  jm3.1lem2  43636  sqrtcval  44258  imo72b2lem0  44782  refsum2cnlem1  45648  oddfl  45888  xralrple2  45961  infleinflem2  45977  sumnnodd  46237  0ellimcdiv  46254  coseq0  46469  sinmulcos  46470  coskpi2  46471  sinaover2ne0  46473  cosknegpi  46474  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  itgsinexp  46560  stoweidlem1  46606  stoweidlem62  46667  wallispilem4  46673  wallispilem5  46674  wallispi  46675  wallispi2lem1  46676  wallispi2lem2  46677  wallispi2  46678  stirlinglem1  46679  stirlinglem3  46681  stirlinglem4  46682  stirlinglem5  46683  stirlinglem6  46684  stirlinglem7  46685  stirlinglem8  46686  stirlinglem10  46688  stirlinglem11  46689  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  dirker2re  46697  dirkerdenne0  46698  dirkerval2  46699  dirkerre  46700  dirkertrigeqlem1  46703  dirkertrigeqlem2  46704  dirkertrigeqlem3  46705  dirkertrigeq  46706  dirkeritg  46707  dirkercncflem1  46708  dirkercncflem2  46709  dirkercncflem4  46711  fourierdlem43  46755  fourierdlem44  46756  fourierdlem56  46767  fourierdlem57  46768  fourierdlem58  46769  fourierdlem62  46773  fourierdlem66  46777  fourierdlem68  46779  fourierdlem72  46783  fourierdlem76  46787  fourierdlem79  46790  fourierdlem80  46791  fourierdlem83  46794  fourierdlem95  46806  fourierdlem104  46815  fourierdlem112  46823  fouriercnp  46831  fourierswlem  46835  sge0ad2en  47036  hoicvrrex  47161  hoiqssbllem2  47228  sin3t  47496  cos3t  47497  sin5tlem1  47498  sin5tlem3  47500  sin5tlem4  47501  sin5t  47503  2tceilhalfelfzo1  47961  minusmodnep2tmod  47984  modmkpkne  47992  modm2nep1  47997  modm1nem2  48000  fmtnoodd  48173  sqrtpwpw2p  48178  fmtnorec2lem  48182  fmtnodvds  48184  goldbachthlem2  48186  fmtnoprmfac1lem  48204  fmtnoprmfac2  48207  fmtnofac1  48210  2pwp1prm  48229  mod42tp1mod8  48242  sfprmdvdsmersenne  48243  lighneallem2  48246  lighneallem4  48250  proththd  48254  nprmdvdsfacm1lem1  48260  ppivalnn4  48267  quad1  48273  requad01  48274  requad1  48275  requad2  48276  dfodd6  48290  dfeven4  48291  enege  48298  onego  48299  dfeven2  48302  oddflALTV  48316  opoeALTV  48336  opeoALTV  48337  nn0onn0exALTV  48352  nn0enn0exALTV  48353  nnennexALTV  48354  mogoldbblem  48373  perfectALTV  48376  fppr2odd  48384  sgoldbeven3prm  48436  gpg3nbgrvtx0  48729  gpg3kgrtriexlem2  48737  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  0nodd  48823  2nodd  48825  2zlidl  48893  2zrngamgm  48898  2zrngagrp  48902  2zrngmmgm  48905  2zrngnmlid  48908  nn0onn0ex  49187  nn0enn0ex  49188  nnennex  49189  nnpw2even  49193  fldivexpfllog2  49229  blenpw2m1  49243  nnpw2blen  49244  blennn0em1  49255  dig2nn1st  49269  dig2bits  49278  dignn0flhalflem1  49279  dignn0flhalflem2  49280  dignn0ehalf  49281  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  itcovalt2lem2lem2  49338  ackval2  49346  ackval3  49347  itschlc0yqe  49424  itsclc0yqsollem1  49426  itsclc0yqsol  49428  itsclc0xyqsolr  49433  itsclquadb  49440  2itscplem1  49442  2itscplem3  49444  itscnhlinecirc02plem1  49446