Theorem 2cnd 12414

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11191  2c2 12390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addcl 11253

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12398

This theorem is used by:  subhalfhalf  12573  cnm2m1cnm3  12592  xp1d2m1eqxm1d2  12593  zeo2  12779  ge2halflem1  13230  fzosplitprm1  13906  2tnp1ge0ge0  13962  flhalf  13963  2txmodxeq0  14067  mulbinom2  14360  binom3  14361  zesq  14363  expmulnbnd  14372  discr  14377  sqoddm1div8  14380  mulsubdivbinom2  14399  swrds2m  15085  amgm2  15530  bhmafibid1cn  15626  bhmafibid2cn  15627  iseraltlem2  15843  iseralt  15845  trirecip  16025  geo2sum  16035  bpolydiflem  16213  bpoly4  16218  ege2le3  16249  tanval3  16295  sinhval  16315  tanhlt1  16321  sqrt2irrlem  16409  sqrt2irr  16410  even2n  16505  oddm1even  16506  oddp1even  16507  mod2eq1n2dvds  16510  ltoddhalfle  16524  m1exp1  16539  nn0enne  16540  flodddiv4  16578  flodddiv4t2lthalf  16581  bitsp1e  16595  bitsp1o  16596  bitsfzo  16598  bitsmod  16599  bitsinv1lem  16604  sadadd2lem2  16613  sadcaddlem  16620  bitsuz  16637  bitsshft  16638  prmdiv  16955  vfermltlALT  16973  iserodd  17006  4sqlem7  17115  4sqlem10  17118  4sqlem19  17134  prmgaplem7  17228  2expltfac  17263  smndex2dlinvh  19109  efgredlemg  19949  frgpnabllem1  20080  ablsimpgfindlem1  20316  metnrmlem3  25174  iihalf1cn  25246  iihalf2cn  25248  pcoass  25338  cphipval2  25555  csbren  25713  trirn  25714  minveclem2  25740  ovolunlem1a  25810  uniioombllem5  25901  uniioombl  25903  dyaddisjlem  25909  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  dvsincos  26294  lhop1  26327  cosargd  26929  dvcnsqrt  27065  root1id  27075  ssscongptld  27143  chordthmlem  27153  chordthmlem2  27154  chordthmlem4  27156  heron  27159  dcubic1  27166  mcubic  27168  cubic2  27169  quartlem4  27181  quart  27182  cosasin  27225  cosatan  27242  atantayl  27258  atantayl2  27259  atantayl3  27260  log2tlbnd  27266  cxp2limlem  27296  divsqrtsumlem  27300  lgamgulmlem2  27350  lgamgulmlem4  27352  lgamucov  27358  ftalem2  27394  basellem2  27402  basellem3  27403  basellem5  27405  basellem8  27408  logfaclbnd  27542  perfectlem2  27550  perfect  27551  bcp1ctr  27599  bposlem1  27604  bposlem2  27605  lgslem1  27617  lgsqrlem2  27667  gausslemma2dlem1a  27685  gausslemma2dlem3  27688  gausslemma2dlem4  27689  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgsquadlem1  27700  lgsquadlem2  27701  lgsquad2lem1  27704  2lgslem1a1  27709  2lgslem1a2  27710  2lgslem1b  27712  2lgslem1c  27713  2lgslem3a1  27720  2lgslem3d1  27723  2sq2  27753  addsq2nreurex  27764  chebbnd1lem3  27791  chto1ub  27796  dchrisumlem2  27810  dchrisum0flblem2  27829  dchrisum0fno1  27831  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2  27838  logdivsum  27853  mulog2sumlem2  27855  vmalogdivsum2  27858  log2sumbnd  27864  selberglem2  27866  chpdifbndlem1  27873  selberg3lem1  27877  selberg3  27879  selberg4lem1  27880  selberg4  27881  selberg4r  27890  selberg34r  27891  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntpbnd1a  27905  pntpbnd2  27907  pntibndlem2  27911  pntlemb  27917  pntlemg  27918  pntlemh  27919  pntlemr  27922  pntlemk  27926  pntlemo  27927  ostth2lem1  27938  fltne  27968  flt4lem5e  27979  finsumvtxdg2ssteplem4  30122  upgrwlkdvdelem  30315  wwlksnextwrd  30479  wwlksnextinj  30481  clwlkclwwlklem2a1  30576  clwlkclwwlklem2a4  30581  clwlkclwwlklem3  30585  clwwlkext2edg  30640  clwwlknonex2lem1  30691  clwwlknonex2lem2  30692  2clwwlk2clwwlk  30944  numclwwlk1lem2foalem  30945  numclwwlk1lem2fo  30952  numclwwlk2lem1  30970  numclwlk2lem2f  30971  numclwwlk2  30975  ex-ind-dvds  31055  nrt2irr  31067  binom2subadd  33326  quad3d  33334  2exple2exp  33418  wrdt2ind  33509  archirngz  33743  archiabllem2c  33749  fldext2rspun  34307  constrrtcc  34360  constrelextdg2  34372  constraddcl  34387  constrrecl  34394  constrresqrtcl  34402  2sqr3nconstr  34406  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem3  34409  cos9thpiminply  34413  cos9thpinconstrlem1  34414  cos9thpinconstrlem2  34415  cos9thpinconstr  34416  sqsscirc1  34533  dya2icoseg  34902  dya2iocucvr  34909  oddpwdc  34979  eulerpartlemgs2  35005  fibp1  35026  signslema  35184  itgexpif  35228  vtsprod  35261  hgt750lemd  35270  logdivsqrle  35272  subfacp1lem1  35923  subfacp1lem5  35928  dnibndlem10  37333  knoppcnlem10  37348  knoppndvlem2  37359  knoppndvlem7  37364  knoppndvlem9  37366  knoppndvlem10  37367  knoppndvlem16  37373  irrdifflemf  38226  qdiff  38228  itg2addnclem  38569  dvasin  38602  areacirclem1  38606  areacirclem3  38608  isbnd2  38697  lcmineqlem21  43079  3lexlogpow2ineq2  43089  dvrelog2b  43096  dvrelogpow2b  43098  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p9  43118  posbezout  43130  2np3bcnp1  43174  2ap1caineq  43175  oddnumth  43348  nicomachus  43349  sumcubes  43350  ef11d  43370  cxpi11d  43374  tan3rdpi  43383  readvrec2  43392  remul02  43436  remul01  43438  dffltz  43650  cu3addd  43671  rmspecsqrtnq  43892  rmxluc  43922  rmyluc2  43924  rmydbl  43926  jm2.18  43974  jm2.22  43981  jm2.25  43985  jm2.27c  43993  jm3.1lem2  44004  sqrtcval  44626  imo72b2lem0  45150  refsum2cnlem1  46023  oddfl  46263  xralrple2  46335  infleinflem2  46351  sumnnodd  46611  0ellimcdiv  46628  coseq0  46843  sinmulcos  46844  coskpi2  46845  sinaover2ne0  46847  cosknegpi  46848  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  itgsinexp  46934  stoweidlem1  46980  stoweidlem62  47041  wallispilem4  47047  wallispilem5  47048  wallispi  47049  wallispi2lem1  47050  wallispi2lem2  47051  wallispi2  47052  stirlinglem1  47053  stirlinglem3  47055  stirlinglem4  47056  stirlinglem5  47057  stirlinglem6  47058  stirlinglem7  47059  stirlinglem8  47060  stirlinglem10  47062  stirlinglem11  47063  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  dirker2re  47071  dirkerdenne0  47072  dirkerval2  47073  dirkerre  47074  dirkertrigeqlem1  47077  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkeritg  47081  dirkercncflem1  47082  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem43  47129  fourierdlem44  47130  fourierdlem56  47141  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fourierdlem66  47151  fourierdlem68  47153  fourierdlem72  47157  fourierdlem76  47161  fourierdlem79  47164  fourierdlem80  47165  fourierdlem83  47168  fourierdlem95  47180  fourierdlem104  47189  fourierdlem112  47197  fouriercnp  47205  fourierswlem  47209  sge0ad2en  47410  hoicvrrex  47535  hoiqssbllem2  47602  sin3t  47886  cos3t  47887  sin5tlem1  47888  sin5tlem3  47890  sin5tlem4  47891  sin5t  47893  2tceilhalfelfzo1  48375  minusmodnep2tmod  48398  modmkpkne  48406  modm2nep1  48411  modm1nem2  48414  fmtnoodd  48587  sqrtpwpw2p  48592  fmtnorec2lem  48596  fmtnodvds  48598  goldbachthlem2  48600  fmtnoprmfac1lem  48618  fmtnoprmfac2  48621  fmtnofac1  48624  2pwp1prm  48643  mod42tp1mod8  48656  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem4  48664  proththd  48668  nprmdvdsfacm1lem1  48674  ppivalnn4  48681  quad1  48687  requad01  48688  requad1  48689  requad2  48690  dfodd6  48704  dfeven4  48705  enege  48712  onego  48713  dfeven2  48716  oddflALTV  48730  opoeALTV  48750  opeoALTV  48751  nn0onn0exALTV  48766  nn0enn0exALTV  48767  nnennexALTV  48768  mogoldbblem  48787  perfectALTV  48790  fppr2odd  48798  sgoldbeven3prm  48850  gpg3nbgrvtx0  49143  gpg3kgrtriexlem2  49151  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  0nodd  49236  2nodd  49238  2zlidl  49306  2zrngamgm  49311  2zrngagrp  49315  2zrngmmgm  49318  2zrngnmlid  49321  nn0onn0ex  49604  nn0enn0ex  49605  nnennex  49606  nnpw2even  49610  fldivexpfllog2  49646  blenpw2m1  49660  nnpw2blen  49661  blennn0em1  49672  dig2nn1st  49686  dig2bits  49695  dignn0flhalflem1  49696  dignn0flhalflem2  49697  dignn0ehalf  49698  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  itcovalt2lem2lem2  49755  ackval2  49763  ackval3  49764  itschlc0yqe  49841  itsclc0yqsollem1  49843  itsclc0yqsol  49845  itsclc0xyqsolr  49850  itsclquadb  49857  2itscplem1  49859  2itscplem3  49861  itscnhlinecirc02plem1  49863