Theorem 2cnd 12344

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  2c2 12321

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329

This theorem is referenced by:  subhalfhalf  12500  cnm2m1cnm3  12519  xp1d2m1eqxm1d2  12520  zeo2  12705  ge2halflem1  13150  fzosplitprm1  13816  2tnp1ge0ge0  13869  flhalf  13870  2txmodxeq0  13972  mulbinom2  14262  binom3  14263  zesq  14265  expmulnbnd  14274  discr  14279  sqoddm1div8  14282  mulsubdivbinom2  14301  swrds2m  14980  amgm2  15408  bhmafibid1cn  15502  bhmafibid2cn  15503  iseraltlem2  15719  iseralt  15721  trirecip  15899  geo2sum  15909  bpolydiflem  16090  ege2le3  16126  tanval3  16170  sinhval  16190  tanhlt1  16196  sqrt2irrlem  16284  sqrt2irr  16285  even2n  16379  oddm1even  16380  oddp1even  16381  mod2eq1n2dvds  16384  ltoddhalfle  16398  m1exp1  16413  nn0enne  16414  flodddiv4  16452  flodddiv4t2lthalf  16455  bitsp1e  16469  bitsp1o  16470  bitsfzo  16472  bitsmod  16473  bitsinv1lem  16478  sadadd2lem2  16487  sadcaddlem  16494  bitsuz  16511  bitsshft  16512  prmdiv  16822  vfermltlALT  16840  iserodd  16873  4sqlem7  16982  4sqlem10  16985  4sqlem19  17001  prmgaplem7  17095  2expltfac  17130  smndex2dlinvh  18930  efgredlemg  19760  frgpnabllem1  19891  ablsimpgfindlem1  20127  metnrmlem3  24883  iihalf1cn  24959  iihalf1cnOLD  24960  iihalf2cn  24962  iihalf2cnOLD  24963  pcoass  25057  cphipval2  25275  csbren  25433  trirn  25434  minveclem2  25460  ovolunlem1a  25531  uniioombllem5  25622  uniioombl  25624  dyaddisjlem  25630  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  dvsincos  26019  lhop1  26053  cosargd  26650  dvcnsqrt  26786  root1id  26797  ssscongptld  26865  chordthmlem  26875  chordthmlem2  26876  chordthmlem4  26878  heron  26881  dcubic1  26888  mcubic  26890  cubic2  26891  quartlem4  26903  quart  26904  cosasin  26947  cosatan  26964  atantayl  26980  atantayl2  26981  atantayl3  26982  log2tlbnd  26988  cxp2limlem  27019  divsqrtsumlem  27023  lgamgulmlem2  27073  lgamgulmlem4  27075  lgamucov  27081  ftalem2  27117  basellem2  27125  basellem3  27126  basellem5  27128  basellem8  27131  logfaclbnd  27266  perfectlem2  27274  perfect  27275  bcp1ctr  27323  bposlem1  27328  bposlem2  27329  lgslem1  27341  lgsqrlem2  27391  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  gausslemma2dlem4  27413  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem1  27428  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1b  27436  2lgslem1c  27437  2lgslem3a1  27444  2lgslem3d1  27447  2sq2  27477  addsq2nreurex  27488  chebbnd1lem3  27515  chto1ub  27520  dchrisumlem2  27534  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2  27562  logdivsum  27577  mulog2sumlem2  27579  vmalogdivsum2  27582  log2sumbnd  27588  selberglem2  27590  chpdifbndlem1  27597  selberg3lem1  27601  selberg3  27603  selberg4lem1  27604  selberg4  27605  selberg4r  27614  selberg34r  27615  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem2  27635  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemr  27646  pntlemk  27650  pntlemo  27651  ostth2lem1  27662  finsumvtxdg2ssteplem4  29566  upgrwlkdvdelem  29756  wwlksnextwrd  29917  wwlksnextinj  29919  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a4  30016  clwlkclwwlklem3  30020  clwwlkext2edg  30075  clwwlknonex2lem1  30126  clwwlknonex2lem2  30127  2clwwlk2clwwlk  30369  numclwwlk1lem2foalem  30370  numclwwlk1lem2fo  30377  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwwlk2  30400  ex-ind-dvds  30480  nrt2irr  30492  quad3d  32754  2exple2exp  32834  wrdt2ind  32938  archirngz  33196  archiabllem2c  33202  fldext2rspun  33732  constrrtcc  33776  constrelextdg2  33788  sqsscirc1  33907  dya2icoseg  34279  dya2iocucvr  34286  oddpwdc  34356  eulerpartlemgs2  34382  fibp1  34403  signslema  34577  itgexpif  34621  vtsprod  34654  hgt750lemd  34663  logdivsqrle  34665  subfacp1lem1  35184  subfacp1lem5  35189  dnibndlem10  36488  knoppcnlem10  36503  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem9  36521  knoppndvlem10  36522  knoppndvlem16  36528  irrdifflemf  37326  itg2addnclem  37678  dvasin  37711  areacirclem1  37715  areacirclem3  37717  isbnd2  37790  lcmineqlem21  42050  3lexlogpow2ineq2  42060  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p9  42089  posbezout  42101  2np3bcnp1  42145  2ap1caineq  42146  oddnumth  42345  nicomachus  42346  sumcubes  42347  ef11d  42375  cxpi11d  42379  tan3rdpi  42386  readvrec2  42391  remul02  42435  remul01  42437  dffltz  42644  fltne  42654  flt4lem5e  42666  cu3addd  42691  rmspecsqrtnq  42917  rmxluc  42948  rmyluc2  42950  rmydbl  42952  jm2.18  43000  jm2.22  43007  jm2.25  43011  jm2.27c  43019  jm3.1lem2  43030  sqrtcval  43654  imo72b2lem0  44178  refsum2cnlem1  45042  oddfl  45289  xralrple2  45365  infleinflem2  45382  sumnnodd  45645  0ellimcdiv  45664  coseq0  45879  sinmulcos  45880  coskpi2  45881  sinaover2ne0  45883  cosknegpi  45884  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  itgsinexp  45970  stoweidlem1  46016  stoweidlem62  46077  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  dirker2re  46107  dirkerdenne0  46108  dirkerval2  46109  dirkerre  46110  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkeritg  46117  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem43  46165  fourierdlem44  46166  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem66  46187  fourierdlem68  46189  fourierdlem72  46193  fourierdlem76  46197  fourierdlem79  46200  fourierdlem80  46201  fourierdlem83  46204  fourierdlem95  46216  fourierdlem104  46225  fourierdlem112  46233  fouriercnp  46241  fourierswlem  46245  sge0ad2en  46446  hoicvrrex  46571  hoiqssbllem2  46638  minusmodnep2tmod  47355  fmtnoodd  47520  sqrtpwpw2p  47525  fmtnorec2lem  47529  fmtnodvds  47531  goldbachthlem2  47533  fmtnoprmfac1lem  47551  fmtnoprmfac2  47554  fmtnofac1  47557  2pwp1prm  47576  mod42tp1mod8  47589  sfprmdvdsmersenne  47590  lighneallem2  47593  lighneallem4  47597  proththd  47601  quad1  47607  requad01  47608  requad1  47609  requad2  47610  dfodd6  47624  dfeven4  47625  enege  47632  onego  47633  dfeven2  47636  oddflALTV  47650  opoeALTV  47670  opeoALTV  47671  nn0onn0exALTV  47686  nn0enn0exALTV  47687  nnennexALTV  47688  mogoldbblem  47707  perfectALTV  47710  fppr2odd  47718  sgoldbeven3prm  47770  2tceilhalfelfzo1  48018  gpg3nbgrvtx0  48032  gpg3kgrtriexlem2  48040  0nodd  48086  2nodd  48088  2zlidl  48156  2zrngamgm  48161  2zrngagrp  48165  2zrngmmgm  48168  2zrngnmlid  48171  nn0onn0ex  48444  nn0enn0ex  48445  nnennex  48446  nnpw2even  48450  fldivexpfllog2  48486  blenpw2m1  48500  nnpw2blen  48501  blennn0em1  48512  dig2nn1st  48526  dig2bits  48535  dignn0flhalflem1  48536  dignn0flhalflem2  48537  dignn0ehalf  48538  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  itcovalt2lem2lem2  48595  ackval2  48603  ackval3  48604  itschlc0yqe  48681  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itsclc0xyqsolr  48690  itsclquadb  48697  2itscplem1  48699  2itscplem3  48701  itscnhlinecirc02plem1  48703