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

Theorem 1cnd 9677
Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1cnd  |-  ( ph  ->  1  e.  CC )

Proof of Theorem 1cnd
StepHypRef Expression
1 ax-1cn 9615 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   CCcc 9555   1c1 9558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9615
This theorem is referenced by:  1p1times  9822  addcom  9837  addcomd  9853  pncan1  10064  npcan1  10065  mulsubfacd  10099  recrec  10326  rec11  10327  rec11r  10328  rereccl  10347  subrec  10458  nn1m1nn  10651  add1p1  10886  sub1m1  10887  cnm2m1cnm3  10888  nn0n0n1ge2  10956  zneo  11041  rpnnen1lem5  11317  lincmb01cmp  11801  iccf1o  11802  xov1plusxeqvd  11804  zpnn0elfzo1  12016  ubmelm1fzo  12036  fzoshftral  12053  fladdz  12091  ltdifltdiv  12099  dfceil2  12101  modvalp1  12148  negmod  12171  modnegd  12179  addmodlteq  12198  binom3  12431  zesq  12433  bcm1k  12538  bcp1n  12539  bcp1m1  12543  bcpasc  12544  bcn2m1  12547  hashfz  12640  hashfzo  12642  hashf1lem2  12660  hashf1  12661  brfi1indlem  12690  lswccatn0lsw  12785  swrdccatwrd  12878  revccat  12925  repswrevw  12943  cshwidxm1  12963  cshwidxn  12965  cshweqrep  12977  cshimadifsn0  12986  swrd2lsw  13102  relexpaddnn  13191  absexpz  13445  reccn2  13737  rlimno1  13794  isercolllem1  13805  isercoll2  13809  iseraltlem2  13826  iseraltlem3  13827  hashiun  13959  binomlem  13964  bcxmas  13970  incexc  13972  incexc2  13973  climcndslem1  13984  arisum  13995  trireciplem  13997  geolim2  14004  georeclim  14005  mertenslem1  14017  prodfrec  14028  ntrivcvg  14030  ntrivcvgtail  14033  prodrblem  14060  prodmolem2a  14065  fprodntriv  14073  prod1  14075  fprodser  14080  fprodcl  14083  fprodm1  14098  fprodp1  14100  risefacval2  14140  fallfacval2  14141  risefacp1  14159  fallfacp1  14160  risefacfac  14165  fallfacfwd  14166  binomfallfaclem2  14170  fallfacval4  14173  bpolydiflem  14184  ef0lem  14210  tanaddlem  14297  tanadd  14298  cos01bnd  14317  oddm1even  14444  oddp1even  14445  oexpneg  14446  bitsp1o  14485  bitsf1  14499  sadcp1  14508  qredeu  14743  prmdiv  14812  prmdiveq  14813  vfermltlALT  14832  pcexp  14888  pc2dvds  14907  4sqlem11  14978  4sqlem12  14979  vdwapun  15003  vdwlem3  15012  vdwlem6  15015  vdwlem9  15018  ramub1lem2  15064  prmop1  15075  prmdvdsprmo  15079  prmgaplem8  15107  cshwshashnsame  15152  gsumccat  16703  mulgnnass  16864  psgnunilem5  17213  psgnunilem2  17214  sylow1lem1  17328  efgredlemc  17473  odadd2  17565  srgbinomlem3  17853  srgbinomlem4  17854  cncrng  19066  cnfldmulg  19077  gzrngunit  19110  zringunit  19139  prmirredlem  19141  cayhamlem1  19967  expcn  21982  iirevcn  22036  iihalf2cn  22040  icchmeo  22047  icopnfcnv  22048  icopnfhmeo  22049  evth  22065  pjthlem1  22469  ovolunlem1a  22527  ovolunlem1  22528  opnmbllem  22638  mbfi1fseqlem6  22757  bddibl  22876  dvnadd  22962  dvmptid  22990  dvcnvlem  23007  dveflem  23010  dvsincos  23012  dvlipcn  23025  dvivthlem1  23039  lhop2  23046  dvcvx  23051  dvfsumle  23052  dvfsumabs  23054  dvfsumlem1  23057  dvfsumlem2  23058  ply1divex  23166  fta1glem1  23195  dgrcolem1  23306  dgrcolem2  23307  aaliou3lem2  23378  aaliou3lem8  23380  dvtaylp  23404  dvntaylp  23405  taylthlem1  23407  taylthlem2  23408  abelthlem1  23465  abelthlem2  23466  abelthlem6  23470  abelthlem7  23472  logdivlti  23648  advlog  23678  advlogexp  23679  logtayl  23684  cxpmul2  23713  dvcxp1  23759  dvcxp2  23760  dvcncxp1  23762  dvcnsqrt  23763  loglesqrt  23777  relogbdiv  23795  ang180lem4  23820  ang180lem5  23821  isosctrlem2  23827  isosctrlem3  23828  affineequiv  23831  affineequiv2  23832  angpieqvdlem  23833  chordthmlem2  23838  chordthmlem3  23839  chordthmlem5  23841  dcubic2  23849  dcubic  23851  quart1lem  23860  quart1  23861  quart  23866  asinlem  23873  asinlem3  23876  atansopn  23937  dvatan  23940  leibpi  23947  birthdaylem2  23957  efrlim  23974  cxplim  23976  divsqrtsumlem  23984  logdifbnd  23998  emcllem2  24001  emcllem3  24002  emcllem5  24004  zetacvg  24019  lgamgulmlem2  24034  lgamgulmlem3  24035  lgamgulmlem4  24036  lgamgulmlem5  24037  lgamgulmlem6  24038  lgamgulm2  24040  lgamcvg2  24059  gamcvg  24060  gamcvg2lem  24063  lgam1  24068  gamfac  24071  ftalem5  24080  ftalem5OLD  24082  basellem3  24088  basellem5  24090  basellem8  24093  basellem9  24094  sqff1o  24188  muinv  24201  logfaclbnd  24229  logfacrlim  24231  logexprlim  24232  perfectlem2  24237  dchr1cl  24258  dchrinvcl  24260  dchrfi  24262  dchr1  24264  dchrsum2  24275  bcmono  24284  bcp1ctr  24286  bclbnd  24287  bposlem1  24291  bposlem9  24299  lgseisenlem4  24359  lgsquadlem1  24361  m1lgs  24369  2sqlem8  24379  chtppilim  24392  rpvmasumlem  24404  dchrisumlem1  24406  dchrisum0re  24430  dchrisum0lem2a  24434  mudivsum  24447  mulogsumlem  24448  mulogsum  24449  2vmadivsumlem  24457  selberg4lem1  24477  pntrsumo1  24482  selberg34r  24488  pntrlog2bndlem2  24495  pntrlog2bndlem4  24497  pntrlog2bndlem5  24498  pntrlog2bndlem6  24500  pntibndlem2  24508  pntlemg  24515  pntlemr  24519  pntlemf  24522  pntlemk  24523  pntlemo  24524  pntlem3  24526  ostth2lem2  24551  ttgcontlem1  24994  cusgrasizeinds  25283  cusgrasize2inds  25284  wlkdvspthlem  25416  fargshiftf1  25444  fargshiftfo  25445  wwlknimp  25494  wlklniswwlkn2  25507  wwlknred  25530  wwlknextbi  25532  wwlknredwwlkn  25533  wwlkextwrd  25535  wwlkextinj  25537  wwlkextproplem2  25549  wwlkextproplem3  25550  clwlkisclwwlklem2a1  25586  clwlkisclwwlklem2a4  25591  clwlkisclwwlklem2a  25592  clwlkisclwwlklem1  25594  clwlkisclwwlklem0  25595  clwlkisclwwlk  25596  clwwlkel  25600  clwwlkf  25601  clwwlkext2edg  25609  clwwisshclwwlem1  25612  clwwisshclww  25614  wlklenvclwlk  25646  nbhashuvtx1  25722  rusgra0edg  25762  eupatrl  25775  frghash2spot  25870  frgregordn0  25877  extwwlkfablem1  25881  extwwlkfablem2  25885  numclwwlkovf2ex  25893  numclwlk1lem2foa  25898  numclwlk1lem2fo  25902  numclwlk2lem2f  25910  numclwlk2lem2f1o  25912  smcnlem  26414  bcm1n  28446  ltesubnnd  28460  omndmul2  28549  archirngz  28580  archiabllem1a  28582  archiabllem2c  28586  psgnfzto1stlem  28687  1smat1  28704  madjusmdetlem2  28728  madjusmdetlem4  28730  dya2icoseg  29172  iwrdsplit  29293  fibp1  29307  ballotlemfp1  29397  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemic  29412  ballotlem1c  29413  ballotlemsgt1  29416  ballotlemsdom  29417  ballotlemsel1i  29418  ballotlemsi  29420  ballotlemsima  29421  ballotlem1ri  29440  ballotlemicOLD  29450  ballotlem1cOLD  29451  ballotlemsgt1OLD  29454  ballotlemsdomOLD  29455  ballotlemsel1iOLD  29456  ballotlemsiOLD  29458  ballotlemsimaOLD  29459  ballotlem1riOLD  29478  sgn0bi  29491  signstfvn  29530  signsvtn0  29531  signstfveq0  29538  signsvfn  29543  signsvtn  29545  signshf  29549  subfacp1lem1  29974  subfacp1lem5  29979  cvxpcon  30037  sinccvglem  30388  divcnvlin  30438  muls1d  30439  bcm1nt  30444  bcprod  30445  bccolsum  30446  iprodgam  30449  faclimlem1  30450  faclimlem2  30451  faclimlem3  30452  faclim  30453  iprodfac  30454  faclim2  30455  fwddifnp1  31003  bj-bary1lem1  31786  poimirlem25  32029  poimirlem32  32036  opnmbllem0  32040  itg2addnclem2  32058  dvasin  32092  dvacos  32093  areacirclem1  32096  areacirclem4  32099  areacirc  32101  bfp  32220  pell1qrge1  35787  rmspecfund  35828  acongeq  35904  jm2.18  35914  jm2.19lem3  35917  jm2.25  35925  jm2.16nn0  35930  jm3.1lem1  35943  jm3.1lem2  35944  itgpowd  36170  areaquad  36172  relexpmulnn  36372  relexpaddss  36381  cvgdvgrat  36732  radcnvrat  36733  hashnzfzclim  36741  ofdivrec  36745  expgrowthi  36752  bccm1k  36761  dvradcnv2  36766  binomcxplemwb  36767  binomcxplemnn0  36768  binomcxplemrat  36769  binomcxplemfrat  36770  binomcxplemdvbinom  36772  binomcxplemnotnn0  36775  refsum2cnlem1  37421  adddirp1d  37598  fzisoeu  37606  fperiodmullem  37609  fzdifsuc2  37618  xralrple2  37664  nnsplit  37668  infleinflem2  37681  fmul01lt1lem2  37760  m1expevenOLD  37767  clim1fr1  37776  isumneg  37777  climneg  37786  sumnnodd  37807  reclimc  37831  coseq0  37836  coskpi2  37838  cosknegpi  37841  fprodcncf  37876  dvmptdiv  37886  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnxpaek  37914  dvnmul  37915  dvmptfprod  37917  dvnprodlem3  37920  itgsinexp  37928  itgiccshift  37954  itgperiod  37955  itgsbtaddcnst  37956  stoweidlem1  37973  stoweidlem7  37979  stoweidlem10  37982  stoweidlem11  37983  stoweidlem14  37986  stoweidlem17  37989  stoweidlem34  38007  stoweidlem42  38015  wallispilem3  38041  wallispilem5  38043  wallispi  38044  wallispi2lem1  38045  wallispi2lem2  38046  wallispi2  38047  stirlinglem1  38048  stirlinglem3  38050  stirlinglem4  38051  stirlinglem5  38052  stirlinglem6  38053  stirlinglem7  38054  stirlinglem8  38055  stirlinglem10  38057  stirlinglem11  38058  stirlinglem12  38059  stirlinglem13  38060  stirlinglem15  38062  dirkertrigeqlem2  38073  dirkertrigeqlem3  38074  dirkertrigeq  38075  dirkercncflem1  38077  dirkercncflem2  38078  dirkercncflem4  38080  fourierdlem11  38092  fourierdlem15  38096  fourierdlem26  38107  fourierdlem36  38118  fourierdlem40  38122  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem48  38130  fourierdlem49  38131  fourierdlem56  38138  fourierdlem58  38140  fourierdlem59  38141  fourierdlem62  38144  fourierdlem64  38146  fourierdlem65  38147  fourierdlem78  38160  fourierdlem79  38161  sqwvfoura  38204  fourierswlem  38206  fouriersw  38207  etransclem23  38234  etransclem24  38235  etransclem28  38239  etransclem35  38246  etransclem38  38249  nnfoctbdjlem  38409  sigaradd  38621  xp1d2m1eqxm1d2  38856  deccarry  38860  onego  38921  zofldiv2ALTV  38936  oexpnegALTV  38951  opoeALTV  38957  opeoALTV  38958  epee  38977  perfectALTVlem1  38988  fzosplitpr  39210  cusgrsize2inds  39679  wlkOnwlk1l  39861  pthdadjvtx  39923  crctcsh1wlkn0lem1  39988  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem5  39992  crctcsh1wlkn0lem6  39993  eucrct2eupth  40157  0nodd  40318  2nodd  40320  nnsgrpnmnd  40326  1neven  40440  altgsumbc  40641  pw2m1lepw2m1  40826  m1modmmod  40832  nn0ob  40838  zofldiv2  40846  nnpw2pmod  40902  blen1b  40907  blennn0em1  40910  dignn0flhalflem1  40934  dignn0flhalflem2  40935  nn0sumshdiglemB  40939  nn0sumshdiglem1  40940  nn0sumshdiglem2  40941
  Copyright terms: Public domain W3C validator