Theorem 2cnd 12271

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  2c2 12248

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 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256

This theorem is referenced by:  subhalfhalf  12423  cnm2m1cnm3  12442  xp1d2m1eqxm1d2  12443  zeo2  12628  ge2halflem1  13075  fzosplitprm1  13745  2tnp1ge0ge0  13798  flhalf  13799  2txmodxeq0  13903  mulbinom2  14195  binom3  14196  zesq  14198  expmulnbnd  14207  discr  14212  sqoddm1div8  14215  mulsubdivbinom2  14234  swrds2m  14914  amgm2  15343  bhmafibid1cn  15439  bhmafibid2cn  15440  iseraltlem2  15656  iseralt  15658  trirecip  15836  geo2sum  15846  bpolydiflem  16027  ege2le3  16063  tanval3  16109  sinhval  16129  tanhlt1  16135  sqrt2irrlem  16223  sqrt2irr  16224  even2n  16319  oddm1even  16320  oddp1even  16321  mod2eq1n2dvds  16324  ltoddhalfle  16338  m1exp1  16353  nn0enne  16354  flodddiv4  16392  flodddiv4t2lthalf  16395  bitsp1e  16409  bitsp1o  16410  bitsfzo  16412  bitsmod  16413  bitsinv1lem  16418  sadadd2lem2  16427  sadcaddlem  16434  bitsuz  16451  bitsshft  16452  prmdiv  16762  vfermltlALT  16780  iserodd  16813  4sqlem7  16922  4sqlem10  16925  4sqlem19  16941  prmgaplem7  17035  2expltfac  17070  smndex2dlinvh  18851  efgredlemg  19679  frgpnabllem1  19810  ablsimpgfindlem1  20046  metnrmlem3  24757  iihalf1cn  24833  iihalf1cnOLD  24834  iihalf2cn  24836  iihalf2cnOLD  24837  pcoass  24931  cphipval2  25148  csbren  25306  trirn  25307  minveclem2  25333  ovolunlem1a  25404  uniioombllem5  25495  uniioombl  25497  dyaddisjlem  25503  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  dvsincos  25892  lhop1  25926  cosargd  26524  dvcnsqrt  26660  root1id  26671  ssscongptld  26739  chordthmlem  26749  chordthmlem2  26750  chordthmlem4  26752  heron  26755  dcubic1  26762  mcubic  26764  cubic2  26765  quartlem4  26777  quart  26778  cosasin  26821  cosatan  26838  atantayl  26854  atantayl2  26855  atantayl3  26856  log2tlbnd  26862  cxp2limlem  26893  divsqrtsumlem  26897  lgamgulmlem2  26947  lgamgulmlem4  26949  lgamucov  26955  ftalem2  26991  basellem2  26999  basellem3  27000  basellem5  27002  basellem8  27005  logfaclbnd  27140  perfectlem2  27148  perfect  27149  bcp1ctr  27197  bposlem1  27202  bposlem2  27203  lgslem1  27215  lgsqrlem2  27265  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  gausslemma2dlem4  27287  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem1  27302  2lgslem1a1  27307  2lgslem1a2  27308  2lgslem1b  27310  2lgslem1c  27311  2lgslem3a1  27318  2lgslem3d1  27321  2sq2  27351  addsq2nreurex  27362  chebbnd1lem3  27389  chto1ub  27394  dchrisumlem2  27408  dchrisum0flblem2  27427  dchrisum0fno1  27429  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2  27436  logdivsum  27451  mulog2sumlem2  27453  vmalogdivsum2  27456  log2sumbnd  27462  selberglem2  27464  chpdifbndlem1  27471  selberg3lem1  27475  selberg3  27477  selberg4lem1  27478  selberg4  27479  selberg4r  27488  selberg34r  27489  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2  27509  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemr  27520  pntlemk  27524  pntlemo  27525  ostth2lem1  27536  finsumvtxdg2ssteplem4  29483  upgrwlkdvdelem  29673  wwlksnextwrd  29834  wwlksnextinj  29836  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a4  29933  clwlkclwwlklem3  29937  clwwlkext2edg  29992  clwwlknonex2lem1  30043  clwwlknonex2lem2  30044  2clwwlk2clwwlk  30286  numclwwlk1lem2foalem  30287  numclwwlk1lem2fo  30294  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwwlk2  30317  ex-ind-dvds  30397  nrt2irr  30409  binom2subadd  32672  quad3d  32680  2exple2exp  32777  wrdt2ind  32882  archirngz  33150  archiabllem2c  33156  fldext2rspun  33684  constrrtcc  33732  constrelextdg2  33744  constraddcl  33759  constrrecl  33766  constrresqrtcl  33774  2sqr3nconstr  33778  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminply  33785  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  cos9thpinconstr  33788  sqsscirc1  33905  dya2icoseg  34275  dya2iocucvr  34282  oddpwdc  34352  eulerpartlemgs2  34378  fibp1  34399  signslema  34560  itgexpif  34604  vtsprod  34637  hgt750lemd  34646  logdivsqrle  34648  subfacp1lem1  35173  subfacp1lem5  35178  dnibndlem10  36482  knoppcnlem10  36497  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem9  36515  knoppndvlem10  36516  knoppndvlem16  36522  irrdifflemf  37320  itg2addnclem  37672  dvasin  37705  areacirclem1  37709  areacirclem3  37711  isbnd2  37784  lcmineqlem21  42044  3lexlogpow2ineq2  42054  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p9  42083  posbezout  42095  2np3bcnp1  42139  2ap1caineq  42140  oddnumth  42306  nicomachus  42307  sumcubes  42308  ef11d  42334  cxpi11d  42338  tan3rdpi  42347  readvrec2  42356  remul02  42400  remul01  42402  dffltz  42629  fltne  42639  flt4lem5e  42651  cu3addd  42676  rmspecsqrtnq  42901  rmxluc  42932  rmyluc2  42934  rmydbl  42936  jm2.18  42984  jm2.22  42991  jm2.25  42995  jm2.27c  43003  jm3.1lem2  43014  sqrtcval  43637  imo72b2lem0  44161  refsum2cnlem1  45038  oddfl  45283  xralrple2  45357  infleinflem2  45374  sumnnodd  45635  0ellimcdiv  45654  coseq0  45869  sinmulcos  45870  coskpi2  45871  sinaover2ne0  45873  cosknegpi  45874  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  itgsinexp  45960  stoweidlem1  46006  stoweidlem62  46067  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirker2re  46097  dirkerdenne0  46098  dirkerval2  46099  dirkerre  46100  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkeritg  46107  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem43  46155  fourierdlem44  46156  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem66  46177  fourierdlem68  46179  fourierdlem72  46183  fourierdlem76  46187  fourierdlem79  46190  fourierdlem80  46191  fourierdlem83  46194  fourierdlem95  46206  fourierdlem104  46215  fourierdlem112  46223  fouriercnp  46231  fourierswlem  46235  sge0ad2en  46436  hoicvrrex  46561  hoiqssbllem2  46628  2tceilhalfelfzo1  47337  minusmodnep2tmod  47358  modmkpkne  47366  modm2nep1  47371  modm1nem2  47374  fmtnoodd  47538  sqrtpwpw2p  47543  fmtnorec2lem  47547  fmtnodvds  47549  goldbachthlem2  47551  fmtnoprmfac1lem  47569  fmtnoprmfac2  47572  fmtnofac1  47575  2pwp1prm  47594  mod42tp1mod8  47607  sfprmdvdsmersenne  47608  lighneallem2  47611  lighneallem4  47615  proththd  47619  quad1  47625  requad01  47626  requad1  47627  requad2  47628  dfodd6  47642  dfeven4  47643  enege  47650  onego  47651  dfeven2  47654  oddflALTV  47668  opoeALTV  47688  opeoALTV  47689  nn0onn0exALTV  47704  nn0enn0exALTV  47705  nnennexALTV  47706  mogoldbblem  47725  perfectALTV  47728  fppr2odd  47736  sgoldbeven3prm  47788  gpg3nbgrvtx0  48071  gpg3kgrtriexlem2  48079  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  0nodd  48162  2nodd  48164  2zlidl  48232  2zrngamgm  48237  2zrngagrp  48241  2zrngmmgm  48244  2zrngnmlid  48247  nn0onn0ex  48516  nn0enn0ex  48517  nnennex  48518  nnpw2even  48522  fldivexpfllog2  48558  blenpw2m1  48572  nnpw2blen  48573  blennn0em1  48584  dig2nn1st  48598  dig2bits  48607  dignn0flhalflem1  48608  dignn0flhalflem2  48609  dignn0ehalf  48610  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  itcovalt2lem2lem2  48667  ackval2  48675  ackval3  48676  itschlc0yqe  48753  itsclc0yqsollem1  48755  itsclc0yqsol  48757  itsclc0xyqsolr  48762  itsclquadb  48769  2itscplem1  48771  2itscplem3  48773  itscnhlinecirc02plem1  48775