Theorem 2cnd 12343

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

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

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 2732  ax-1cn 11182  ax-addcl 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12327

This theorem is used by:  subhalfhalf  12502  cnm2m1cnm3  12521  xp1d2m1eqxm1d2  12522  zeo2  12708  ge2halflem1  13159  fzosplitprm1  13834  2tnp1ge0ge0  13890  flhalf  13891  2txmodxeq0  13995  mulbinom2  14287  binom3  14288  zesq  14290  expmulnbnd  14299  discr  14304  sqoddm1div8  14307  mulsubdivbinom2  14326  swrds2m  15012  amgm2  15457  bhmafibid1cn  15553  bhmafibid2cn  15554  iseraltlem2  15770  iseralt  15772  trirecip  15952  geo2sum  15962  bpolydiflem  16140  bpoly4  16145  ege2le3  16176  tanval3  16222  sinhval  16242  tanhlt1  16248  sqrt2irrlem  16336  sqrt2irr  16337  even2n  16432  oddm1even  16433  oddp1even  16434  mod2eq1n2dvds  16437  ltoddhalfle  16451  m1exp1  16466  nn0enne  16467  flodddiv4  16505  flodddiv4t2lthalf  16508  bitsp1e  16522  bitsp1o  16523  bitsfzo  16525  bitsmod  16526  bitsinv1lem  16531  sadadd2lem2  16540  sadcaddlem  16547  bitsuz  16564  bitsshft  16565  prmdiv  16876  vfermltlALT  16894  iserodd  16927  4sqlem7  17036  4sqlem10  17039  4sqlem19  17055  prmgaplem7  17149  2expltfac  17184  smndex2dlinvh  19029  efgredlemg  19869  frgpnabllem1  20000  ablsimpgfindlem1  20236  metnrmlem3  25088  iihalf1cn  25160  iihalf2cn  25162  pcoass  25252  cphipval2  25469  csbren  25627  trirn  25628  minveclem2  25654  ovolunlem1a  25724  uniioombllem5  25815  uniioombl  25817  dyaddisjlem  25823  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  dvsincos  26208  lhop1  26241  cosargd  26845  dvcnsqrt  26981  root1id  26991  ssscongptld  27059  chordthmlem  27069  chordthmlem2  27070  chordthmlem4  27072  heron  27075  dcubic1  27082  mcubic  27084  cubic2  27085  quartlem4  27097  quart  27098  cosasin  27141  cosatan  27158  atantayl  27174  atantayl2  27175  atantayl3  27176  log2tlbnd  27182  cxp2limlem  27212  divsqrtsumlem  27216  lgamgulmlem2  27266  lgamgulmlem4  27268  lgamucov  27274  ftalem2  27310  basellem2  27318  basellem3  27319  basellem5  27321  basellem8  27324  logfaclbnd  27458  perfectlem2  27466  perfect  27467  bcp1ctr  27515  bposlem1  27520  bposlem2  27521  lgslem1  27533  lgsqrlem2  27583  gausslemma2dlem1a  27601  gausslemma2dlem3  27604  gausslemma2dlem4  27605  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  lgsquadlem2  27617  lgsquad2lem1  27620  2lgslem1a1  27625  2lgslem1a2  27626  2lgslem1b  27628  2lgslem1c  27629  2lgslem3a1  27636  2lgslem3d1  27639  2sq2  27669  addsq2nreurex  27680  chebbnd1lem3  27707  chto1ub  27712  dchrisumlem2  27726  dchrisum0flblem2  27745  dchrisum0fno1  27747  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2  27754  logdivsum  27769  mulog2sumlem2  27771  vmalogdivsum2  27774  log2sumbnd  27780  selberglem2  27782  chpdifbndlem1  27789  selberg3lem1  27793  selberg3  27795  selberg4lem1  27796  selberg4  27797  selberg4r  27806  selberg34r  27807  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntpbnd1a  27821  pntpbnd2  27823  pntibndlem2  27827  pntlemb  27833  pntlemg  27834  pntlemh  27835  pntlemr  27838  pntlemk  27842  pntlemo  27843  ostth2lem1  27854  finsumvtxdg2ssteplem4  30008  upgrwlkdvdelem  30201  wwlksnextwrd  30365  wwlksnextinj  30367  clwlkclwwlklem2a1  30462  clwlkclwwlklem2a4  30467  clwlkclwwlklem3  30471  clwwlkext2edg  30526  clwwlknonex2lem1  30577  clwwlknonex2lem2  30578  2clwwlk2clwwlk  30830  numclwwlk1lem2foalem  30831  numclwwlk1lem2fo  30838  numclwwlk2lem1  30856  numclwlk2lem2f  30857  numclwwlk2  30861  ex-ind-dvds  30941  nrt2irr  30953  binom2subadd  33212  quad3d  33220  2exple2exp  33304  wrdt2ind  33395  archirngz  33629  archiabllem2c  33635  fldext2rspun  34192  constrrtcc  34245  constrelextdg2  34257  constraddcl  34272  constrrecl  34279  constrresqrtcl  34287  2sqr3nconstr  34291  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminply  34298  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  cos9thpinconstr  34301  sqsscirc1  34418  dya2icoseg  34788  dya2iocucvr  34795  oddpwdc  34865  eulerpartlemgs2  34891  fibp1  34912  signslema  35070  itgexpif  35114  vtsprod  35147  hgt750lemd  35156  logdivsqrle  35158  subfacp1lem1  35758  subfacp1lem5  35763  dnibndlem10  37184  knoppcnlem10  37199  knoppndvlem2  37210  knoppndvlem7  37215  knoppndvlem9  37217  knoppndvlem10  37218  knoppndvlem16  37224  irrdifflemf  38077  qdiff  38079  itg2addnclem  38420  dvasin  38453  areacirclem1  38457  areacirclem3  38459  isbnd2  38533  lcmineqlem21  42915  3lexlogpow2ineq2  42925  dvrelog2b  42932  dvrelogpow2b  42934  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p9  42954  posbezout  42966  2np3bcnp1  43010  2ap1caineq  43011  oddnumth  43186  nicomachus  43187  sumcubes  43188  ef11d  43214  cxpi11d  43218  tan3rdpi  43227  readvrec2  43236  remul02  43280  remul01  43282  dffltz  43480  fltne  43490  flt4lem5e  43502  cu3addd  43526  rmspecsqrtnq  43747  rmxluc  43777  rmyluc2  43779  rmydbl  43781  jm2.18  43829  jm2.22  43836  jm2.25  43840  jm2.27c  43848  jm3.1lem2  43859  sqrtcval  44481  imo72b2lem0  45005  refsum2cnlem1  45871  oddfl  46111  xralrple2  46184  infleinflem2  46200  sumnnodd  46460  0ellimcdiv  46477  coseq0  46692  sinmulcos  46693  coskpi2  46694  sinaover2ne0  46696  cosknegpi  46697  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  itgsinexp  46783  stoweidlem1  46829  stoweidlem62  46890  wallispilem4  46896  wallispilem5  46897  wallispi  46898  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem6  46907  stirlinglem7  46908  stirlinglem8  46909  stirlinglem10  46911  stirlinglem11  46912  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  dirker2re  46920  dirkerdenne0  46921  dirkerval2  46922  dirkerre  46923  dirkertrigeqlem1  46926  dirkertrigeqlem2  46927  dirkertrigeqlem3  46928  dirkertrigeq  46929  dirkeritg  46930  dirkercncflem1  46931  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem43  46978  fourierdlem44  46979  fourierdlem56  46990  fourierdlem57  46991  fourierdlem58  46992  fourierdlem62  46996  fourierdlem66  47000  fourierdlem68  47002  fourierdlem72  47006  fourierdlem76  47010  fourierdlem79  47013  fourierdlem80  47014  fourierdlem83  47017  fourierdlem95  47029  fourierdlem104  47038  fourierdlem112  47046  fouriercnp  47054  fourierswlem  47058  sge0ad2en  47259  hoicvrrex  47384  hoiqssbllem2  47451  sin3t  47735  cos3t  47736  sin5tlem1  47737  sin5tlem3  47739  sin5tlem4  47740  sin5t  47742  2tceilhalfelfzo1  48224  minusmodnep2tmod  48247  modmkpkne  48255  modm2nep1  48260  modm1nem2  48263  fmtnoodd  48436  sqrtpwpw2p  48441  fmtnorec2lem  48445  fmtnodvds  48447  goldbachthlem2  48449  fmtnoprmfac1lem  48467  fmtnoprmfac2  48470  fmtnofac1  48473  2pwp1prm  48492  mod42tp1mod8  48505  sfprmdvdsmersenne  48506  lighneallem2  48509  lighneallem4  48513  proththd  48517  nprmdvdsfacm1lem1  48523  ppivalnn4  48530  quad1  48536  requad01  48537  requad1  48538  requad2  48539  dfodd6  48553  dfeven4  48554  enege  48561  onego  48562  dfeven2  48565  oddflALTV  48579  opoeALTV  48599  opeoALTV  48600  nn0onn0exALTV  48615  nn0enn0exALTV  48616  nnennexALTV  48617  mogoldbblem  48636  perfectALTV  48639  fppr2odd  48647  sgoldbeven3prm  48699  gpg3nbgrvtx0  48992  gpg3kgrtriexlem2  49000  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  0nodd  49085  2nodd  49087  2zlidl  49155  2zrngamgm  49160  2zrngagrp  49164  2zrngmmgm  49167  2zrngnmlid  49170  nn0onn0ex  49453  nn0enn0ex  49454  nnennex  49455  nnpw2even  49459  fldivexpfllog2  49495  blenpw2m1  49509  nnpw2blen  49510  blennn0em1  49521  dig2nn1st  49535  dig2bits  49544  dignn0flhalflem1  49545  dignn0flhalflem2  49546  dignn0ehalf  49547  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  itcovalt2lem2lem2  49604  ackval2  49612  ackval3  49613  itschlc0yqe  49690  itsclc0yqsollem1  49692  itsclc0yqsol  49694  itsclc0xyqsolr  49699  itsclquadb  49706  2itscplem1  49708  2itscplem3  49710  itscnhlinecirc02plem1  49712