Theorem 2cnd 12314

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11093  2c2 12290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298

This theorem is referenced by:  subhalfhalf  12473  cnm2m1cnm3  12492  xp1d2m1eqxm1d2  12493  zeo2  12678  ge2halflem1  13128  fzosplitprm1  13803  2tnp1ge0ge0  13858  flhalf  13859  2txmodxeq0  13963  mulbinom2  14255  binom3  14256  zesq  14258  expmulnbnd  14267  discr  14272  sqoddm1div8  14275  mulsubdivbinom2  14294  swrds2m  14974  amgm2  15417  bhmafibid1cn  15513  bhmafibid2cn  15514  iseraltlem2  15730  iseralt  15732  trirecip  15913  geo2sum  15923  bpolydiflem  16103  bpoly4  16108  ege2le3  16139  tanval3  16185  sinhval  16205  tanhlt1  16211  sqrt2irrlem  16299  sqrt2irr  16300  even2n  16395  oddm1even  16396  oddp1even  16397  mod2eq1n2dvds  16400  ltoddhalfle  16414  m1exp1  16429  nn0enne  16430  flodddiv4  16468  flodddiv4t2lthalf  16471  bitsp1e  16485  bitsp1o  16486  bitsfzo  16488  bitsmod  16489  bitsinv1lem  16494  sadadd2lem2  16503  sadcaddlem  16510  bitsuz  16527  bitsshft  16528  prmdiv  16839  vfermltlALT  16857  iserodd  16890  4sqlem7  16999  4sqlem10  17002  4sqlem19  17018  prmgaplem7  17112  2expltfac  17147  smndex2dlinvh  18974  efgredlemg  19807  frgpnabllem1  19938  ablsimpgfindlem1  20174  metnrmlem3  25019  iihalf1cn  25091  iihalf2cn  25093  pcoass  25183  cphipval2  25400  csbren  25558  trirn  25559  minveclem2  25585  ovolunlem1a  25655  uniioombllem5  25746  uniioombl  25748  dyaddisjlem  25754  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  dvsincos  26140  lhop1  26173  cosargd  26773  dvcnsqrt  26909  root1id  26919  ssscongptld  26987  chordthmlem  26997  chordthmlem2  26998  chordthmlem4  27000  heron  27003  dcubic1  27010  mcubic  27012  cubic2  27013  quartlem4  27025  quart  27026  cosasin  27069  cosatan  27086  atantayl  27102  atantayl2  27103  atantayl3  27104  log2tlbnd  27110  cxp2limlem  27140  divsqrtsumlem  27144  lgamgulmlem2  27194  lgamgulmlem4  27196  lgamucov  27202  ftalem2  27238  basellem2  27246  basellem3  27247  basellem5  27249  basellem8  27252  logfaclbnd  27386  perfectlem2  27394  perfect  27395  bcp1ctr  27443  bposlem1  27448  bposlem2  27449  lgslem1  27461  lgsqrlem2  27511  gausslemma2dlem1a  27529  gausslemma2dlem3  27532  gausslemma2dlem4  27533  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgsquadlem1  27544  lgsquadlem2  27545  lgsquad2lem1  27548  2lgslem1a1  27553  2lgslem1a2  27554  2lgslem1b  27556  2lgslem1c  27557  2lgslem3a1  27564  2lgslem3d1  27567  2sq2  27597  addsq2nreurex  27608  chebbnd1lem3  27635  chto1ub  27640  dchrisumlem2  27654  dchrisum0flblem2  27673  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2  27682  logdivsum  27697  mulog2sumlem2  27699  vmalogdivsum2  27702  log2sumbnd  27708  selberglem2  27710  chpdifbndlem1  27717  selberg3lem1  27721  selberg3  27723  selberg4lem1  27724  selberg4  27725  selberg4r  27734  selberg34r  27735  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem2  27755  pntlemb  27761  pntlemg  27762  pntlemh  27763  pntlemr  27766  pntlemk  27770  pntlemo  27771  ostth2lem1  27782  finsumvtxdg2ssteplem4  29898  upgrwlkdvdelem  30085  wwlksnextwrd  30246  wwlksnextinj  30248  clwlkclwwlklem2a1  30343  clwlkclwwlklem2a4  30348  clwlkclwwlklem3  30352  clwwlkext2edg  30407  clwwlknonex2lem1  30458  clwwlknonex2lem2  30459  2clwwlk2clwwlk  30701  numclwwlk1lem2foalem  30702  numclwwlk1lem2fo  30709  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwwlk2  30732  ex-ind-dvds  30812  nrt2irr  30824  binom2subadd  33086  quad3d  33094  2exple2exp  33178  wrdt2ind  33273  archirngz  33509  archiabllem2c  33515  fldext2rspun  34072  constrrtcc  34125  constrelextdg2  34137  constraddcl  34152  constrrecl  34159  constrresqrtcl  34167  2sqr3nconstr  34171  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  cos9thpinconstr  34181  sqsscirc1  34298  dya2icoseg  34667  dya2iocucvr  34674  oddpwdc  34744  eulerpartlemgs2  34770  fibp1  34791  signslema  34949  itgexpif  34993  vtsprod  35026  hgt750lemd  35035  logdivsqrle  35037  subfacp1lem1  35671  subfacp1lem5  35676  dnibndlem10  37076  knoppcnlem10  37091  knoppndvlem2  37102  knoppndvlem7  37107  knoppndvlem9  37109  knoppndvlem10  37110  knoppndvlem16  37116  irrdifflemf  37969  qdiff  37971  itg2addnclem  38322  dvasin  38355  areacirclem1  38359  areacirclem3  38361  isbnd2  38434  lcmineqlem21  42816  3lexlogpow2ineq2  42826  dvrelog2b  42833  dvrelogpow2b  42835  aks4d1p1p4  42838  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p9  42855  posbezout  42867  2np3bcnp1  42911  2ap1caineq  42912  oddnumth  43072  nicomachus  43073  sumcubes  43074  ef11d  43100  cxpi11d  43104  tan3rdpi  43113  readvrec2  43122  remul02  43166  remul01  43168  dffltz  43366  fltne  43376  flt4lem5e  43388  cu3addd  43412  rmspecsqrtnq  43633  rmxluc  43663  rmyluc2  43665  rmydbl  43667  jm2.18  43715  jm2.22  43722  jm2.25  43726  jm2.27c  43734  jm3.1lem2  43745  sqrtcval  44367  imo72b2lem0  44891  refsum2cnlem1  45757  oddfl  45997  xralrple2  46070  infleinflem2  46086  sumnnodd  46346  0ellimcdiv  46363  coseq0  46578  sinmulcos  46579  coskpi2  46580  sinaover2ne0  46582  cosknegpi  46583  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  itgsinexp  46669  stoweidlem1  46715  stoweidlem62  46776  wallispilem4  46782  wallispilem5  46783  wallispi  46784  wallispi2lem1  46785  wallispi2lem2  46786  wallispi2  46787  stirlinglem1  46788  stirlinglem3  46790  stirlinglem4  46791  stirlinglem5  46792  stirlinglem6  46793  stirlinglem7  46794  stirlinglem8  46795  stirlinglem10  46797  stirlinglem11  46798  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  dirker2re  46806  dirkerdenne0  46807  dirkerval2  46808  dirkerre  46809  dirkertrigeqlem1  46812  dirkertrigeqlem2  46813  dirkertrigeqlem3  46814  dirkertrigeq  46815  dirkeritg  46816  dirkercncflem1  46817  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem43  46864  fourierdlem44  46865  fourierdlem56  46876  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fourierdlem66  46886  fourierdlem68  46888  fourierdlem72  46892  fourierdlem76  46896  fourierdlem79  46899  fourierdlem80  46900  fourierdlem83  46903  fourierdlem95  46915  fourierdlem104  46924  fourierdlem112  46932  fouriercnp  46940  fourierswlem  46944  sge0ad2en  47145  hoicvrrex  47270  hoiqssbllem2  47337  sin3t  47608  cos3t  47609  sin5tlem1  47610  sin5tlem3  47612  sin5tlem4  47613  sin5t  47615  2tceilhalfelfzo1  48073  minusmodnep2tmod  48096  modmkpkne  48104  modm2nep1  48109  modm1nem2  48112  fmtnoodd  48285  sqrtpwpw2p  48290  fmtnorec2lem  48294  fmtnodvds  48296  goldbachthlem2  48298  fmtnoprmfac1lem  48316  fmtnoprmfac2  48319  fmtnofac1  48322  2pwp1prm  48341  mod42tp1mod8  48354  sfprmdvdsmersenne  48355  lighneallem2  48358  lighneallem4  48362  proththd  48366  nprmdvdsfacm1lem1  48372  ppivalnn4  48379  quad1  48385  requad01  48386  requad1  48387  requad2  48388  dfodd6  48402  dfeven4  48403  enege  48410  onego  48411  dfeven2  48414  oddflALTV  48428  opoeALTV  48448  opeoALTV  48449  nn0onn0exALTV  48464  nn0enn0exALTV  48465  nnennexALTV  48466  mogoldbblem  48485  perfectALTV  48488  fppr2odd  48496  sgoldbeven3prm  48548  gpg3nbgrvtx0  48841  gpg3kgrtriexlem2  48849  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  0nodd  48935  2nodd  48937  2zlidl  49005  2zrngamgm  49010  2zrngagrp  49014  2zrngmmgm  49017  2zrngnmlid  49020  nn0onn0ex  49303  nn0enn0ex  49304  nnennex  49305  nnpw2even  49309  fldivexpfllog2  49345  blenpw2m1  49359  nnpw2blen  49360  blennn0em1  49371  dig2nn1st  49385  dig2bits  49394  dignn0flhalflem1  49395  dignn0flhalflem2  49396  dignn0ehalf  49397  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  itcovalt2lem2lem2  49454  ackval2  49462  ackval3  49463  itschlc0yqe  49540  itsclc0yqsollem1  49542  itsclc0yqsol  49544  itsclc0xyqsolr  49549  itsclquadb  49556  2itscplem1  49558  2itscplem3  49560  itscnhlinecirc02plem1  49562