Theorem 2cnd 12259

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  2c2 12236

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 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244

This theorem is referenced by:  subhalfhalf  12411  cnm2m1cnm3  12430  xp1d2m1eqxm1d2  12431  zeo2  12616  ge2halflem1  13059  fzosplitprm1  13733  2tnp1ge0ge0  13788  flhalf  13789  2txmodxeq0  13893  mulbinom2  14185  binom3  14186  zesq  14188  expmulnbnd  14197  discr  14202  sqoddm1div8  14205  mulsubdivbinom2  14224  swrds2m  14903  amgm2  15332  bhmafibid1cn  15428  bhmafibid2cn  15429  iseraltlem2  15645  iseralt  15647  trirecip  15828  geo2sum  15838  bpolydiflem  16019  ege2le3  16055  tanval3  16101  sinhval  16121  tanhlt1  16127  sqrt2irrlem  16215  sqrt2irr  16216  even2n  16311  oddm1even  16312  oddp1even  16313  mod2eq1n2dvds  16316  ltoddhalfle  16330  m1exp1  16345  nn0enne  16346  flodddiv4  16384  flodddiv4t2lthalf  16387  bitsp1e  16401  bitsp1o  16402  bitsfzo  16404  bitsmod  16405  bitsinv1lem  16410  sadadd2lem2  16419  sadcaddlem  16426  bitsuz  16443  bitsshft  16444  prmdiv  16755  vfermltlALT  16773  iserodd  16806  4sqlem7  16915  4sqlem10  16918  4sqlem19  16934  prmgaplem7  17028  2expltfac  17063  smndex2dlinvh  18888  efgredlemg  19717  frgpnabllem1  19848  ablsimpgfindlem1  20084  metnrmlem3  24827  iihalf1cn  24899  iihalf2cn  24901  pcoass  24991  cphipval2  25208  csbren  25366  trirn  25367  minveclem2  25393  ovolunlem1a  25463  uniioombllem5  25554  uniioombl  25556  dyaddisjlem  25562  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  dvsincos  25948  lhop1  25981  cosargd  26572  dvcnsqrt  26708  root1id  26718  ssscongptld  26786  chordthmlem  26796  chordthmlem2  26797  chordthmlem4  26799  heron  26802  dcubic1  26809  mcubic  26811  cubic2  26812  quartlem4  26824  quart  26825  cosasin  26868  cosatan  26885  atantayl  26901  atantayl2  26902  atantayl3  26903  log2tlbnd  26909  cxp2limlem  26939  divsqrtsumlem  26943  lgamgulmlem2  26993  lgamgulmlem4  26995  lgamucov  27001  ftalem2  27037  basellem2  27045  basellem3  27046  basellem5  27048  basellem8  27051  logfaclbnd  27185  perfectlem2  27193  perfect  27194  bcp1ctr  27242  bposlem1  27247  bposlem2  27248  lgslem1  27260  lgsqrlem2  27310  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  gausslemma2dlem4  27332  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem1  27347  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1b  27355  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3d1  27366  2sq2  27396  addsq2nreurex  27407  chebbnd1lem3  27434  chto1ub  27439  dchrisumlem2  27453  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2  27481  logdivsum  27496  mulog2sumlem2  27498  vmalogdivsum2  27501  log2sumbnd  27507  selberglem2  27509  chpdifbndlem1  27516  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  selberg4r  27533  selberg34r  27534  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem2  27554  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemr  27565  pntlemk  27569  pntlemo  27570  ostth2lem1  27581  finsumvtxdg2ssteplem4  29617  upgrwlkdvdelem  29804  wwlksnextwrd  29965  wwlksnextinj  29967  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a4  30067  clwlkclwwlklem3  30071  clwwlkext2edg  30126  clwwlknonex2lem1  30177  clwwlknonex2lem2  30178  2clwwlk2clwwlk  30420  numclwwlk1lem2foalem  30421  numclwwlk1lem2fo  30428  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwwlk2  30451  ex-ind-dvds  30531  nrt2irr  30543  binom2subadd  32814  quad3d  32822  2exple2exp  32918  wrdt2ind  33013  archirngz  33250  archiabllem2c  33256  fldext2rspun  33826  constrrtcc  33879  constrelextdg2  33891  constraddcl  33906  constrrecl  33913  constrresqrtcl  33921  2sqr3nconstr  33925  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  cos9thpinconstr  33935  sqsscirc1  34052  dya2icoseg  34421  dya2iocucvr  34428  oddpwdc  34498  eulerpartlemgs2  34524  fibp1  34545  signslema  34706  itgexpif  34750  vtsprod  34783  hgt750lemd  34792  logdivsqrle  34794  subfacp1lem1  35361  subfacp1lem5  35366  dnibndlem10  36747  knoppcnlem10  36762  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem9  36780  knoppndvlem10  36781  knoppndvlem16  36787  irrdifflemf  37639  qdiff  37641  itg2addnclem  37992  dvasin  38025  areacirclem1  38029  areacirclem3  38031  isbnd2  38104  lcmineqlem21  42488  3lexlogpow2ineq2  42498  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p9  42527  posbezout  42539  2np3bcnp1  42583  2ap1caineq  42584  oddnumth  42743  nicomachus  42744  sumcubes  42745  ef11d  42771  cxpi11d  42775  tan3rdpi  42784  readvrec2  42793  remul02  42837  remul01  42839  dffltz  43067  fltne  43077  flt4lem5e  43089  cu3addd  43113  rmspecsqrtnq  43334  rmxluc  43364  rmyluc2  43366  rmydbl  43368  jm2.18  43416  jm2.22  43423  jm2.25  43427  jm2.27c  43435  jm3.1lem2  43446  sqrtcval  44068  imo72b2lem0  44592  refsum2cnlem1  45468  oddfl  45711  xralrple2  45784  infleinflem2  45800  sumnnodd  46060  0ellimcdiv  46077  coseq0  46292  sinmulcos  46293  coskpi2  46294  sinaover2ne0  46296  cosknegpi  46297  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  itgsinexp  46383  stoweidlem1  46429  stoweidlem62  46490  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  dirker2re  46520  dirkerdenne0  46521  dirkerval2  46522  dirkerre  46523  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem43  46578  fourierdlem44  46579  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem66  46600  fourierdlem68  46602  fourierdlem72  46606  fourierdlem76  46610  fourierdlem79  46613  fourierdlem80  46614  fourierdlem83  46617  fourierdlem95  46629  fourierdlem104  46638  fourierdlem112  46646  fouriercnp  46654  fourierswlem  46658  sge0ad2en  46859  hoicvrrex  46984  hoiqssbllem2  47051  sin3t  47319  cos3t  47320  sin5tlem1  47321  sin5tlem3  47323  sin5tlem4  47324  sin5t  47326  2tceilhalfelfzo1  47784  minusmodnep2tmod  47807  modmkpkne  47815  modm2nep1  47820  modm1nem2  47823  fmtnoodd  47996  sqrtpwpw2p  48001  fmtnorec2lem  48005  fmtnodvds  48007  goldbachthlem2  48009  fmtnoprmfac1lem  48027  fmtnoprmfac2  48030  fmtnofac1  48033  2pwp1prm  48052  mod42tp1mod8  48065  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem4  48073  proththd  48077  nprmdvdsfacm1lem1  48083  ppivalnn4  48090  quad1  48096  requad01  48097  requad1  48098  requad2  48099  dfodd6  48113  dfeven4  48114  enege  48121  onego  48122  dfeven2  48125  oddflALTV  48139  opoeALTV  48159  opeoALTV  48160  nn0onn0exALTV  48175  nn0enn0exALTV  48176  nnennexALTV  48177  mogoldbblem  48196  perfectALTV  48199  fppr2odd  48207  sgoldbeven3prm  48259  gpg3nbgrvtx0  48552  gpg3kgrtriexlem2  48560  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  0nodd  48646  2nodd  48648  2zlidl  48716  2zrngamgm  48721  2zrngagrp  48725  2zrngmmgm  48728  2zrngnmlid  48731  nn0onn0ex  48999  nn0enn0ex  49000  nnennex  49001  nnpw2even  49005  fldivexpfllog2  49041  blenpw2m1  49055  nnpw2blen  49056  blennn0em1  49067  dig2nn1st  49081  dig2bits  49090  dignn0flhalflem1  49091  dignn0flhalflem2  49092  dignn0ehalf  49093  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  itcovalt2lem2lem2  49150  ackval2  49158  ackval3  49159  itschlc0yqe  49236  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itsclc0xyqsolr  49245  itsclquadb  49252  2itscplem1  49254  2itscplem3  49256  itscnhlinecirc02plem1  49258