Theorem 2cnd 12325

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ℂcc 11104  2c2 12301

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11164  ax-addcl 11166

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837  df-2 12309

This theorem is used by:  subhalfhalf  12484  cnm2m1cnm3  12503  xp1d2m1eqxm1d2  12504  zeo2  12689  ge2halflem1  13139  fzosplitprm1  13814  2tnp1ge0ge0  13869  flhalf  13870  2txmodxeq0  13974  mulbinom2  14266  binom3  14267  zesq  14269  expmulnbnd  14278  discr  14283  sqoddm1div8  14286  mulsubdivbinom2  14305  swrds2m  14985  amgm2  15428  bhmafibid1cn  15524  bhmafibid2cn  15525  iseraltlem2  15741  iseralt  15743  trirecip  15924  geo2sum  15934  bpolydiflem  16114  bpoly4  16119  ege2le3  16150  tanval3  16196  sinhval  16216  tanhlt1  16222  sqrt2irrlem  16310  sqrt2irr  16311  even2n  16406  oddm1even  16407  oddp1even  16408  mod2eq1n2dvds  16411  ltoddhalfle  16425  m1exp1  16440  nn0enne  16441  flodddiv4  16479  flodddiv4t2lthalf  16482  bitsp1e  16496  bitsp1o  16497  bitsfzo  16499  bitsmod  16500  bitsinv1lem  16505  sadadd2lem2  16514  sadcaddlem  16521  bitsuz  16538  bitsshft  16539  prmdiv  16850  vfermltlALT  16868  iserodd  16901  4sqlem7  17010  4sqlem10  17013  4sqlem19  17029  prmgaplem7  17123  2expltfac  17158  smndex2dlinvh  18985  efgredlemg  19818  frgpnabllem1  19949  ablsimpgfindlem1  20185  metnrmlem3  25030  iihalf1cn  25102  iihalf2cn  25104  pcoass  25194  cphipval2  25411  csbren  25569  trirn  25570  minveclem2  25596  ovolunlem1a  25666  uniioombllem5  25757  uniioombl  25759  dyaddisjlem  25765  mbfi1fseqlem5  25889  mbfi1fseqlem6  25890  dvsincos  26151  lhop1  26184  cosargd  26784  dvcnsqrt  26920  root1id  26930  ssscongptld  26998  chordthmlem  27008  chordthmlem2  27009  chordthmlem4  27011  heron  27014  dcubic1  27021  mcubic  27023  cubic2  27024  quartlem4  27036  quart  27037  cosasin  27080  cosatan  27097  atantayl  27113  atantayl2  27114  atantayl3  27115  log2tlbnd  27121  cxp2limlem  27151  divsqrtsumlem  27155  lgamgulmlem2  27205  lgamgulmlem4  27207  lgamucov  27213  ftalem2  27249  basellem2  27257  basellem3  27258  basellem5  27260  basellem8  27263  logfaclbnd  27397  perfectlem2  27405  perfect  27406  bcp1ctr  27454  bposlem1  27459  bposlem2  27460  lgslem1  27472  lgsqrlem2  27522  gausslemma2dlem1a  27540  gausslemma2dlem3  27543  gausslemma2dlem4  27544  lgseisenlem1  27550  lgseisenlem2  27551  lgseisenlem3  27552  lgseisenlem4  27553  lgsquadlem1  27555  lgsquadlem2  27556  lgsquad2lem1  27559  2lgslem1a1  27564  2lgslem1a2  27565  2lgslem1b  27567  2lgslem1c  27568  2lgslem3a1  27575  2lgslem3d1  27578  2sq2  27608  addsq2nreurex  27619  chebbnd1lem3  27646  chto1ub  27651  dchrisumlem2  27665  dchrisum0flblem2  27684  dchrisum0fno1  27686  dchrisum0lem1b  27690  dchrisum0lem1  27691  dchrisum0lem2  27693  logdivsum  27708  mulog2sumlem2  27710  vmalogdivsum2  27713  log2sumbnd  27719  selberglem2  27721  chpdifbndlem1  27728  selberg3lem1  27732  selberg3  27734  selberg4lem1  27735  selberg4  27736  selberg4r  27745  selberg34r  27746  pntrlog2bndlem3  27754  pntrlog2bndlem4  27755  pntrlog2bndlem5  27756  pntrlog2bndlem6  27758  pntpbnd1a  27760  pntpbnd2  27762  pntibndlem2  27766  pntlemb  27772  pntlemg  27773  pntlemh  27774  pntlemr  27777  pntlemk  27781  pntlemo  27782  ostth2lem1  27793  finsumvtxdg2ssteplem4  29909  upgrwlkdvdelem  30096  wwlksnextwrd  30257  wwlksnextinj  30259  clwlkclwwlklem2a1  30354  clwlkclwwlklem2a4  30359  clwlkclwwlklem3  30363  clwwlkext2edg  30418  clwwlknonex2lem1  30469  clwwlknonex2lem2  30470  2clwwlk2clwwlk  30712  numclwwlk1lem2foalem  30713  numclwwlk1lem2fo  30720  numclwwlk2lem1  30738  numclwlk2lem2f  30739  numclwwlk2  30743  ex-ind-dvds  30823  nrt2irr  30835  binom2subadd  33097  quad3d  33105  2exple2exp  33189  wrdt2ind  33282  archirngz  33518  archiabllem2c  33524  fldext2rspun  34081  constrrtcc  34134  constrelextdg2  34146  constraddcl  34161  constrrecl  34168  constrresqrtcl  34176  2sqr3nconstr  34180  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  cos9thpiminplylem3  34183  cos9thpiminply  34187  cos9thpinconstrlem1  34188  cos9thpinconstrlem2  34189  cos9thpinconstr  34190  sqsscirc1  34307  dya2icoseg  34676  dya2iocucvr  34683  oddpwdc  34753  eulerpartlemgs2  34779  fibp1  34800  signslema  34958  itgexpif  35002  vtsprod  35035  hgt750lemd  35044  logdivsqrle  35046  subfacp1lem1  35679  subfacp1lem5  35684  dnibndlem10  37104  knoppcnlem10  37119  knoppndvlem2  37130  knoppndvlem7  37135  knoppndvlem9  37137  knoppndvlem10  37138  knoppndvlem16  37144  irrdifflemf  37997  qdiff  37999  itg2addnclem  38350  dvasin  38383  areacirclem1  38387  areacirclem3  38389  isbnd2  38462  lcmineqlem21  42844  3lexlogpow2ineq2  42854  dvrelog2b  42861  dvrelogpow2b  42863  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p9  42883  posbezout  42895  2np3bcnp1  42939  2ap1caineq  42940  oddnumth  43100  nicomachus  43101  sumcubes  43102  ef11d  43128  cxpi11d  43132  tan3rdpi  43141  readvrec2  43150  remul02  43194  remul01  43196  dffltz  43394  fltne  43404  flt4lem5e  43416  cu3addd  43440  rmspecsqrtnq  43661  rmxluc  43691  rmyluc2  43693  rmydbl  43695  jm2.18  43743  jm2.22  43750  jm2.25  43754  jm2.27c  43762  jm3.1lem2  43773  sqrtcval  44395  imo72b2lem0  44919  refsum2cnlem1  45785  oddfl  46025  xralrple2  46098  infleinflem2  46114  sumnnodd  46374  0ellimcdiv  46391  coseq0  46606  sinmulcos  46607  coskpi2  46608  sinaover2ne0  46610  cosknegpi  46611  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  itgsinexp  46697  stoweidlem1  46743  stoweidlem62  46804  wallispilem4  46810  wallispilem5  46811  wallispi  46812  wallispi2lem1  46813  wallispi2lem2  46814  wallispi2  46815  stirlinglem1  46816  stirlinglem3  46818  stirlinglem4  46819  stirlinglem5  46820  stirlinglem6  46821  stirlinglem7  46822  stirlinglem8  46823  stirlinglem10  46825  stirlinglem11  46826  stirlinglem13  46828  stirlinglem14  46829  stirlinglem15  46830  dirker2re  46834  dirkerdenne0  46835  dirkerval2  46836  dirkerre  46837  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkeritg  46844  dirkercncflem1  46845  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem43  46892  fourierdlem44  46893  fourierdlem56  46904  fourierdlem57  46905  fourierdlem58  46906  fourierdlem62  46910  fourierdlem66  46914  fourierdlem68  46916  fourierdlem72  46920  fourierdlem76  46924  fourierdlem79  46927  fourierdlem80  46928  fourierdlem83  46931  fourierdlem95  46943  fourierdlem104  46952  fourierdlem112  46960  fouriercnp  46968  fourierswlem  46972  sge0ad2en  47173  hoicvrrex  47298  hoiqssbllem2  47365  sin3t  47636  cos3t  47637  sin5tlem1  47638  sin5tlem3  47640  sin5tlem4  47641  sin5t  47643  2tceilhalfelfzo1  48101  minusmodnep2tmod  48124  modmkpkne  48132  modm2nep1  48137  modm1nem2  48140  fmtnoodd  48313  sqrtpwpw2p  48318  fmtnorec2lem  48322  fmtnodvds  48324  goldbachthlem2  48326  fmtnoprmfac1lem  48344  fmtnoprmfac2  48347  fmtnofac1  48350  2pwp1prm  48369  mod42tp1mod8  48382  sfprmdvdsmersenne  48383  lighneallem2  48386  lighneallem4  48390  proththd  48394  nprmdvdsfacm1lem1  48400  ppivalnn4  48407  quad1  48413  requad01  48414  requad1  48415  requad2  48416  dfodd6  48430  dfeven4  48431  enege  48438  onego  48439  dfeven2  48442  oddflALTV  48456  opoeALTV  48476  opeoALTV  48477  nn0onn0exALTV  48492  nn0enn0exALTV  48493  nnennexALTV  48494  mogoldbblem  48513  perfectALTV  48516  fppr2odd  48524  sgoldbeven3prm  48576  gpg3nbgrvtx0  48869  gpg3kgrtriexlem2  48877  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  0nodd  48963  2nodd  48965  2zlidl  49033  2zrngamgm  49038  2zrngagrp  49042  2zrngmmgm  49045  2zrngnmlid  49048  nn0onn0ex  49331  nn0enn0ex  49332  nnennex  49333  nnpw2even  49337  fldivexpfllog2  49373  blenpw2m1  49387  nnpw2blen  49388  blennn0em1  49399  dig2nn1st  49413  dig2bits  49422  dignn0flhalflem1  49423  dignn0flhalflem2  49424  dignn0ehalf  49425  nn0sumshdiglemA  49427  nn0sumshdiglemB  49428  itcovalt2lem2lem2  49482  ackval2  49490  ackval3  49491  itschlc0yqe  49568  itsclc0yqsollem1  49570  itsclc0yqsol  49572  itsclc0xyqsolr  49577  itsclquadb  49584  2itscplem1  49586  2itscplem3  49588  itscnhlinecirc02plem1  49590