Theorem 2cnd 11716

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  2c2 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-2 11701

This theorem is referenced by:  subhalfhalf  11872  cnm2m1cnm3  11891  xp1d2m1eqxm1d2  11892  zeo2  12070  fzosplitprm1  13148  2tnp1ge0ge0  13200  flhalf  13201  2txmodxeq0  13300  mulbinom2  13585  binom3  13586  zesq  13588  expmulnbnd  13597  discr  13602  sqoddm1div8  13605  mulsubdivbinom2  13623  swrds2m  14303  amgm2  14729  bhmafibid1cn  14823  bhmafibid2cn  14824  iseraltlem2  15039  iseralt  15041  trirecip  15218  geo2sum  15229  bpolydiflem  15408  ege2le3  15443  tanval3  15487  sinhval  15507  tanhlt1  15513  sqrt2irrlem  15601  sqrt2irr  15602  even2n  15691  oddm1even  15692  oddp1even  15693  mod2eq1n2dvds  15696  ltoddhalfle  15710  m1exp1  15727  nn0enne  15728  flodddiv4  15764  flodddiv4t2lthalf  15767  bitsp1e  15781  bitsp1o  15782  bitsfzo  15784  bitsmod  15785  bitsinv1lem  15790  sadadd2lem2  15799  sadcaddlem  15806  bitsuz  15823  bitsshft  15824  prmdiv  16122  vfermltlALT  16139  iserodd  16172  4sqlem7  16280  4sqlem10  16283  4sqlem19  16299  prmgaplem7  16393  2expltfac  16426  smndex2dlinvh  18082  efgredlemg  18868  frgpnabllem1  18993  ablsimpgfindlem1  19229  metnrmlem3  23469  iihalf1cn  23536  iihalf2cn  23538  pcoass  23628  cphipval2  23844  csbren  24002  trirn  24003  minveclem2  24029  ovolunlem1a  24097  uniioombllem5  24188  uniioombl  24190  dyaddisjlem  24196  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  dvsincos  24578  lhop1  24611  cosargd  25191  dvcnsqrt  25325  root1id  25335  ssscongptld  25400  chordthmlem  25410  chordthmlem2  25411  chordthmlem4  25413  heron  25416  dcubic1  25423  mcubic  25425  cubic2  25426  quartlem4  25438  quart  25439  cosasin  25482  cosatan  25499  atantayl  25515  atantayl2  25516  atantayl3  25517  log2tlbnd  25523  cxp2limlem  25553  divsqrtsumlem  25557  lgamgulmlem2  25607  lgamgulmlem4  25609  lgamucov  25615  ftalem2  25651  basellem2  25659  basellem3  25660  basellem5  25662  basellem8  25665  logfaclbnd  25798  perfectlem2  25806  perfect  25807  bcp1ctr  25855  bposlem1  25860  bposlem2  25861  lgslem1  25873  lgsqrlem2  25923  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  gausslemma2dlem4  25945  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem1  25960  2lgslem1a1  25965  2lgslem1a2  25966  2lgslem1b  25968  2lgslem1c  25969  2lgslem3a1  25976  2lgslem3d1  25979  2sq2  26009  addsq2nreurex  26020  chebbnd1lem3  26047  chto1ub  26052  dchrisumlem2  26066  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2  26094  logdivsum  26109  mulog2sumlem2  26111  vmalogdivsum2  26114  log2sumbnd  26120  selberglem2  26122  chpdifbndlem1  26129  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  selberg4r  26146  selberg34r  26147  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  pntlemk  26182  pntlemo  26183  ostth2lem1  26194  finsumvtxdg2ssteplem4  27330  upgrwlkdvdelem  27517  wwlksnextwrd  27675  wwlksnextinj  27677  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem3  27779  clwwlkext2edg  27835  clwwlknonex2lem1  27886  clwwlknonex2lem2  27887  2clwwlk2clwwlk  28129  numclwwlk1lem2foalem  28130  numclwwlk1lem2fo  28137  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwwlk2  28160  ex-ind-dvds  28240  wrdt2ind  30627  archirngz  30818  archiabllem2c  30824  sqsscirc1  31151  dya2icoseg  31535  dya2iocucvr  31542  oddpwdc  31612  eulerpartlemgs2  31638  fibp1  31659  signslema  31832  itgexpif  31877  vtsprod  31910  hgt750lemd  31919  logdivsqrle  31921  subfacp1lem1  32426  subfacp1lem5  32431  dnibndlem10  33826  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem9  33859  knoppndvlem10  33860  knoppndvlem16  33866  itg2addnclem  34958  dvasin  34993  areacirclem1  34997  areacirclem3  34999  isbnd2  35076  remul02  39255  remul01  39257  dffltz  39291  fltne  39292  cu3addd  39297  rmspecsqrtnq  39523  rmxluc  39553  rmyluc2  39555  rmydbl  39557  jm2.18  39605  jm2.22  39612  jm2.25  39616  jm2.27c  39624  jm3.1lem2  39635  imo72b2lem0  40536  refsum2cnlem1  41314  oddfl  41563  xralrple2  41642  infleinflem2  41659  sumnnodd  41931  0ellimcdiv  41950  coseq0  42165  sinmulcos  42166  coskpi2  42167  sinaover2ne0  42169  cosknegpi  42170  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  itgsinexp  42260  stoweidlem1  42306  stoweidlem62  42367  wallispilem4  42373  wallispilem5  42374  wallispi  42375  wallispi2lem1  42376  wallispi2lem2  42377  wallispi2  42378  stirlinglem1  42379  stirlinglem3  42381  stirlinglem4  42382  stirlinglem5  42383  stirlinglem6  42384  stirlinglem7  42385  stirlinglem8  42386  stirlinglem10  42388  stirlinglem11  42389  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  dirker2re  42397  dirkerdenne0  42398  dirkerval2  42399  dirkerre  42400  dirkertrigeqlem1  42403  dirkertrigeqlem2  42404  dirkertrigeqlem3  42405  dirkertrigeq  42406  dirkeritg  42407  dirkercncflem1  42408  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem43  42455  fourierdlem44  42456  fourierdlem56  42467  fourierdlem57  42468  fourierdlem58  42469  fourierdlem62  42473  fourierdlem66  42477  fourierdlem68  42479  fourierdlem72  42483  fourierdlem76  42487  fourierdlem79  42490  fourierdlem80  42491  fourierdlem83  42494  fourierdlem95  42506  fourierdlem104  42515  fourierdlem112  42523  fouriercnp  42531  fourierswlem  42535  sge0ad2en  42733  hoicvrrex  42858  hoiqssbllem2  42925  fmtnoodd  43715  sqrtpwpw2p  43720  fmtnorec2lem  43724  fmtnodvds  43726  goldbachthlem2  43728  fmtnoprmfac1lem  43746  fmtnoprmfac2  43749  fmtnofac1  43752  2pwp1prm  43771  mod42tp1mod8  43787  sfprmdvdsmersenne  43788  lighneallem2  43791  lighneallem4  43795  proththd  43799  quad1  43805  requad01  43806  requad1  43807  requad2  43808  dfodd6  43822  dfeven4  43823  enege  43830  onego  43831  dfeven2  43834  oddflALTV  43848  opoeALTV  43868  opeoALTV  43869  nn0onn0exALTV  43884  nn0enn0exALTV  43885  nnennexALTV  43886  mogoldbblem  43905  perfectALTV  43908  fppr2odd  43916  sgoldbeven3prm  43968  0nodd  44097  2nodd  44099  2zlidl  44225  2zrngamgm  44230  2zrngagrp  44234  2zrngmmgm  44237  2zrngnmlid  44240  nn0onn0ex  44603  nn0enn0ex  44604  nnennex  44605  nnpw2even  44609  fldivexpfllog2  44645  blenpw2m1  44659  nnpw2blen  44660  blennn0em1  44671  dig2nn1st  44685  dig2bits  44694  dignn0flhalflem1  44695  dignn0flhalflem2  44696  dignn0ehalf  44697  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700  itschlc0yqe  44767  itsclc0yqsollem1  44769  itsclc0yqsol  44771  itsclc0xyqsolr  44776  itsclquadb  44783  2itscplem1  44785  2itscplem3  44787  itscnhlinecirc02plem1  44789