Theorem 2cnd 12306

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℂcc 11122  2c2 12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-1cn 11182  ax-addcl 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-clel 2805  df-2 12291

This theorem is referenced by:  subhalfhalf  12462  cnm2m1cnm3  12481  xp1d2m1eqxm1d2  12482  zeo2  12665  fzosplitprm1  13760  2tnp1ge0ge0  13812  flhalf  13813  2txmodxeq0  13914  mulbinom2  14203  binom3  14204  zesq  14206  expmulnbnd  14215  discr  14220  sqoddm1div8  14223  mulsubdivbinom2  14239  swrds2m  14910  amgm2  15334  bhmafibid1cn  15428  bhmafibid2cn  15429  iseraltlem2  15647  iseralt  15649  trirecip  15827  geo2sum  15837  bpolydiflem  16016  ege2le3  16052  tanval3  16096  sinhval  16116  tanhlt1  16122  sqrt2irrlem  16210  sqrt2irr  16211  even2n  16304  oddm1even  16305  oddp1even  16306  mod2eq1n2dvds  16309  ltoddhalfle  16323  m1exp1  16338  nn0enne  16339  flodddiv4  16375  flodddiv4t2lthalf  16378  bitsp1e  16392  bitsp1o  16393  bitsfzo  16395  bitsmod  16396  bitsinv1lem  16401  sadadd2lem2  16410  sadcaddlem  16417  bitsuz  16434  bitsshft  16435  prmdiv  16739  vfermltlALT  16756  iserodd  16789  4sqlem7  16898  4sqlem10  16901  4sqlem19  16917  prmgaplem7  17011  2expltfac  17047  smndex2dlinvh  18854  efgredlemg  19681  frgpnabllem1  19812  ablsimpgfindlem1  20048  metnrmlem3  24751  iihalf1cn  24827  iihalf1cnOLD  24828  iihalf2cn  24830  iihalf2cnOLD  24831  pcoass  24925  cphipval2  25143  csbren  25301  trirn  25302  minveclem2  25328  ovolunlem1a  25399  uniioombllem5  25490  uniioombl  25492  dyaddisjlem  25498  mbfi1fseqlem5  25623  mbfi1fseqlem6  25624  dvsincos  25887  lhop1  25921  cosargd  26516  dvcnsqrt  26652  root1id  26663  ssscongptld  26728  chordthmlem  26738  chordthmlem2  26739  chordthmlem4  26741  heron  26744  dcubic1  26751  mcubic  26753  cubic2  26754  quartlem4  26766  quart  26767  cosasin  26810  cosatan  26827  atantayl  26843  atantayl2  26844  atantayl3  26845  log2tlbnd  26851  cxp2limlem  26882  divsqrtsumlem  26886  lgamgulmlem2  26936  lgamgulmlem4  26938  lgamucov  26944  ftalem2  26980  basellem2  26988  basellem3  26989  basellem5  26991  basellem8  26994  logfaclbnd  27129  perfectlem2  27137  perfect  27138  bcp1ctr  27186  bposlem1  27191  bposlem2  27192  lgslem1  27204  lgsqrlem2  27254  gausslemma2dlem1a  27272  gausslemma2dlem3  27275  gausslemma2dlem4  27276  lgseisenlem1  27282  lgseisenlem2  27283  lgseisenlem3  27284  lgseisenlem4  27285  lgsquadlem1  27287  lgsquadlem2  27288  lgsquad2lem1  27291  2lgslem1a1  27296  2lgslem1a2  27297  2lgslem1b  27299  2lgslem1c  27300  2lgslem3a1  27307  2lgslem3d1  27310  2sq2  27340  addsq2nreurex  27351  chebbnd1lem3  27378  chto1ub  27383  dchrisumlem2  27397  dchrisum0flblem2  27416  dchrisum0fno1  27418  dchrisum0lem1b  27422  dchrisum0lem1  27423  dchrisum0lem2  27425  logdivsum  27440  mulog2sumlem2  27442  vmalogdivsum2  27445  log2sumbnd  27451  selberglem2  27453  chpdifbndlem1  27460  selberg3lem1  27464  selberg3  27466  selberg4lem1  27467  selberg4  27468  selberg4r  27477  selberg34r  27478  pntrlog2bndlem3  27486  pntrlog2bndlem4  27487  pntrlog2bndlem5  27488  pntrlog2bndlem6  27490  pntpbnd1a  27492  pntpbnd2  27494  pntibndlem2  27498  pntlemb  27504  pntlemg  27505  pntlemh  27506  pntlemr  27509  pntlemk  27513  pntlemo  27514  ostth2lem1  27525  finsumvtxdg2ssteplem4  29336  upgrwlkdvdelem  29524  wwlksnextwrd  29682  wwlksnextinj  29684  clwlkclwwlklem2a1  29776  clwlkclwwlklem2a4  29781  clwlkclwwlklem3  29785  clwwlkext2edg  29840  clwwlknonex2lem1  29891  clwwlknonex2lem2  29892  2clwwlk2clwwlk  30134  numclwwlk1lem2foalem  30135  numclwwlk1lem2fo  30142  numclwwlk2lem1  30160  numclwlk2lem2f  30161  numclwwlk2  30165  ex-ind-dvds  30245  nrt2irr  30257  wrdt2ind  32643  archirngz  32862  archiabllem2c  32868  sqsscirc1  33432  dya2icoseg  33820  dya2iocucvr  33827  oddpwdc  33897  eulerpartlemgs2  33923  fibp1  33944  signslema  34117  itgexpif  34161  vtsprod  34194  hgt750lemd  34203  logdivsqrle  34205  subfacp1lem1  34712  subfacp1lem5  34717  dnibndlem10  35885  knoppcnlem10  35900  knoppndvlem2  35911  knoppndvlem7  35916  knoppndvlem9  35918  knoppndvlem10  35919  knoppndvlem16  35925  irrdifflemf  36727  itg2addnclem  37066  dvasin  37099  areacirclem1  37103  areacirclem3  37105  isbnd2  37178  lcmineqlem21  41444  3lexlogpow2ineq2  41454  dvrelog2b  41461  dvrelogpow2b  41463  aks4d1p1p4  41466  aks4d1p1p6  41468  aks4d1p1p7  41469  aks4d1p1p5  41470  aks4d1p9  41483  posbezout  41494  2np3bcnp1  41535  2ap1caineq  41536  oddnumth  41783  nicomachus  41784  sumcubes  41785  ef11d  41822  cxpi11d  41826  remul02  41872  remul01  41874  dffltz  41970  fltne  41980  flt4lem5e  41992  cu3addd  42012  rmspecsqrtnq  42238  rmxluc  42269  rmyluc2  42271  rmydbl  42273  jm2.18  42321  jm2.22  42328  jm2.25  42332  jm2.27c  42340  jm3.1lem2  42351  sqrtcval  42984  imo72b2lem0  43508  refsum2cnlem1  44312  oddfl  44572  xralrple2  44649  infleinflem2  44666  sumnnodd  44931  0ellimcdiv  44950  coseq0  45165  sinmulcos  45166  coskpi2  45167  sinaover2ne0  45169  cosknegpi  45170  ioodvbdlimc1lem2  45233  ioodvbdlimc2lem  45235  itgsinexp  45256  stoweidlem1  45302  stoweidlem62  45363  wallispilem4  45369  wallispilem5  45370  wallispi  45371  wallispi2lem1  45372  wallispi2lem2  45373  wallispi2  45374  stirlinglem1  45375  stirlinglem3  45377  stirlinglem4  45378  stirlinglem5  45379  stirlinglem6  45380  stirlinglem7  45381  stirlinglem8  45382  stirlinglem10  45384  stirlinglem11  45385  stirlinglem13  45387  stirlinglem14  45388  stirlinglem15  45389  dirker2re  45393  dirkerdenne0  45394  dirkerval2  45395  dirkerre  45396  dirkertrigeqlem1  45399  dirkertrigeqlem2  45400  dirkertrigeqlem3  45401  dirkertrigeq  45402  dirkeritg  45403  dirkercncflem1  45404  dirkercncflem2  45405  dirkercncflem4  45407  fourierdlem43  45451  fourierdlem44  45452  fourierdlem56  45463  fourierdlem57  45464  fourierdlem58  45465  fourierdlem62  45469  fourierdlem66  45473  fourierdlem68  45475  fourierdlem72  45479  fourierdlem76  45483  fourierdlem79  45486  fourierdlem80  45487  fourierdlem83  45490  fourierdlem95  45502  fourierdlem104  45511  fourierdlem112  45519  fouriercnp  45527  fourierswlem  45531  sge0ad2en  45732  hoicvrrex  45857  hoiqssbllem2  45924  fmtnoodd  46786  sqrtpwpw2p  46791  fmtnorec2lem  46795  fmtnodvds  46797  goldbachthlem2  46799  fmtnoprmfac1lem  46817  fmtnoprmfac2  46820  fmtnofac1  46823  2pwp1prm  46842  mod42tp1mod8  46855  sfprmdvdsmersenne  46856  lighneallem2  46859  lighneallem4  46863  proththd  46867  quad1  46873  requad01  46874  requad1  46875  requad2  46876  dfodd6  46890  dfeven4  46891  enege  46898  onego  46899  dfeven2  46902  oddflALTV  46916  opoeALTV  46936  opeoALTV  46937  nn0onn0exALTV  46952  nn0enn0exALTV  46953  nnennexALTV  46954  mogoldbblem  46973  perfectALTV  46976  fppr2odd  46984  sgoldbeven3prm  47036  0nodd  47145  2nodd  47147  2zlidl  47215  2zrngamgm  47220  2zrngagrp  47224  2zrngmmgm  47227  2zrngnmlid  47230  nn0onn0ex  47509  nn0enn0ex  47510  nnennex  47511  nnpw2even  47515  fldivexpfllog2  47551  blenpw2m1  47565  nnpw2blen  47566  blennn0em1  47577  dig2nn1st  47591  dig2bits  47600  dignn0flhalflem1  47601  dignn0flhalflem2  47602  dignn0ehalf  47603  nn0sumshdiglemA  47605  nn0sumshdiglemB  47606  itcovalt2lem2lem2  47660  ackval2  47668  ackval3  47669  itschlc0yqe  47746  itsclc0yqsollem1  47748  itsclc0yqsol  47750  itsclc0xyqsolr  47755  itsclquadb  47762  2itscplem1  47764  2itscplem3  47766  itscnhlinecirc02plem1  47768