Theorem 2cnd 12264

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  2c2 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249

This theorem is referenced by:  subhalfhalf  12416  cnm2m1cnm3  12435  xp1d2m1eqxm1d2  12436  zeo2  12621  ge2halflem1  13068  fzosplitprm1  13738  2tnp1ge0ge0  13791  flhalf  13792  2txmodxeq0  13896  mulbinom2  14188  binom3  14189  zesq  14191  expmulnbnd  14200  discr  14205  sqoddm1div8  14208  mulsubdivbinom2  14227  swrds2m  14907  amgm2  15336  bhmafibid1cn  15432  bhmafibid2cn  15433  iseraltlem2  15649  iseralt  15651  trirecip  15829  geo2sum  15839  bpolydiflem  16020  ege2le3  16056  tanval3  16102  sinhval  16122  tanhlt1  16128  sqrt2irrlem  16216  sqrt2irr  16217  even2n  16312  oddm1even  16313  oddp1even  16314  mod2eq1n2dvds  16317  ltoddhalfle  16331  m1exp1  16346  nn0enne  16347  flodddiv4  16385  flodddiv4t2lthalf  16388  bitsp1e  16402  bitsp1o  16403  bitsfzo  16405  bitsmod  16406  bitsinv1lem  16411  sadadd2lem2  16420  sadcaddlem  16427  bitsuz  16444  bitsshft  16445  prmdiv  16755  vfermltlALT  16773  iserodd  16806  4sqlem7  16915  4sqlem10  16918  4sqlem19  16934  prmgaplem7  17028  2expltfac  17063  smndex2dlinvh  18844  efgredlemg  19672  frgpnabllem1  19803  ablsimpgfindlem1  20039  metnrmlem3  24750  iihalf1cn  24826  iihalf1cnOLD  24827  iihalf2cn  24829  iihalf2cnOLD  24830  pcoass  24924  cphipval2  25141  csbren  25299  trirn  25300  minveclem2  25326  ovolunlem1a  25397  uniioombllem5  25488  uniioombl  25490  dyaddisjlem  25496  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  dvsincos  25885  lhop1  25919  cosargd  26517  dvcnsqrt  26653  root1id  26664  ssscongptld  26732  chordthmlem  26742  chordthmlem2  26743  chordthmlem4  26745  heron  26748  dcubic1  26755  mcubic  26757  cubic2  26758  quartlem4  26770  quart  26771  cosasin  26814  cosatan  26831  atantayl  26847  atantayl2  26848  atantayl3  26849  log2tlbnd  26855  cxp2limlem  26886  divsqrtsumlem  26890  lgamgulmlem2  26940  lgamgulmlem4  26942  lgamucov  26948  ftalem2  26984  basellem2  26992  basellem3  26993  basellem5  26995  basellem8  26998  logfaclbnd  27133  perfectlem2  27141  perfect  27142  bcp1ctr  27190  bposlem1  27195  bposlem2  27196  lgslem1  27208  lgsqrlem2  27258  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  gausslemma2dlem4  27280  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem1  27295  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1b  27303  2lgslem1c  27304  2lgslem3a1  27311  2lgslem3d1  27314  2sq2  27344  addsq2nreurex  27355  chebbnd1lem3  27382  chto1ub  27387  dchrisumlem2  27401  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2  27429  logdivsum  27444  mulog2sumlem2  27446  vmalogdivsum2  27449  log2sumbnd  27455  selberglem2  27457  chpdifbndlem1  27464  selberg3lem1  27468  selberg3  27470  selberg4lem1  27471  selberg4  27472  selberg4r  27481  selberg34r  27482  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2  27502  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemr  27513  pntlemk  27517  pntlemo  27518  ostth2lem1  27529  finsumvtxdg2ssteplem4  29476  upgrwlkdvdelem  29666  wwlksnextwrd  29827  wwlksnextinj  29829  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a4  29926  clwlkclwwlklem3  29930  clwwlkext2edg  29985  clwwlknonex2lem1  30036  clwwlknonex2lem2  30037  2clwwlk2clwwlk  30279  numclwwlk1lem2foalem  30280  numclwwlk1lem2fo  30287  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwwlk2  30310  ex-ind-dvds  30390  nrt2irr  30402  binom2subadd  32665  quad3d  32673  2exple2exp  32770  wrdt2ind  32875  archirngz  33143  archiabllem2c  33149  fldext2rspun  33677  constrrtcc  33725  constrelextdg2  33737  constraddcl  33752  constrrecl  33759  constrresqrtcl  33767  2sqr3nconstr  33771  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cos9thpinconstr  33781  sqsscirc1  33898  dya2icoseg  34268  dya2iocucvr  34275  oddpwdc  34345  eulerpartlemgs2  34371  fibp1  34392  signslema  34553  itgexpif  34597  vtsprod  34630  hgt750lemd  34639  logdivsqrle  34641  subfacp1lem1  35166  subfacp1lem5  35171  dnibndlem10  36475  knoppcnlem10  36490  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem9  36508  knoppndvlem10  36509  knoppndvlem16  36515  irrdifflemf  37313  itg2addnclem  37665  dvasin  37698  areacirclem1  37702  areacirclem3  37704  isbnd2  37777  lcmineqlem21  42037  3lexlogpow2ineq2  42047  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p9  42076  posbezout  42088  2np3bcnp1  42132  2ap1caineq  42133  oddnumth  42299  nicomachus  42300  sumcubes  42301  ef11d  42327  cxpi11d  42331  tan3rdpi  42340  readvrec2  42349  remul02  42393  remul01  42395  dffltz  42622  fltne  42632  flt4lem5e  42644  cu3addd  42669  rmspecsqrtnq  42894  rmxluc  42925  rmyluc2  42927  rmydbl  42929  jm2.18  42977  jm2.22  42984  jm2.25  42988  jm2.27c  42996  jm3.1lem2  43007  sqrtcval  43630  imo72b2lem0  44154  refsum2cnlem1  45031  oddfl  45276  xralrple2  45350  infleinflem2  45367  sumnnodd  45628  0ellimcdiv  45647  coseq0  45862  sinmulcos  45863  coskpi2  45864  sinaover2ne0  45866  cosknegpi  45867  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  itgsinexp  45953  stoweidlem1  45999  stoweidlem62  46060  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirker2re  46090  dirkerdenne0  46091  dirkerval2  46092  dirkerre  46093  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem43  46148  fourierdlem44  46149  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem66  46170  fourierdlem68  46172  fourierdlem72  46176  fourierdlem76  46180  fourierdlem79  46183  fourierdlem80  46184  fourierdlem83  46187  fourierdlem95  46199  fourierdlem104  46208  fourierdlem112  46216  fouriercnp  46224  fourierswlem  46228  sge0ad2en  46429  hoicvrrex  46554  hoiqssbllem2  46621  2tceilhalfelfzo1  47333  minusmodnep2tmod  47354  modmkpkne  47362  modm2nep1  47367  modm1nem2  47370  fmtnoodd  47534  sqrtpwpw2p  47539  fmtnorec2lem  47543  fmtnodvds  47545  goldbachthlem2  47547  fmtnoprmfac1lem  47565  fmtnoprmfac2  47568  fmtnofac1  47571  2pwp1prm  47590  mod42tp1mod8  47603  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem4  47611  proththd  47615  quad1  47621  requad01  47622  requad1  47623  requad2  47624  dfodd6  47638  dfeven4  47639  enege  47646  onego  47647  dfeven2  47650  oddflALTV  47664  opoeALTV  47684  opeoALTV  47685  nn0onn0exALTV  47700  nn0enn0exALTV  47701  nnennexALTV  47702  mogoldbblem  47721  perfectALTV  47724  fppr2odd  47732  sgoldbeven3prm  47784  gpg3nbgrvtx0  48067  gpg3kgrtriexlem2  48075  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  0nodd  48158  2nodd  48160  2zlidl  48228  2zrngamgm  48233  2zrngagrp  48237  2zrngmmgm  48240  2zrngnmlid  48243  nn0onn0ex  48512  nn0enn0ex  48513  nnennex  48514  nnpw2even  48518  fldivexpfllog2  48554  blenpw2m1  48568  nnpw2blen  48569  blennn0em1  48580  dig2nn1st  48594  dig2bits  48603  dignn0flhalflem1  48604  dignn0flhalflem2  48605  dignn0ehalf  48606  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itcovalt2lem2lem2  48663  ackval2  48671  ackval3  48672  itschlc0yqe  48749  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itsclc0xyqsolr  48758  itsclquadb  48765  2itscplem1  48767  2itscplem3  48769  itscnhlinecirc02plem1  48771