MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1cnd Structured version   Visualization version   GIF version

Theorem 1cnd 9913
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
StepHypRef Expression
1 ax-1cn 9851 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9791  1c1 9794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9851
This theorem is referenced by:  adddirp1d  9923  1p1times  10059  addcom  10074  addcomd  10090  muladd11r  10101  pncan1  10306  npcan1  10307  muls1d  10343  mulsubfacd  10344  recrec  10574  rec11  10575  rec11r  10576  rereccl  10595  subrec  10706  nn1m1nn  10890  add1p1  11133  sub1m1  11134  cnm2m1cnm3  11135  xp1d2m1eqxm1d2  11136  div4p1lem1div2  11137  nn0n0n1ge2  11208  zneo  11295  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  lincmb01cmp  12145  iccf1o  12146  xov1plusxeqvd  12148  zpnn0elfzo1  12366  ubmelm1fzo  12388  fzoshftral  12405  fladdz  12446  2tnp1ge0ge0  12450  ltdifltdiv  12455  dfceil2  12460  modvalp1  12509  negmod  12535  modnegd  12545  addmodlteq  12565  binom2sub1  12802  binom3  12805  zesq  12807  sqoddm1div8  12848  bcm1k  12922  bcp1n  12923  bcp1m1  12927  bcpasc  12928  bcn2m1  12931  hashfz  13029  hashfzo  13031  hashfzp1  13033  hashf1lem2  13052  hashf1  13053  brfi1indlem  13082  lswccatn0lsw  13175  swrdccatwrd  13269  revccat  13315  repswrevw  13333  cshwidxm1  13353  cshwidxn  13355  cshweqrep  13367  cshimadifsn0  13376  swrd2lsw  13492  relexpaddnn  13588  absexpz  13842  reccn2  14124  rlimno1  14181  isercolllem1  14192  isercoll2  14196  iseraltlem2  14210  iseraltlem3  14211  hashiun  14344  binomlem  14349  bcxmas  14355  incexc  14357  incexc2  14358  climcndslem1  14369  arisum  14380  arisum2  14381  trireciplem  14382  pwm1geoser  14388  geolim2  14390  georeclim  14391  mertenslem1  14404  prodfrec  14415  ntrivcvg  14417  ntrivcvgtail  14420  prodrblem  14447  prodmolem2a  14452  fprodntriv  14460  prod1  14462  fprodser  14467  fprodcl  14470  fprodm1  14485  fprodp1  14487  risefacval2  14529  fallfacval2  14530  risefacp1  14548  fallfacp1  14549  risefacfac  14554  fallfacfwd  14555  binomfallfaclem2  14559  fallfacval4  14562  bpolydiflem  14573  ef0lem  14597  tanaddlem  14684  tanadd  14685  cos01bnd  14704  oddm1even  14854  oddp1even  14855  oexpneg  14856  ltoddhalfle  14872  halfleoddlt  14873  nn0ob  14887  pwp1fsum  14901  flodddiv4  14924  bitsp1o  14942  bitsf1  14955  sadcp1  14964  qredeu  15159  prmdiv  15277  prmdiveq  15278  vfermltlALT  15294  pcexp  15351  pc2dvds  15370  4sqlem11  15446  4sqlem12  15447  vdwapun  15465  vdwlem3  15474  vdwlem6  15477  vdwlem9  15480  ramub1lem2  15518  prmop1  15529  prmdvdsprmo  15533  prmgaplem8  15549  cshwshashnsame  15597  gsumccat  17150  mulgnnass  17348  mulgnnassOLD  17349  psgnunilem5  17686  psgnunilem2  17687  sylow1lem1  17785  efgredlemc  17930  odadd2  18024  srgbinomlem3  18314  srgbinomlem4  18315  cncrng  19535  cnfldmulg  19546  gzrngunit  19580  zringunit  19606  prmirredlem  19608  cayhamlem1  20438  expcn  22431  iirevcn  22485  iihalf2cn  22489  icchmeo  22496  icopnfcnv  22497  icopnfhmeo  22498  evth  22514  pjthlem1  22961  ovolunlem1a  23016  ovolunlem1  23017  opnmbllem  23120  mbfi1fseqlem6  23238  bddibl  23357  dvnadd  23443  dvmptid  23471  dvcnvlem  23488  dveflem  23491  dvsincos  23493  dvlipcn  23506  dvivthlem1  23520  lhop2  23527  dvcvx  23532  dvfsumle  23533  dvfsumabs  23535  dvfsumlem1  23538  dvfsumlem2  23539  ply1divex  23645  fta1glem1  23674  dgrcolem1  23778  dgrcolem2  23779  aaliou3lem2  23847  aaliou3lem8  23849  dvtaylp  23873  dvntaylp  23874  taylthlem1  23876  taylthlem2  23877  abelthlem1  23934  abelthlem2  23935  abelthlem6  23939  abelthlem7  23941  logdivlti  24115  advlog  24145  advlogexp  24146  logtayl  24151  cxpmul2  24180  dvcxp1  24226  dvcxp2  24227  dvcncxp1  24229  dvcnsqrt  24230  loglesqrt  24244  relogbdiv  24262  ang180lem4  24287  ang180lem5  24288  isosctrlem2  24294  isosctrlem3  24295  affineequiv  24298  affineequiv2  24299  angpieqvdlem  24300  chordthmlem2  24305  chordthmlem3  24306  chordthmlem5  24308  dcubic2  24316  dcubic  24318  quart1lem  24327  quart1  24328  quart  24333  asinlem  24340  asinlem3  24343  atansopn  24404  dvatan  24407  leibpi  24414  birthdaylem2  24424  efrlim  24441  cxplim  24443  divsqrtsumlem  24451  logdifbnd  24465  emcllem2  24468  emcllem3  24469  emcllem5  24471  zetacvg  24486  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamgulmlem4  24503  lgamgulmlem5  24504  lgamgulmlem6  24505  lgamgulm2  24507  lgamcvg2  24526  gamcvg  24527  gamcvg2lem  24530  lgam1  24535  gamfac  24538  wilthimp  24543  ftalem5  24548  basellem3  24554  basellem5  24556  basellem8  24559  basellem9  24560  sqff1o  24653  muinv  24664  logfaclbnd  24692  logfacrlim  24694  logexprlim  24695  perfectlem2  24700  dchr1cl  24721  dchrinvcl  24723  dchrfi  24725  dchr1  24727  dchrsum2  24738  bcmono  24747  bcp1ctr  24749  bclbnd  24750  bposlem1  24754  bposlem9  24762  gausslemma2dlem1a  24835  gausslemma2dlem5  24841  lgseisenlem4  24848  lgsquadlem1  24850  m1lgs  24858  2lgslem3a  24866  2lgslem3b  24867  2lgslem3c  24868  2lgslem3d  24869  2lgslem3d1  24873  2lgsoddprmlem1  24878  2sqlem8  24896  chtppilim  24909  rpvmasumlem  24921  dchrisumlem1  24923  dchrisum0re  24947  dchrisum0lem2a  24951  mudivsum  24964  mulogsumlem  24965  mulogsum  24966  2vmadivsumlem  24974  selberg4lem1  24994  pntrsumo1  24999  selberg34r  25005  pntrlog2bndlem2  25012  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntibndlem2  25025  pntlemg  25032  pntlemr  25036  pntlemf  25039  pntlemk  25040  pntlemo  25041  pntlem3  25043  ostth2lem2  25068  ttgcontlem1  25511  cusgrasizeinds  25798  cusgrasize2inds  25799  wlkdvspthlem  25931  fargshiftf1  25959  fargshiftfo  25960  wwlknimp  26009  wlklniswwlkn2  26022  wwlknred  26045  wwlknextbi  26047  wwlknredwwlkn  26048  wwlkextwrd  26050  wwlkextinj  26052  wwlkextproplem2  26064  wwlkextproplem3  26065  clwlkisclwwlklem2a1  26101  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  clwlkisclwwlklem1  26109  clwlkisclwwlklem0  26110  clwlkisclwwlk  26111  clwwlkel  26115  clwwlkf  26116  clwwlkext2edg  26124  clwwisshclwwlem1  26127  clwwisshclww  26129  wlklenvclwlk  26160  nbhashuvtx1  26236  rusgra0edg  26276  eupatrl  26289  frghash2spot  26384  frgregordn0  26391  extwwlkfablem1  26395  extwwlkfablem2  26399  numclwwlkovf2ex  26407  numclwlk1lem2foa  26412  numclwlk1lem2fo  26416  numclwlk2lem2f  26424  numclwlk2lem2f1o  26426  smcnlem  26765  bcm1n  28775  ltesubnnd  28789  omndmul2  28877  archirngz  28908  archiabllem1a  28910  archiabllem2c  28914  psgnfzto1stlem  29015  1smat1  29032  madjusmdetlem2  29056  madjusmdetlem4  29058  dya2icoseg  29500  iwrdsplit  29610  fibp1  29624  ballotlemfp1  29714  ballotlemfc0  29715  ballotlemfcc  29716  ballotlemic  29729  ballotlem1c  29730  ballotlemsgt1  29733  ballotlemsdom  29734  ballotlemsel1i  29735  ballotlemsi  29737  ballotlemsima  29738  ballotlem1ri  29757  sgn0bi  29770  signstfvn  29806  signsvtn0  29807  signstfveq0  29814  signsvfn  29819  signsvtn  29821  signshf  29825  subfacp1lem1  30249  subfacp1lem5  30254  cvxpcon  30312  sinccvglem  30654  divcnvlin  30705  bcm1nt  30710  bcprod  30711  bccolsum  30712  iprodgam  30715  faclimlem1  30716  faclimlem2  30717  faclimlem3  30718  faclim  30719  iprodfac  30720  faclim2  30721  fwddifnp1  31276  dnizphlfeqhlf  31470  dnibndlem3  31474  dnibndlem13  31484  unblimceq0  31502  knoppndvlem6  31512  knoppndvlem9  31515  knoppndvlem14  31520  knoppndvlem15  31521  knoppndvlem16  31522  knoppndvlem17  31523  bj-bary1lem1  32162  poimirlem25  32428  poimirlem26  32429  poimirlem32  32435  opnmbllem0  32439  itg2addnclem2  32456  dvasin  32490  dvacos  32491  areacirclem1  32494  areacirclem4  32497  areacirc  32499  bfp  32617  pell1qrge1  36276  rmspecfund  36316  acongeq  36392  jm2.18  36397  jm2.19lem3  36400  jm2.25  36408  jm2.16nn0  36413  jm3.1lem1  36426  jm3.1lem2  36427  itgpowd  36643  areaquad  36645  relexpmulnn  36844  relexpaddss  36853  cvgdvgrat  37358  radcnvrat  37359  hashnzfzclim  37367  ofdivrec  37371  expgrowthi  37378  bccm1k  37387  dvradcnv2  37392  binomcxplemwb  37393  binomcxplemnn0  37394  binomcxplemrat  37395  binomcxplemfrat  37396  binomcxplemdvbinom  37398  binomcxplemnotnn0  37401  refsum2cnlem1  38043  fzisoeu  38279  fperiodmullem  38282  fzdifsuc2  38290  xralrple2  38335  nnsplit  38339  infleinflem2  38352  fmul01lt1lem2  38476  fprodcn  38491  clim1fr1  38492  isumneg  38493  climneg  38501  sumnnodd  38521  reclimc  38544  coseq0  38571  coskpi2  38573  cosknegpi  38576  fprodcncf  38611  fprodsubrecnncnvlem  38618  fprodaddrecnncnvlem  38620  dvmptdiv  38631  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnxpaek  38656  dvnmul  38657  dvmptfprod  38659  dvnprodlem3  38662  itgsinexp  38670  itgiccshift  38696  itgperiod  38697  itgsbtaddcnst  38698  stoweidlem1  38718  stoweidlem7  38724  stoweidlem10  38727  stoweidlem11  38728  stoweidlem14  38731  stoweidlem17  38734  stoweidlem34  38751  stoweidlem42  38759  wallispilem3  38784  wallispilem5  38786  wallispi  38787  wallispi2lem1  38788  wallispi2lem2  38789  wallispi2  38790  stirlinglem1  38791  stirlinglem3  38793  stirlinglem4  38794  stirlinglem5  38795  stirlinglem6  38796  stirlinglem7  38797  stirlinglem8  38798  stirlinglem10  38800  stirlinglem11  38801  stirlinglem12  38802  stirlinglem13  38803  stirlinglem15  38805  dirkertrigeqlem2  38816  dirkertrigeqlem3  38817  dirkertrigeq  38818  dirkercncflem1  38820  dirkercncflem2  38821  dirkercncflem4  38823  fourierdlem11  38835  fourierdlem15  38839  fourierdlem26  38850  fourierdlem36  38860  fourierdlem40  38864  fourierdlem41  38865  fourierdlem42  38866  fourierdlem48  38871  fourierdlem49  38872  fourierdlem56  38879  fourierdlem58  38881  fourierdlem59  38882  fourierdlem62  38885  fourierdlem64  38887  fourierdlem65  38888  fourierdlem78  38901  fourierdlem79  38902  sqwvfoura  38945  fourierswlem  38947  fouriersw  38948  etransclem23  38974  etransclem24  38975  etransclem28  38979  etransclem35  38986  etransclem38  38989  nnfoctbdjlem  39172  smfmullem1  39500  sigaradd  39528  deccarry  39766  fmtnof1  39810  sqrtpwpw2p  39813  fmtnorec2lem  39817  fmtnorec4  39824  fmtnoprmfac1lem  39839  fmtnoprmfac1  39840  fmtnoprmfac2  39842  pwdif  39864  pwm1geoserALT  39865  2pwp1prm  39866  mod42tp1mod8  39882  sfprmdvdsmersenne  39883  lighneallem3  39887  lighneallem4  39890  onego  39922  zofldiv2ALTV  39937  oexpnegALTV  39951  opoeALTV  39957  opeoALTV  39958  epee  39977  perfectALTVlem1  39989  fzosplitpr  40209  cusgrsize2inds  40691  1wlklenvclwlk  40885  pthdadjvtx  40958  crctcsh1wlkn0lem1  41035  crctcsh1wlkn0lem4  41038  crctcsh1wlkn0lem5  41039  1wlklnwwlkln2lem  41101  wwlksnred  41120  wwlksnextbi  41122  wwlksnredwwlkn  41123  wwlksnextwrd  41125  wwlksnextinj  41127  wwlksnextproplem2  41138  wwlksnextproplem3  41139  clwlkclwwlklem2a1  41223  clwlkclwwlklem2a4  41228  clwlkclwwlklem2a  41229  clwlkclwwlklem2  41231  clwlkclwwlklem3  41232  clwlkclwwlk  41233  clwwlksel  41243  clwwlksf  41244  clwwlksext2edg  41252  wwlksext2clwwlk  41253  clwwisshclwwslemlem  41255  clwwisshclwws  41257  eucrct2eupth  41435  frgrhash2wsp  41519  fusgreghash2wspv  41521  frrusgrord0  41525  av-extwwlkfablem1  41530  av-extwwlkfablem2  41532  av-numclwwlkovf2ex  41539  av-numclwlk1lem2foa  41543  av-numclwlk1lem2fo  41547  av-numclwlk2lem2f  41555  av-numclwlk2lem2f1o  41557  av-numclwwlk6  41566  0nodd  41622  2nodd  41624  nnsgrpnmnd  41630  1neven  41744  altgsumbc  41945  pw2m1lepw2m1  42126  m1modmmod  42132  zofldiv2  42141  nnpw2pmod  42197  blen1b  42202  blennn0em1  42205  dignn0flhalflem1  42229  dignn0flhalflem2  42230  nn0sumshdiglemB  42234  nn0sumshdiglem1  42235  nn0sumshdiglem2  42236
  Copyright terms: Public domain W3C validator