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

Theorem 1cnd 9666
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 9604 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   CCcc 9544   1c1 9547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9604
This theorem is referenced by:  1p1times  9811  addcom  9826  addcomd  9842  pncan1  10050  npcan1  10051  mulsubfacd  10085  recrec  10311  rec11  10312  rec11r  10313  rereccl  10332  subrec  10443  nn1m1nn  10636  add1p1  10869  sub1m1  10870  cnm2m1cnm3  10871  nn0n0n1ge2  10939  zneo  11025  rpnnen1lem5  11301  lincmb01cmp  11782  iccf1o  11783  xov1plusxeqvd  11785  zpnn0elfzo1  11993  ubmelm1fzo  12013  fzoshftral  12028  fladdz  12064  ltdifltdiv  12072  dfceil2  12074  modvalp1  12121  negmod  12144  modnegd  12151  binom3  12399  zesq  12401  bcm1k  12506  bcp1n  12507  bcp1m1  12511  bcpasc  12512  bcn2m1  12515  hashfz  12603  hashfzo  12605  hashf1lem2  12623  hashf1  12624  brfi1indlem  12653  lswccatn0lsw  12738  swrdccatwrd  12826  revccat  12873  repswrevw  12891  cshwidxm1  12910  cshwidxn  12912  cshweqrep  12922  swrd2lsw  13027  relexpaddnn  13114  absexpz  13368  reccn2  13659  rlimno1  13716  isercolllem1  13727  isercoll2  13731  iseraltlem2  13748  iseraltlem3  13749  hashiun  13881  binomlem  13886  bcxmas  13892  incexc  13894  incexc2  13895  climcndslem1  13906  arisum  13917  trireciplem  13919  geolim2  13926  georeclim  13927  mertenslem1  13939  prodfrec  13950  ntrivcvg  13952  ntrivcvgtail  13955  prodrblem  13982  prodmolem2a  13987  fprodntriv  13995  prod1  13997  fprodser  14002  fprodcl  14005  fprodm1  14020  fprodp1  14022  risefacval2  14062  fallfacval2  14063  risefacp1  14081  fallfacp1  14082  risefacfac  14087  fallfacfwd  14088  binomfallfaclem2  14092  fallfacval4  14095  bpolydiflem  14106  ef0lem  14132  tanaddlem  14219  tanadd  14220  cos01bnd  14239  oddm1even  14365  oddp1even  14366  oexpneg  14367  bitsp1o  14405  bitsf1  14419  sadcp1  14428  qredeu  14663  prmdiv  14732  prmdiveq  14733  vfermltlALT  14752  pcexp  14808  pc2dvds  14827  4sqlem11  14898  4sqlem12  14899  vdwapun  14923  vdwlem3  14932  vdwlem6  14935  vdwlem9  14938  ramub1lem2  14984  prmop1  14995  prmdvdsprmo  14999  prmgaplem8  15027  cshwshashnsame  15073  gsumccat  16624  mulgnnass  16785  psgnunilem5  17134  psgnunilem2  17135  sylow1lem1  17249  efgredlemc  17394  odadd2  17486  srgbinomlem3  17774  srgbinomlem4  17775  cncrng  18988  cnfldmulg  18999  gzrngunit  19032  zringunit  19060  prmirredlem  19062  cayhamlem1  19888  expcn  21902  iirevcn  21956  iihalf2cn  21960  icchmeo  21967  icopnfcnv  21968  icopnfhmeo  21969  evth  21985  pjthlem1  22389  ovolunlem1a  22447  ovolunlem1  22448  opnmbllem  22557  mbfi1fseqlem6  22676  bddibl  22795  dvnadd  22881  dvmptid  22909  dvcnvlem  22926  dveflem  22929  dvsincos  22931  dvlipcn  22944  dvivthlem1  22958  lhop2  22965  dvcvx  22970  dvfsumle  22971  dvfsumabs  22973  dvfsumlem1  22976  dvfsumlem2  22977  ply1divex  23085  fta1glem1  23114  dgrcolem1  23225  dgrcolem2  23226  aaliou3lem2  23297  aaliou3lem8  23299  dvtaylp  23323  dvntaylp  23324  taylthlem1  23326  taylthlem2  23327  abelthlem1  23384  abelthlem2  23385  abelthlem6  23389  abelthlem7  23391  logdivlti  23567  advlog  23597  advlogexp  23598  logtayl  23603  cxpmul2  23632  dvcxp1  23678  dvcxp2  23679  dvcncxp1  23681  dvcnsqrt  23682  loglesqrt  23696  relogbdiv  23714  ang180lem4  23739  ang180lem5  23740  isosctrlem2  23746  isosctrlem3  23747  affineequiv  23750  affineequiv2  23751  angpieqvdlem  23752  chordthmlem2  23757  chordthmlem3  23758  chordthmlem5  23760  dcubic2  23768  dcubic  23770  quart1lem  23779  quart1  23780  quart  23785  asinlem  23792  asinlem3  23795  atansopn  23856  dvatan  23859  leibpi  23866  birthdaylem2  23876  efrlim  23893  cxplim  23895  divsqrtsumlem  23903  logdifbnd  23917  emcllem2  23920  emcllem3  23921  emcllem5  23923  zetacvg  23938  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem4  23955  lgamgulmlem5  23956  lgamgulmlem6  23957  lgamgulm2  23959  lgamcvg2  23978  gamcvg  23979  gamcvg2lem  23982  lgam1  23987  gamfac  23990  ftalem5  23999  ftalem5OLD  24001  basellem3  24007  basellem5  24009  basellem8  24012  basellem9  24013  sqff1o  24107  muinv  24120  logfaclbnd  24148  logfacrlim  24150  logexprlim  24151  perfectlem2  24156  dchr1cl  24177  dchrinvcl  24179  dchrfi  24181  dchr1  24183  dchrsum2  24194  bcmono  24203  bcp1ctr  24205  bclbnd  24206  bposlem1  24210  bposlem9  24218  lgseisenlem4  24278  lgsquadlem1  24280  m1lgs  24288  2sqlem8  24298  chtppilim  24311  rpvmasumlem  24323  dchrisumlem1  24325  dchrisum0re  24349  dchrisum0lem2a  24353  mudivsum  24366  mulogsumlem  24367  mulogsum  24368  2vmadivsumlem  24376  selberg4lem1  24396  pntrsumo1  24401  selberg34r  24407  pntrlog2bndlem2  24414  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntibndlem2  24427  pntlemg  24434  pntlemr  24438  pntlemf  24441  pntlemk  24442  pntlemo  24443  pntlem3  24445  ostth2lem2  24470  ttgcontlem1  24913  cusgrasizeinds  25202  cusgrasize2inds  25203  wlkdvspthlem  25335  fargshiftf1  25363  fargshiftfo  25364  wwlknimp  25413  wlklniswwlkn2  25426  wwlknred  25449  wwlknextbi  25451  wwlknredwwlkn  25452  wwlkextwrd  25454  wwlkextinj  25456  wwlkextproplem2  25468  wwlkextproplem3  25469  clwlkisclwwlklem2a1  25505  clwlkisclwwlklem2a4  25510  clwlkisclwwlklem2a  25511  clwlkisclwwlklem1  25513  clwlkisclwwlklem0  25514  clwlkisclwwlk  25515  clwwlkel  25519  clwwlkf  25520  clwwlkext2edg  25528  clwwisshclwwlem1  25531  clwwisshclww  25533  wlklenvclwlk  25565  nbhashuvtx1  25641  rusgra0edg  25681  eupatrl  25694  frghash2spot  25789  frgregordn0  25796  extwwlkfablem1  25800  extwwlkfablem2  25804  numclwwlkovf2ex  25812  numclwlk1lem2foa  25817  numclwlk1lem2fo  25821  numclwlk2lem2f  25829  numclwlk2lem2f1o  25831  smcnlem  26331  bcm1n  28377  ltesubnnd  28392  omndmul2  28482  archirngz  28513  archiabllem1a  28515  archiabllem2c  28519  psgnfzto1stlem  28621  1smat1  28638  madjusmdetlem2  28662  madjusmdetlem4  28664  dya2icoseg  29107  iwrdsplit  29228  fibp1  29242  ballotlemfp1  29332  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemic  29347  ballotlem1c  29348  ballotlemsgt1  29351  ballotlemsdom  29352  ballotlemsel1i  29353  ballotlemsi  29355  ballotlemsima  29356  ballotlem1ri  29375  ballotlemicOLD  29385  ballotlem1cOLD  29386  ballotlemsgt1OLD  29389  ballotlemsdomOLD  29390  ballotlemsel1iOLD  29391  ballotlemsiOLD  29393  ballotlemsimaOLD  29394  ballotlem1riOLD  29413  sgn0bi  29426  signstfvn  29466  signsvtn0  29467  signstfveq0  29474  signsvfn  29479  signsvtn  29481  signshf  29485  subfacp1lem1  29910  subfacp1lem5  29915  cvxpcon  29973  sinccvglem  30324  divcnvlin  30374  muls1d  30375  bcm1nt  30380  bcprod  30381  bccolsum  30382  iprodgam  30385  faclimlem1  30386  faclimlem2  30387  faclimlem3  30388  faclim  30389  iprodfac  30390  faclim2  30391  fwddifnp1  30937  bj-bary1lem1  31680  poimirlem25  31929  poimirlem32  31936  opnmbllem0  31940  itg2addnclem2  31958  dvasin  31992  dvacos  31993  areacirclem1  31996  areacirclem4  31999  areacirc  32001  bfp  32120  pell1qrge1  35686  rmspecfund  35727  acongeq  35803  jm2.18  35813  jm2.19lem3  35816  jm2.25  35824  jm2.16nn0  35829  jm3.1lem1  35842  jm3.1lem2  35843  itgpowd  36069  areaquad  36071  relexpmulnn  36271  relexpaddss  36280  cvgdvgrat  36632  radcnvrat  36633  hashnzfzclim  36641  ofdivrec  36645  expgrowthi  36652  bccm1k  36661  dvradcnv2  36666  binomcxplemwb  36667  binomcxplemnn0  36668  binomcxplemrat  36669  binomcxplemfrat  36670  binomcxplemdvbinom  36672  binomcxplemnotnn0  36675  refsum2cnlem1  37331  adddirp1d  37464  fzisoeu  37472  fperiodmullem  37475  fzdifsuc2  37484  xralrple2  37531  nnsplit  37535  fmul01lt1lem2  37603  m1expevenOLD  37610  clim1fr1  37619  isumneg  37620  climneg  37629  sumnnodd  37650  reclimc  37674  coseq0  37679  coskpi2  37681  cosknegpi  37684  fprodcncf  37719  dvmptdiv  37729  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnxpaek  37757  dvnmul  37758  dvmptfprod  37760  dvnprodlem3  37763  itgsinexp  37771  itgiccshift  37797  itgperiod  37798  itgsbtaddcnst  37799  stoweidlem1  37801  stoweidlem7  37807  stoweidlem10  37810  stoweidlem11  37811  stoweidlem14  37814  stoweidlem17  37817  stoweidlem34  37835  stoweidlem42  37843  wallispilem3  37869  wallispilem5  37871  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  wallispi2  37875  stirlinglem1  37876  stirlinglem3  37878  stirlinglem4  37879  stirlinglem5  37880  stirlinglem6  37881  stirlinglem7  37882  stirlinglem8  37883  stirlinglem10  37885  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  stirlinglem15  37890  dirkertrigeqlem2  37901  dirkertrigeqlem3  37902  dirkertrigeq  37903  dirkercncflem1  37905  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem11  37920  fourierdlem15  37924  fourierdlem26  37935  fourierdlem36  37946  fourierdlem40  37950  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem49  37959  fourierdlem56  37966  fourierdlem58  37968  fourierdlem59  37969  fourierdlem62  37972  fourierdlem64  37974  fourierdlem65  37975  fourierdlem78  37988  fourierdlem79  37989  sqwvfoura  38032  fourierswlem  38034  fouriersw  38035  etransclem23  38062  etransclem24  38063  etransclem28  38067  etransclem35  38074  etransclem38  38077  nnfoctbdjlem  38201  sigaradd  38346  xp1d2m1eqxm1d2  38581  deccarry  38585  onego  38646  zofldiv2ALTV  38661  oexpnegALTV  38676  opoeALTV  38682  opeoALTV  38683  epee  38702  perfectALTVlem1  38713  fzosplitpr  38919  cusgrsize2inds  39270  0nodd  39429  2nodd  39431  nnsgrpnmnd  39437  1neven  39551  altgsumbc  39754  pw2m1lepw2m1  39939  m1modmmod  39945  nn0ob  39951  zofldiv2  39959  nnpw2pmod  40015  blen1b  40020  blennn0em1  40023  dignn0flhalflem1  40047  dignn0flhalflem2  40048  nn0sumshdiglemB  40052  nn0sumshdiglem1  40053  nn0sumshdiglem2  40054
  Copyright terms: Public domain W3C validator