Theorem 2cnd 12060

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  2c2 12037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addcl 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-2 12045

This theorem is referenced by:  subhalfhalf  12216  cnm2m1cnm3  12235  xp1d2m1eqxm1d2  12236  zeo2  12416  fzosplitprm1  13506  2tnp1ge0ge0  13558  flhalf  13559  2txmodxeq0  13660  mulbinom2  13947  binom3  13948  zesq  13950  expmulnbnd  13959  discr  13964  sqoddm1div8  13967  mulsubdivbinom2  13985  swrds2m  14663  amgm2  15090  bhmafibid1cn  15184  bhmafibid2cn  15185  iseraltlem2  15403  iseralt  15405  trirecip  15584  geo2sum  15594  bpolydiflem  15773  ege2le3  15808  tanval3  15852  sinhval  15872  tanhlt1  15878  sqrt2irrlem  15966  sqrt2irr  15967  even2n  16060  oddm1even  16061  oddp1even  16062  mod2eq1n2dvds  16065  ltoddhalfle  16079  m1exp1  16094  nn0enne  16095  flodddiv4  16131  flodddiv4t2lthalf  16134  bitsp1e  16148  bitsp1o  16149  bitsfzo  16151  bitsmod  16152  bitsinv1lem  16157  sadadd2lem2  16166  sadcaddlem  16173  bitsuz  16190  bitsshft  16191  prmdiv  16495  vfermltlALT  16512  iserodd  16545  4sqlem7  16654  4sqlem10  16657  4sqlem19  16673  prmgaplem7  16767  2expltfac  16803  smndex2dlinvh  18565  efgredlemg  19357  frgpnabllem1  19483  ablsimpgfindlem1  19719  metnrmlem3  24033  iihalf1cn  24104  iihalf2cn  24106  pcoass  24196  cphipval2  24414  csbren  24572  trirn  24573  minveclem2  24599  ovolunlem1a  24669  uniioombllem5  24760  uniioombl  24762  dyaddisjlem  24768  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  dvsincos  25154  lhop1  25187  cosargd  25772  dvcnsqrt  25906  root1id  25916  ssscongptld  25981  chordthmlem  25991  chordthmlem2  25992  chordthmlem4  25994  heron  25997  dcubic1  26004  mcubic  26006  cubic2  26007  quartlem4  26019  quart  26020  cosasin  26063  cosatan  26080  atantayl  26096  atantayl2  26097  atantayl3  26098  log2tlbnd  26104  cxp2limlem  26134  divsqrtsumlem  26138  lgamgulmlem2  26188  lgamgulmlem4  26190  lgamucov  26196  ftalem2  26232  basellem2  26240  basellem3  26241  basellem5  26243  basellem8  26246  logfaclbnd  26379  perfectlem2  26387  perfect  26388  bcp1ctr  26436  bposlem1  26441  bposlem2  26442  lgslem1  26454  lgsqrlem2  26504  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  gausslemma2dlem4  26526  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2lem1  26541  2lgslem1a1  26546  2lgslem1a2  26547  2lgslem1b  26549  2lgslem1c  26550  2lgslem3a1  26557  2lgslem3d1  26560  2sq2  26590  addsq2nreurex  26601  chebbnd1lem3  26628  chto1ub  26633  dchrisumlem2  26647  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2  26675  logdivsum  26690  mulog2sumlem2  26692  vmalogdivsum2  26695  log2sumbnd  26701  selberglem2  26703  chpdifbndlem1  26710  selberg3lem1  26714  selberg3  26716  selberg4lem1  26717  selberg4  26718  selberg4r  26727  selberg34r  26728  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntpbnd1a  26742  pntpbnd2  26744  pntibndlem2  26748  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemr  26759  pntlemk  26763  pntlemo  26764  ostth2lem1  26775  finsumvtxdg2ssteplem4  27924  upgrwlkdvdelem  28113  wwlksnextwrd  28271  wwlksnextinj  28273  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a4  28370  clwlkclwwlklem3  28374  clwwlkext2edg  28429  clwwlknonex2lem1  28480  clwwlknonex2lem2  28481  2clwwlk2clwwlk  28723  numclwwlk1lem2foalem  28724  numclwwlk1lem2fo  28731  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwwlk2  28754  ex-ind-dvds  28834  wrdt2ind  31234  archirngz  31452  archiabllem2c  31458  sqsscirc1  31867  dya2icoseg  32253  dya2iocucvr  32260  oddpwdc  32330  eulerpartlemgs2  32356  fibp1  32377  signslema  32550  itgexpif  32595  vtsprod  32628  hgt750lemd  32637  logdivsqrle  32639  subfacp1lem1  33150  subfacp1lem5  33155  dnibndlem10  34676  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem9  34709  knoppndvlem10  34710  knoppndvlem16  34716  irrdifflemf  35505  itg2addnclem  35837  dvasin  35870  areacirclem1  35874  areacirclem3  35876  isbnd2  35950  lcmineqlem21  40064  3lexlogpow2ineq2  40074  dvrelog2b  40081  dvrelogpow2b  40083  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p9  40103  2np3bcnp1  40107  2ap1caineq  40108  remul02  40395  remul01  40397  dffltz  40478  fltne  40488  flt4lem5e  40500  cu3addd  40509  rmspecsqrtnq  40735  rmxluc  40765  rmyluc2  40767  rmydbl  40769  jm2.18  40817  jm2.22  40824  jm2.25  40828  jm2.27c  40836  jm3.1lem2  40847  sqrtcval  41256  imo72b2lem0  41783  refsum2cnlem1  42587  oddfl  42823  xralrple2  42900  infleinflem2  42917  sumnnodd  43178  0ellimcdiv  43197  coseq0  43412  sinmulcos  43413  coskpi2  43414  sinaover2ne0  43416  cosknegpi  43417  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  itgsinexp  43503  stoweidlem1  43549  stoweidlem62  43610  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  dirker2re  43640  dirkerdenne0  43641  dirkerval2  43642  dirkerre  43643  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem43  43698  fourierdlem44  43699  fourierdlem56  43710  fourierdlem57  43711  fourierdlem58  43712  fourierdlem62  43716  fourierdlem66  43720  fourierdlem68  43722  fourierdlem72  43726  fourierdlem76  43730  fourierdlem79  43733  fourierdlem80  43734  fourierdlem83  43737  fourierdlem95  43749  fourierdlem104  43758  fourierdlem112  43766  fouriercnp  43774  fourierswlem  43778  sge0ad2en  43976  hoicvrrex  44101  hoiqssbllem2  44168  fmtnoodd  44996  sqrtpwpw2p  45001  fmtnorec2lem  45005  fmtnodvds  45007  goldbachthlem2  45009  fmtnoprmfac1lem  45027  fmtnoprmfac2  45030  fmtnofac1  45033  2pwp1prm  45052  mod42tp1mod8  45065  sfprmdvdsmersenne  45066  lighneallem2  45069  lighneallem4  45073  proththd  45077  quad1  45083  requad01  45084  requad1  45085  requad2  45086  dfodd6  45100  dfeven4  45101  enege  45108  onego  45109  dfeven2  45112  oddflALTV  45126  opoeALTV  45146  opeoALTV  45147  nn0onn0exALTV  45162  nn0enn0exALTV  45163  nnennexALTV  45164  mogoldbblem  45183  perfectALTV  45186  fppr2odd  45194  sgoldbeven3prm  45246  0nodd  45375  2nodd  45377  2zlidl  45503  2zrngamgm  45508  2zrngagrp  45512  2zrngmmgm  45515  2zrngnmlid  45518  nn0onn0ex  45880  nn0enn0ex  45881  nnennex  45882  nnpw2even  45886  fldivexpfllog2  45922  blenpw2m1  45936  nnpw2blen  45937  blennn0em1  45948  dig2nn1st  45962  dig2bits  45971  dignn0flhalflem1  45972  dignn0flhalflem2  45973  dignn0ehalf  45974  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  itcovalt2lem2lem2  46031  ackval2  46039  ackval3  46040  itschlc0yqe  46117  itsclc0yqsollem1  46119  itsclc0yqsol  46121  itsclc0xyqsolr  46126  itsclquadb  46133  2itscplem1  46135  2itscplem3  46137  itscnhlinecirc02plem1  46139