Theorem 2cnd 12461

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11237  2c2 12437

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12445

This theorem is used by:  subhalfhalf  12620  cnm2m1cnm3  12639  xp1d2m1eqxm1d2  12640  zeo2  12826  ge2halflem1  13277  fzosplitprm1  13953  2tnp1ge0ge0  14009  flhalf  14010  2txmodxeq0  14114  mulbinom2  14408  binom3  14409  zesq  14411  expmulnbnd  14420  discr  14425  sqoddm1div8  14428  mulsubdivbinom2  14447  swrds2m  15135  amgm2  15581  bhmafibid1cn  15677  bhmafibid2cn  15678  iseraltlem2  15894  iseralt  15896  trirecip  16076  geo2sum  16086  bpolydiflem  16264  bpoly4  16269  ege2le3  16300  tanval3  16346  sinhval  16366  tanhlt1  16372  sqrt2irrlem  16460  sqrt2irr  16461  even2n  16556  oddm1even  16557  oddp1even  16558  mod2eq1n2dvds  16561  ltoddhalfle  16575  m1exp1  16590  nn0enne  16591  flodddiv4  16629  flodddiv4t2lthalf  16632  bitsp1e  16646  bitsp1o  16647  bitsfzo  16649  bitsmod  16650  bitsinv1lem  16655  sadadd2lem2  16664  sadcaddlem  16671  bitsuz  16688  bitsshft  16689  prmdiv  17006  vfermltlALT  17024  iserodd  17057  4sqlem7  17166  4sqlem10  17169  4sqlem19  17185  prmgaplem7  17279  2expltfac  17314  smndex2dlinvh  19166  efgredlemg  20007  frgpnabllem1  20138  ablsimpgfindlem1  20374  metnrmlem3  25236  iihalf1cn  25308  iihalf2cn  25310  pcoass  25400  cphipval2  25617  csbren  25775  trirn  25776  minveclem2  25802  ovolunlem1a  25872  uniioombllem5  25963  uniioombl  25965  dyaddisjlem  25971  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  dvsincos  26356  lhop1  26389  cosargd  26993  dvcnsqrt  27129  root1id  27139  ssscongptld  27207  chordthmlem  27217  chordthmlem2  27218  chordthmlem4  27220  heron  27223  dcubic1  27230  mcubic  27232  cubic2  27233  quartlem4  27245  quart  27246  cosasin  27289  cosatan  27306  atantayl  27322  atantayl2  27323  atantayl3  27324  log2tlbnd  27330  cxp2limlem  27360  divsqrtsumlem  27364  lgamgulmlem2  27414  lgamgulmlem4  27416  lgamucov  27422  ftalem2  27458  basellem2  27466  basellem3  27467  basellem5  27469  basellem8  27472  logfaclbnd  27606  perfectlem2  27614  perfect  27615  bcp1ctr  27663  bposlem1  27668  bposlem2  27669  lgslem1  27681  lgsqrlem2  27731  gausslemma2dlem1a  27749  gausslemma2dlem3  27752  gausslemma2dlem4  27753  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgsquadlem1  27764  lgsquadlem2  27765  lgsquad2lem1  27768  2lgslem1a1  27773  2lgslem1a2  27774  2lgslem1b  27776  2lgslem1c  27777  2lgslem3a1  27784  2lgslem3d1  27787  2sq2  27817  addsq2nreurex  27828  chebbnd1lem3  27855  chto1ub  27860  dchrisumlem2  27874  dchrisum0flblem2  27893  dchrisum0fno1  27895  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2  27902  logdivsum  27917  mulog2sumlem2  27919  vmalogdivsum2  27922  log2sumbnd  27928  selberglem2  27930  chpdifbndlem1  27937  selberg3lem1  27941  selberg3  27943  selberg4lem1  27944  selberg4  27945  selberg4r  27954  selberg34r  27955  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntpbnd1a  27969  pntpbnd2  27971  pntibndlem2  27975  pntlemb  27981  pntlemg  27982  pntlemh  27983  pntlemr  27986  pntlemk  27990  pntlemo  27991  ostth2lem1  28002  fltne  28032  flt4lem5e  28043  finsumvtxdg2ssteplem4  30186  upgrwlkdvdelem  30379  wwlksnextwrd  30543  wwlksnextinj  30545  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a4  30645  clwlkclwwlklem3  30649  clwwlkext2edg  30704  clwwlknonex2lem1  30755  clwwlknonex2lem2  30756  2clwwlk2clwwlk  31008  numclwwlk1lem2foalem  31009  numclwwlk1lem2fo  31016  numclwwlk2lem1  31034  numclwlk2lem2f  31035  numclwwlk2  31039  ex-ind-dvds  31119  nrt2irr  31131  binom2subadd  33429  quad3d  33437  2exple2exp  33521  wrdt2ind  33612  archirngz  33849  archiabllem2c  33855  fldext2rspun  34425  constrrtcc  34478  constrelextdg2  34490  constraddcl  34505  constrrecl  34512  constrresqrtcl  34520  2sqr3nconstr  34524  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cos9thpinconstr  34534  sqsscirc1  34651  dya2icoseg  35020  dya2iocucvr  35027  omssubadd  35043  oddpwdc  35097  eulerpartlemgs2  35123  fibp1  35144  signslema  35302  itgexpif  35346  vtsprod  35379  hgt750lemd  35388  logdivsqrle  35390  subfacp1lem1  36152  subfacp1lem5  36157  dnibndlem10  37568  knoppcnlem10  37583  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem9  37601  knoppndvlem10  37602  knoppndvlem16  37608  irrdifflemf  38514  qdiff  38516  itg2addnclem  38857  dvasin  38890  areacirclem1  38894  areacirclem3  38896  isbnd2  38983  lcmineqlem21  43365  3lexlogpow2ineq2  43375  dvrelog2b  43382  dvrelogpow2b  43384  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p9  43404  posbezout  43416  2np3bcnp1  43460  2ap1caineq  43461  oddnumth  43634  nicomachus  43635  sumcubes  43636  ef11d  43656  cxpi11d  43660  tan3rdpi  43669  readvrec2  43678  remul02  43722  remul01  43724  dffltz  43936  cu3addd  43957  rmspecsqrtnq  44179  rmxluc  44209  rmyluc2  44211  rmydbl  44213  jm2.18  44261  jm2.22  44268  jm2.25  44272  jm2.27c  44280  jm3.1lem2  44291  sqrtcval  44902  imo72b2lem0  45426  refsum2cnlem1  46328  oddfl  46567  xralrple2  46639  infleinflem2  46655  sumnnodd  46915  0ellimcdiv  46932  coseq0  47147  sinmulcos  47148  coskpi2  47149  sinaover2ne0  47151  cosknegpi  47152  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  itgsinexp  47238  stoweidlem1  47284  stoweidlem62  47345  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem5  47361  stirlinglem6  47362  stirlinglem7  47363  stirlinglem8  47364  stirlinglem10  47366  stirlinglem11  47367  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  dirker2re  47375  dirkerdenne0  47376  dirkerval2  47377  dirkerre  47378  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkertrigeq  47384  dirkeritg  47385  dirkercncflem1  47386  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem43  47433  fourierdlem44  47434  fourierdlem56  47445  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fourierdlem66  47455  fourierdlem68  47457  fourierdlem72  47461  fourierdlem76  47465  fourierdlem79  47468  fourierdlem80  47469  fourierdlem83  47472  fourierdlem95  47484  fourierdlem104  47493  fourierdlem112  47501  fouriercnp  47509  fourierswlem  47513  sge0ad2en  47714  hoicvrrex  47839  hoiqssbllem2  47906  sin3t  48190  cos3t  48191  sin5tlem1  48192  sin5tlem3  48194  sin5tlem4  48195  sin5t  48197  2tceilhalfelfzo1  48679  minusmodnep2tmod  48702  modmkpkne  48710  modm2nep1  48715  modm1nem2  48718  fmtnoodd  48891  sqrtpwpw2p  48896  fmtnorec2lem  48900  fmtnodvds  48902  goldbachthlem2  48904  fmtnoprmfac1lem  48922  fmtnoprmfac2  48925  fmtnofac1  48928  2pwp1prm  48947  mod42tp1mod8  48960  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem4  48968  proththd  48972  nprmdvdsfacm1lem1  48978  ppivalnn4  48985  quad1  48991  requad01  48992  requad1  48993  requad2  48994  dfodd6  49008  dfeven4  49009  enege  49016  onego  49017  dfeven2  49020  oddflALTV  49034  opoeALTV  49054  opeoALTV  49055  nn0onn0exALTV  49070  nn0enn0exALTV  49071  nnennexALTV  49072  mogoldbblem  49091  perfectALTV  49094  fppr2odd  49102  sgoldbeven3prm  49154  gpg3nbgrvtx0  49447  gpg3kgrtriexlem2  49455  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  0nodd  49540  2nodd  49542  2zlidl  49610  2zrngamgm  49615  2zrngagrp  49619  2zrngmmgm  49622  2zrngnmlid  49625  bruval3  49748  nn0onn0ex  49966  nn0enn0ex  49967  nnennex  49968  nnpw2even  49972  fldivexpfllog2  50008  blenpw2m1  50022  nnpw2blen  50023  blennn0em1  50034  dig2nn1st  50048  dig2bits  50057  dignn0flhalflem1  50058  dignn0flhalflem2  50059  dignn0ehalf  50060  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  itcovalt2lem2lem2  50117  ackval2  50125  ackval3  50126  itschlc0yqe  50203  itsclc0yqsollem1  50205  itsclc0yqsol  50207  itsclc0xyqsolr  50212  itsclquadb  50219  2itscplem1  50221  2itscplem3  50223  itscnhlinecirc02plem1  50225