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

Theorem 1cnd 9658
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 9596 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   CCcc 9536   1c1 9539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9596
This theorem is referenced by:  1p1times  9803  addcom  9818  addcomd  9834  pncan1  10042  npcan1  10043  mulsubfacd  10077  recrec  10303  rec11  10304  rec11r  10305  rereccl  10324  subrec  10435  nn1m1nn  10629  add1p1  10862  sub1m1  10863  cnm2m1cnm3  10864  nn0n0n1ge2  10932  zneo  11018  rpnnen1lem5  11294  lincmb01cmp  11773  iccf1o  11774  xov1plusxeqvd  11776  zpnn0elfzo1  11984  ubmelm1fzo  12004  fzoshftral  12019  fladdz  12055  ltdifltdiv  12063  dfceil2  12065  modvalp1  12112  negmod  12135  modnegd  12142  binom3  12390  zesq  12392  bcm1k  12497  bcp1n  12498  bcp1m1  12502  bcpasc  12503  bcn2m1  12506  hashfz  12594  hashfzo  12596  hashf1lem2  12614  hashf1  12615  brfi1indlem  12640  lswccatn0lsw  12721  swrdccatwrd  12809  revccat  12856  repswrevw  12874  cshwidxm1  12893  cshwidxn  12895  cshweqrep  12905  swrd2lsw  13006  relexpaddnn  13093  absexpz  13347  reccn2  13638  rlimno1  13695  isercolllem1  13706  isercoll2  13710  iseraltlem2  13727  iseraltlem3  13728  hashiun  13860  binomlem  13865  bcxmas  13871  incexc  13873  incexc2  13874  climcndslem1  13885  arisum  13896  trireciplem  13898  geolim2  13905  georeclim  13906  mertenslem1  13918  prodfrec  13929  ntrivcvg  13931  ntrivcvgtail  13934  prodrblem  13961  prodmolem2a  13966  fprodntriv  13974  prod1  13976  fprodser  13981  fprodcl  13984  fprodm1  13999  fprodp1  14001  risefacval2  14041  fallfacval2  14042  risefacp1  14060  fallfacp1  14061  risefacfac  14066  fallfacfwd  14067  binomfallfaclem2  14071  fallfacval4  14074  bpolydiflem  14085  ef0lem  14111  tanaddlem  14198  tanadd  14199  cos01bnd  14218  oddm1even  14344  oddp1even  14345  oexpneg  14346  bitsp1o  14381  bitsf1  14394  sadcp1  14403  qredeu  14626  prmdiv  14693  prmdiveq  14694  vfermltlALT  14707  pcexp  14763  pc2dvds  14782  4sqlem11  14853  4sqlem12  14854  vdwapun  14878  vdwlem3  14887  vdwlem6  14890  vdwlem9  14893  ramub1lem2  14939  prmop1  14950  prmdvdsprmo  14954  prmgaplem8  14982  cshwshashnsame  15028  gsumccat  16567  mulgnnass  16728  psgnunilem5  17077  psgnunilem2  17078  sylow1lem1  17176  efgredlemc  17321  odadd2  17413  srgbinomlem3  17701  srgbinomlem4  17702  cncrng  18915  cnfldmulg  18926  gzrngunit  18959  zringunit  18984  prmirredlem  18986  cayhamlem1  19812  expcn  21791  iirevcn  21845  iihalf2cn  21849  icchmeo  21856  icopnfcnv  21857  icopnfhmeo  21858  evth  21874  pjthlem1  22263  ovolunlem1a  22318  ovolunlem1  22319  opnmbllem  22427  mbfi1fseqlem6  22546  bddibl  22665  dvnadd  22751  dvmptid  22779  dvcnvlem  22796  dveflem  22799  dvsincos  22801  dvlipcn  22814  dvivthlem1  22828  lhop2  22835  dvcvx  22840  dvfsumle  22841  dvfsumabs  22843  dvfsumlem1  22846  dvfsumlem2  22847  ply1divex  22953  fta1glem1  22982  dgrcolem1  23086  dgrcolem2  23087  aaliou3lem2  23155  aaliou3lem8  23157  dvtaylp  23181  dvntaylp  23182  taylthlem1  23184  taylthlem2  23185  abelthlem1  23242  abelthlem2  23243  abelthlem6  23247  abelthlem7  23249  logdivlti  23425  advlog  23455  advlogexp  23456  logtayl  23461  cxpmul2  23490  dvcxp1  23536  dvcxp2  23537  dvcncxp1  23539  dvcnsqrt  23540  loglesqrt  23554  relogbdiv  23572  ang180lem4  23597  ang180lem5  23598  isosctrlem2  23604  isosctrlem3  23605  affineequiv  23608  affineequiv2  23609  angpieqvdlem  23610  chordthmlem2  23615  chordthmlem3  23616  chordthmlem5  23618  dcubic2  23626  dcubic  23628  quart1lem  23637  quart1  23638  quart  23643  asinlem  23650  asinlem3  23653  atansopn  23714  dvatan  23717  leibpi  23724  birthdaylem2  23734  efrlim  23751  cxplim  23753  divsqrtsumlem  23761  logdifbnd  23775  emcllem2  23778  emcllem3  23779  emcllem5  23781  zetacvg  23796  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem4  23813  lgamgulmlem5  23814  lgamgulmlem6  23815  lgamgulm2  23817  lgamcvg2  23836  gamcvg  23837  gamcvg2lem  23840  lgam1  23845  gamfac  23848  ftalem5  23857  basellem3  23863  basellem5  23865  basellem8  23868  basellem9  23869  sqff1o  23963  muinv  23976  logfaclbnd  24004  logfacrlim  24006  logexprlim  24007  dchr1cl  24033  dchrinvcl  24035  dchrfi  24037  dchr1  24039  dchrsum2  24050  bcmono  24059  bcp1ctr  24061  bclbnd  24062  bposlem1  24066  bposlem9  24074  lgseisenlem4  24134  lgsquadlem1  24136  m1lgs  24144  2sqlem8  24154  chtppilim  24167  rpvmasumlem  24179  dchrisumlem1  24181  dchrisum0re  24205  dchrisum0lem2a  24209  mudivsum  24222  mulogsumlem  24223  mulogsum  24224  2vmadivsumlem  24232  selberg4lem1  24252  pntrsumo1  24257  selberg34r  24263  pntrlog2bndlem2  24270  pntrlog2bndlem4  24272  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntibndlem2  24283  pntlemg  24290  pntlemr  24294  pntlemf  24297  pntlemk  24298  pntlemo  24299  pntlem3  24301  ostth2lem2  24326  ttgcontlem1  24752  cusgrasizeinds  25040  cusgrasize2inds  25041  wlkdvspthlem  25173  fargshiftf1  25201  fargshiftfo  25202  wwlknimp  25251  wlklniswwlkn2  25264  wwlknred  25287  wwlknextbi  25289  wwlknredwwlkn  25290  wwlkextwrd  25292  wwlkextinj  25294  wwlkextproplem2  25306  wwlkextproplem3  25307  clwlkisclwwlklem2a1  25343  clwlkisclwwlklem2a4  25348  clwlkisclwwlklem2a  25349  clwlkisclwwlklem1  25351  clwlkisclwwlklem0  25352  clwlkisclwwlk  25353  clwwlkel  25357  clwwlkf  25358  clwwlkext2edg  25366  clwwisshclwwlem1  25369  clwwisshclww  25371  wlklenvclwlk  25403  nbhashuvtx1  25479  rusgra0edg  25519  eupatrl  25532  frghash2spot  25627  frgregordn0  25634  extwwlkfablem1  25638  extwwlkfablem2  25642  numclwwlkovf2ex  25650  numclwlk1lem2foa  25655  numclwlk1lem2fo  25659  numclwlk2lem2f  25667  numclwlk2lem2f1o  25669  smcnlem  26169  bcm1n  28198  ltesubnnd  28214  omndmul2  28304  archirngz  28335  archiabllem1a  28337  archiabllem2c  28341  psgnfzto1stlem  28443  1smat1  28460  madjusmdetlem2  28484  madjusmdetlem4  28486  dya2icoseg  28929  iwrdsplit  29037  fibp1  29051  ballotlemfp1  29141  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemic  29156  ballotlem1c  29157  ballotlemsgt1  29160  ballotlemsdom  29161  ballotlemsel1i  29162  ballotlemsi  29164  ballotlemsima  29165  ballotlem1ri  29184  sgn0bi  29197  signstfvn  29237  signsvtn0  29238  signstfveq0  29245  signsvfn  29250  signsvtn  29252  signshf  29256  subfacp1lem1  29681  subfacp1lem5  29686  cvxpcon  29744  sinccvglem  30095  divcnvlin  30145  muls1d  30146  bcm1nt  30151  bcprod  30152  bccolsum  30153  iprodgam  30156  faclimlem1  30157  faclimlem2  30158  faclimlem3  30159  faclim  30160  iprodfac  30161  faclim2  30162  fwddifnp1  30708  bj-bary1lem1  31452  poimirlem25  31659  poimirlem32  31666  opnmbllem0  31670  itg2addnclem2  31688  dvasin  31722  dvacos  31723  areacirclem1  31726  areacirclem4  31729  areacirc  31731  bfp  31850  pell1qrge1  35414  rmspecfund  35453  acongeq  35529  jm2.18  35539  jm2.19lem3  35542  jm2.25  35550  jm2.16nn0  35555  jm3.1lem1  35568  jm3.1lem2  35569  itgpowd  35788  areaquad  35790  relexpmulnn  35930  relexpaddss  35939  cvgdvgrat  36289  radcnvrat  36290  hashnzfzclim  36298  ofdivrec  36302  expgrowthi  36309  bccm1k  36318  dvradcnv2  36323  binomcxplemwb  36324  binomcxplemnn0  36325  binomcxplemrat  36326  binomcxplemfrat  36327  binomcxplemdvbinom  36329  binomcxplemnotnn0  36332  refsum2cnlem1  36988  adddirp1d  37109  fzisoeu  37117  fperiodmullem  37120  fzdifsuc2  37129  fmul01lt1lem2  37225  m1expevenOLD  37232  clim1fr1  37241  isumneg  37242  climneg  37251  sumnnodd  37272  reclimc  37296  coseq0  37301  coskpi2  37303  cosknegpi  37306  fprodcncf  37341  dvmptdiv  37351  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvnxpaek  37376  dvnmul  37377  dvmptfprod  37379  dvnprodlem3  37382  itgsinexp  37390  itgiccshift  37416  itgperiod  37417  itgsbtaddcnst  37418  stoweidlem1  37420  stoweidlem7  37426  stoweidlem10  37429  stoweidlem11  37430  stoweidlem14  37433  stoweidlem17  37436  stoweidlem34  37454  stoweidlem42  37462  wallispilem3  37488  wallispilem5  37490  wallispi  37491  wallispi2lem1  37492  wallispi2lem2  37493  wallispi2  37494  stirlinglem1  37495  stirlinglem3  37497  stirlinglem4  37498  stirlinglem5  37499  stirlinglem6  37500  stirlinglem7  37501  stirlinglem8  37502  stirlinglem10  37504  stirlinglem11  37505  stirlinglem12  37506  stirlinglem13  37507  stirlinglem15  37509  dirkertrigeqlem2  37520  dirkertrigeqlem3  37521  dirkertrigeq  37522  dirkercncflem1  37524  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem11  37539  fourierdlem15  37543  fourierdlem26  37554  fourierdlem36  37564  fourierdlem40  37568  fourierdlem41  37569  fourierdlem42  37570  fourierdlem48  37576  fourierdlem49  37577  fourierdlem56  37584  fourierdlem58  37586  fourierdlem59  37587  fourierdlem62  37590  fourierdlem64  37592  fourierdlem65  37593  fourierdlem78  37606  fourierdlem79  37607  sqwvfoura  37650  fourierswlem  37652  fouriersw  37653  etransclem23  37679  etransclem24  37680  etransclem28  37684  etransclem35  37691  etransclem38  37694  nnfoctbdjlem  37792  sigaradd  37865  xp1d2m1eqxm1d2  38091  deccarry  38095  onego  38156  zofldiv2ALTV  38171  oexpnegALTV  38186  opoeALTV  38192  opeoALTV  38193  epee  38212  perfectALTVlem1  38223  fzosplitpr  38404  0nodd  38558  2nodd  38560  nnsgrpnmnd  38566  1neven  38680  altgsumbc  38883  pw2m1lepw2m1  39069  m1modmmod  39075  nn0ob  39081  zofldiv2  39089  nnpw2pmod  39145  blen1b  39150  blennn0em1  39153  dignn0flhalflem1  39177  dignn0flhalflem2  39178  nn0sumshdiglemB  39182  nn0sumshdiglem1  39183  nn0sumshdiglem2  39184
  Copyright terms: Public domain W3C validator