Theorem 1cnd 9935

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 9873	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  1c1 9816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9873

This theorem is referenced by:  adddirp1d  9945  1p1times  10086  addcom  10101  addcomd  10117  muladd11r  10128  pncan1  10333  npcan1  10334  muls1d  10370  mulsubfacd  10371  recrec  10601  rec11  10602  rec11r  10603  rereccl  10622  subrec  10733  nn1m1nn  10917  add1p1  11160  sub1m1  11161  cnm2m1cnm3  11162  xp1d2m1eqxm1d2  11163  div4p1lem1div2  11164  nn0n0n1ge2  11235  zneo  11336  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  lincmb01cmp  12186  iccf1o  12187  xov1plusxeqvd  12189  zpnn0elfzo1  12408  ubmelm1fzo  12430  fzoshftral  12447  fladdz  12488  2tnp1ge0ge0  12492  ltdifltdiv  12497  dfceil2  12502  modvalp1  12551  negmod  12577  modnegd  12587  addmodlteq  12607  binom2sub1  12844  binom3  12847  zesq  12849  sqoddm1div8  12890  bcm1k  12964  bcp1n  12965  bcp1m1  12969  bcpasc  12970  bcn2m1  12973  hashfz  13074  hashfzo  13076  hashfzp1  13078  hashf1lem2  13097  hashf1  13098  brfi1indlem  13133  lswccatn0lsw  13226  swrdccatwrd  13320  revccat  13366  repswrevw  13384  cshwidxm1  13404  cshwidxn  13406  cshweqrep  13418  cshimadifsn0  13427  swrd2lsw  13543  relexpaddnn  13639  absexpz  13893  reccn2  14175  rlimno1  14232  isercolllem1  14243  isercoll2  14247  iseraltlem2  14261  iseraltlem3  14262  hashiun  14395  binomlem  14400  bcxmas  14406  incexc  14408  incexc2  14409  climcndslem1  14420  arisum  14431  arisum2  14432  trireciplem  14433  pwm1geoser  14439  geolim2  14441  georeclim  14442  mertenslem1  14455  prodfrec  14466  ntrivcvg  14468  ntrivcvgtail  14471  prodrblem  14498  prodmolem2a  14503  fprodntriv  14511  prod1  14513  fprodser  14518  fprodcl  14521  fprodm1  14536  fprodp1  14538  risefacval2  14580  fallfacval2  14581  risefacp1  14599  fallfacp1  14600  risefacfac  14605  fallfacfwd  14606  binomfallfaclem2  14610  fallfacval4  14613  bpolydiflem  14624  ef0lem  14648  tanaddlem  14735  tanadd  14736  cos01bnd  14755  oddm1even  14905  oddp1even  14906  oexpneg  14907  ltoddhalfle  14923  halfleoddlt  14924  nn0ob  14938  pwp1fsum  14952  flodddiv4  14975  bitsp1o  14993  bitsf1  15006  sadcp1  15015  qredeu  15210  prmdiv  15328  prmdiveq  15329  vfermltlALT  15345  pcexp  15402  pc2dvds  15421  4sqlem11  15497  4sqlem12  15498  vdwapun  15516  vdwlem3  15525  vdwlem6  15528  vdwlem9  15531  ramub1lem2  15569  prmop1  15580  prmdvdsprmo  15584  prmgaplem8  15600  cshwshashnsame  15648  gsumccat  17201  mulgnnass  17399  mulgnnassOLD  17400  psgnunilem5  17737  psgnunilem2  17738  sylow1lem1  17836  efgredlemc  17981  odadd2  18075  srgbinomlem3  18365  srgbinomlem4  18366  cncrng  19586  cnfldmulg  19597  gzrngunit  19631  zringunit  19655  prmirredlem  19660  cayhamlem1  20490  expcn  22483  iirevcn  22537  iihalf2cn  22541  icchmeo  22548  icopnfcnv  22549  icopnfhmeo  22550  evth  22566  pjthlem1  23016  ovolunlem1a  23071  ovolunlem1  23072  opnmbllem  23175  mbfi1fseqlem6  23293  bddibl  23412  dvnadd  23498  dvmptid  23526  dvcnvlem  23543  dveflem  23546  dvsincos  23548  dvlipcn  23561  dvivthlem1  23575  lhop2  23582  dvcvx  23587  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  ply1divex  23700  fta1glem1  23729  dgrcolem1  23833  dgrcolem2  23834  aaliou3lem2  23902  aaliou3lem8  23904  dvtaylp  23928  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  abelthlem1  23989  abelthlem2  23990  abelthlem6  23994  abelthlem7  23996  logdivlti  24170  advlog  24200  advlogexp  24201  logtayl  24206  cxpmul2  24235  dvcxp1  24281  dvcxp2  24282  dvcncxp1  24284  dvcnsqrt  24285  loglesqrt  24299  relogbdiv  24317  ang180lem4  24342  ang180lem5  24343  isosctrlem2  24349  isosctrlem3  24350  affineequiv  24353  affineequiv2  24354  angpieqvdlem  24355  chordthmlem2  24360  chordthmlem3  24361  chordthmlem5  24363  dcubic2  24371  dcubic  24373  quart1lem  24382  quart1  24383  quart  24388  asinlem  24395  asinlem3  24398  atansopn  24459  dvatan  24462  leibpi  24469  birthdaylem2  24479  efrlim  24496  cxplim  24498  divsqrtsumlem  24506  logdifbnd  24520  emcllem2  24523  emcllem3  24524  emcllem5  24526  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  lgam1  24590  gamfac  24593  wilthimp  24598  ftalem5  24603  basellem3  24609  basellem5  24611  basellem8  24614  basellem9  24615  sqff1o  24708  muinv  24719  logfaclbnd  24747  logfacrlim  24749  logexprlim  24750  perfectlem2  24755  dchr1cl  24776  dchrinvcl  24778  dchrfi  24780  dchr1  24782  dchrsum2  24793  bcmono  24802  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  bposlem9  24817  gausslemma2dlem1a  24890  gausslemma2dlem5  24896  lgseisenlem4  24903  lgsquadlem1  24905  m1lgs  24913  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgslem3d1  24928  2lgsoddprmlem1  24933  2sqlem8  24951  chtppilim  24964  rpvmasumlem  24976  dchrisumlem1  24978  dchrisum0re  25002  dchrisum0lem2a  25006  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  2vmadivsumlem  25029  selberg4lem1  25049  pntrsumo1  25054  selberg34r  25060  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntibndlem2  25080  pntlemg  25087  pntlemr  25091  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlem3  25098  ostth2lem2  25123  ttgcontlem1  25565  cusgrasizeinds  26004  cusgrasize2inds  26005  wlkdvspthlem  26137  fargshiftf1  26165  fargshiftfo  26166  wwlknimp  26215  wlklniswwlkn2  26228  wwlknred  26251  wwlknextbi  26253  wwlknredwwlkn  26254  wwlkextwrd  26256  wwlkextinj  26258  wwlkextproplem2  26270  wwlkextproplem3  26271  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlklem0  26316  clwlkisclwwlk  26317  clwwlkel  26321  clwwlkf  26322  clwwlkext2edg  26330  clwwisshclwwlem1  26333  clwwisshclww  26335  wlklenvclwlk  26366  nbhashuvtx1  26442  rusgra0edg  26482  eupatrl  26495  frghash2spot  26590  frgregordn0  26597  extwwlkfablem1  26601  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  smcnlem  26936  bcm1n  28941  ltesubnnd  28955  omndmul2  29043  archirngz  29074  archiabllem1a  29076  archiabllem2c  29080  psgnfzto1stlem  29181  1smat1  29198  madjusmdetlem2  29222  madjusmdetlem4  29224  dya2icoseg  29666  iwrdsplit  29776  fibp1  29790  ballotlemfp1  29880  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemic  29895  ballotlem1c  29896  ballotlemsgt1  29899  ballotlemsdom  29900  ballotlemsel1i  29901  ballotlemsi  29903  ballotlemsima  29904  ballotlem1ri  29923  sgn0bi  29936  signstfvn  29972  signsvtn0  29973  signstfveq0  29980  signsvfn  29985  signsvtn  29987  signshf  29991  subfacp1lem1  30415  subfacp1lem5  30420  cvxpcon  30478  sinccvglem  30820  divcnvlin  30871  bcm1nt  30876  bcprod  30877  bccolsum  30878  iprodgam  30881  faclimlem1  30882  faclimlem2  30883  faclimlem3  30884  faclim  30885  iprodfac  30886  faclim2  30887  fwddifnp1  31442  dnizphlfeqhlf  31636  dnibndlem3  31640  dnibndlem13  31650  unblimceq0  31668  knoppndvlem6  31678  knoppndvlem9  31681  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem16  31688  knoppndvlem17  31689  bj-bary1lem1  32338  poimirlem25  32604  poimirlem26  32605  poimirlem32  32611  opnmbllem0  32615  itg2addnclem2  32632  dvasin  32666  dvacos  32667  areacirclem1  32670  areacirclem4  32673  areacirc  32675  bfp  32793  pell1qrge1  36452  rmspecfund  36492  acongeq  36568  jm2.18  36573  jm2.19lem3  36576  jm2.25  36584  jm2.16nn0  36589  jm3.1lem1  36602  jm3.1lem2  36603  itgpowd  36819  areaquad  36821  relexpmulnn  37020  relexpaddss  37029  cvgdvgrat  37534  radcnvrat  37535  hashnzfzclim  37543  ofdivrec  37547  expgrowthi  37554  bccm1k  37563  dvradcnv2  37568  binomcxplemwb  37569  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemfrat  37572  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  refsum2cnlem1  38219  fzisoeu  38455  fperiodmullem  38458  fzdifsuc2  38466  xralrple2  38511  nnsplit  38515  infleinflem2  38528  fmul01lt1lem2  38652  fprodcn  38667  clim1fr1  38668  isumneg  38669  climneg  38677  sumnnodd  38697  reclimc  38720  coseq0  38747  coskpi2  38749  cosknegpi  38752  fprodcncf  38787  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvmptdiv  38807  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  dvnmul  38833  dvmptfprod  38835  dvnprodlem3  38838  itgsinexp  38846  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem1  38894  stoweidlem7  38900  stoweidlem10  38903  stoweidlem11  38904  stoweidlem14  38907  stoweidlem17  38910  stoweidlem34  38927  stoweidlem42  38935  wallispilem3  38960  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem15  38981  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem11  39011  fourierdlem15  39015  fourierdlem26  39026  fourierdlem36  39036  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem56  39055  fourierdlem58  39057  fourierdlem59  39058  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem78  39077  fourierdlem79  39078  sqwvfoura  39121  fourierswlem  39123  fouriersw  39124  etransclem23  39150  etransclem24  39151  etransclem28  39155  etransclem35  39162  etransclem38  39165  nnfoctbdjlem  39348  smfmullem1  39676  sigaradd  39704  deccarry  39941  fmtnof1  39985  sqrtpwpw2p  39988  fmtnorec2lem  39992  fmtnorec4  39999  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnoprmfac2  40017  pwdif  40039  pwm1geoserALT  40040  2pwp1prm  40041  mod42tp1mod8  40057  sfprmdvdsmersenne  40058  lighneallem3  40062  lighneallem4  40065  onego  40097  zofldiv2ALTV  40112  oexpnegALTV  40126  opoeALTV  40132  opeoALTV  40133  epee  40152  perfectALTVlem1  40164  fzosplitpr  40362  cusgrsize2inds  40669  1wlklenvclwlk  40863  pthdadjvtx  40936  crctcsh1wlkn0lem1  41013  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  1wlklnwwlkln2lem  41079  wwlksnred  41098  wwlksnextbi  41100  wwlksnredwwlkn  41101  wwlksnextwrd  41103  wwlksnextinj  41105  wwlksnextproplem2  41116  wwlksnextproplem3  41117  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlklem3  41210  clwlkclwwlk  41211  clwwlksel  41221  clwwlksf  41222  clwwlksext2edg  41230  wwlksext2clwwlk  41231  clwwisshclwwslemlem  41233  clwwisshclwws  41235  eucrct2eupth  41413  frgrhash2wsp  41497  fusgreghash2wspv  41499  frrusgrord0  41503  av-extwwlkfablem1  41508  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-numclwwlk6  41544  0nodd  41600  2nodd  41602  nnsgrpnmnd  41608  1neven  41722  altgsumbc  41923  pw2m1lepw2m1  42104  m1modmmod  42110  zofldiv2  42119  nnpw2pmod  42175  blen1b  42180  blennn0em1  42183  dignn0flhalflem1  42207  dignn0flhalflem2  42208  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  nn0sumshdiglem2  42214