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

Theorem 1cnd 9615
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 9553 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   1c1 9496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9553
This theorem is referenced by:  1p1times  9754  addcom  9769  addcomd  9785  pncan1  9990  npcan1  9991  mulsubfacd  10023  recrec  10248  rec11  10249  rec11r  10250  rereccl  10269  subrec  10380  nn1m1nn  10563  add1p1  10795  sub1m1  10796  cnm2m1cnm3  10797  nn0n0n1ge2  10866  zneo  10952  rpnnen1lem5  11223  lincmb01cmp  11674  iccf1o  11675  xov1plusxeqvd  11677  zpnn0elfzo1  11871  ubmelm1fzo  11890  fzoshftral  11905  fladdz  11940  ltdifltdiv  11948  dfceil2  11950  modvalp1  11996  modnegd  12024  binom3  12269  zesq  12271  bcm1k  12375  bcp1n  12376  bcp1m1  12380  bcpasc  12381  bcn2m1  12384  hashfz  12467  hashfzo  12469  hashf1lem2  12487  hashf1  12488  brfi1indlem  12513  lswccatn0lsw  12589  wrdlenccats1lenm1  12609  ccatw2s1p2  12623  swrdccatwrd  12675  revccat  12722  repswrevw  12740  cshwidxm1  12759  cshwidxn  12761  cshweqrep  12771  swrd2lsw  12872  absexpz  13120  reccn2  13401  rlimno1  13458  isercolllem1  13469  isercoll2  13473  iseraltlem2  13487  iseraltlem3  13488  hashiun  13618  binomlem  13623  bcxmas  13629  incexc  13631  incexc2  13632  climcndslem1  13643  arisum  13653  trireciplem  13655  geolim2  13662  georeclim  13663  mertenslem1  13675  prodfrec  13686  ntrivcvg  13688  ntrivcvgtail  13691  prodrblem  13718  prodmolem2a  13723  fprodntriv  13731  prod1  13733  fprodser  13738  fprodcl  13741  fprodm1  13753  fprodp1  13755  ef0lem  13796  tanaddlem  13883  tanadd  13884  cos01bnd  13903  oddm1even  14029  oddp1even  14030  oexpneg  14031  bitsp1o  14065  bitsf1  14078  sadcp1  14087  qredeu  14230  prmdiv  14297  prmdiveq  14298  pcexp  14365  pc2dvds  14384  4sqlem11  14455  4sqlem12  14456  vdwapun  14474  vdwlem3  14483  vdwlem6  14486  vdwlem9  14489  ramub1lem2  14527  cshwshashnsame  14570  gsumccat  15988  mulgnnass  16149  psgnunilem5  16498  psgnunilem2  16499  sylow1lem1  16597  efgredlemc  16742  odadd2  16834  srgbinomlem3  17172  srgbinomlem4  17173  cncrng  18418  cnfldmulg  18429  gzrngunit  18462  zringunit  18498  zrngunit  18499  prmirredlem  18501  cayhamlem1  19345  expcn  21354  iirevcn  21408  iihalf2cn  21412  icchmeo  21419  icopnfcnv  21420  icopnfhmeo  21421  evth  21437  pjthlem1  21830  ovolunlem1a  21885  ovolunlem1  21886  opnmbllem  21988  mbfi1fseqlem6  22105  bddibl  22224  dvnadd  22310  dvmptid  22338  dvcnvlem  22355  dveflem  22358  dvsincos  22360  dvlipcn  22373  dvivthlem1  22387  lhop2  22394  dvcvx  22399  dvfsumle  22400  dvfsumabs  22402  dvfsumlem1  22405  dvfsumlem2  22406  ply1divex  22515  fta1glem1  22544  dgrcolem1  22648  dgrcolem2  22649  aaliou3lem2  22717  aaliou3lem8  22719  dvtaylp  22743  dvntaylp  22744  taylthlem1  22746  taylthlem2  22747  abelthlem1  22804  abelthlem2  22805  abelthlem6  22809  abelthlem7  22811  logdivlti  22983  advlog  23013  advlogexp  23014  logtayl  23019  cxpmul2  23048  dvcxp1  23094  dvcxp2  23095  loglesqrt  23110  ang180lem4  23122  ang180lem5  23123  isosctrlem2  23131  isosctrlem3  23132  affineequiv  23135  affineequiv2  23136  angpieqvdlem  23137  chordthmlem2  23142  chordthmlem3  23143  chordthmlem5  23145  dcubic2  23153  dcubic  23155  quart1lem  23164  quart1  23165  quart  23170  asinlem  23177  asinlem3  23180  atansopn  23241  dvatan  23244  leibpi  23251  birthdaylem2  23260  efrlim  23277  cxplim  23279  divsqrtsumlem  23287  logdifbnd  23301  emcllem2  23304  emcllem3  23305  emcllem5  23307  ftalem5  23328  basellem3  23334  basellem5  23336  basellem8  23339  basellem9  23340  sqff1o  23434  muinv  23447  logfaclbnd  23475  logfacrlim  23477  logexprlim  23478  dchr1cl  23504  dchrinvcl  23506  dchrfi  23508  dchr1  23510  dchrsum2  23521  bcmono  23530  bcp1ctr  23532  bclbnd  23533  bposlem1  23537  bposlem9  23545  lgseisenlem4  23605  lgsquadlem1  23607  m1lgs  23615  2sqlem8  23625  chtppilim  23638  rpvmasumlem  23650  dchrisumlem1  23652  dchrisum0re  23676  dchrisum0lem2a  23680  mudivsum  23693  mulogsumlem  23694  mulogsum  23695  2vmadivsumlem  23703  selberg4lem1  23723  pntrsumo1  23728  selberg34r  23734  pntrlog2bndlem2  23741  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntibndlem2  23754  pntlemg  23761  pntlemr  23765  pntlemf  23768  pntlemk  23769  pntlemo  23770  pntlem3  23772  ostth2lem2  23797  ttgcontlem1  24166  cusgrasizeinds  24454  cusgrasize2inds  24455  wlkdvspthlem  24587  fargshiftf1  24615  fargshiftfo  24616  wwlknimp  24665  wlklniswwlkn2  24678  wwlknred  24701  wwlknextbi  24703  wwlknredwwlkn  24704  wwlkextwrd  24706  wwlkextinj  24708  wwlkextproplem2  24720  wwlkextproplem3  24721  clwlkisclwwlklem2a1  24757  clwlkisclwwlklem2a4  24762  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  clwlkisclwwlklem0  24766  clwlkisclwwlk  24767  clwwlkel  24771  clwwlkf  24772  clwwlkext2edg  24780  clwwisshclwwlem1  24783  clwwisshclww  24785  wlklenvclwlk  24817  nbhashuvtx1  24893  rusgra0edg  24933  eupatrl  24946  frghash2spot  25041  frgregordn0  25048  extwwlkfablem1  25052  extwwlkfablem2  25056  numclwwlkovf2ex  25064  numclwlk1lem2foa  25069  numclwlk1lem2fo  25073  numclwlk2lem2f  25081  numclwlk2lem2f1o  25083  smcnlem  25585  bcm1n  27578  ltesubnnd  27590  omndmul2  27680  archirngz  27711  archiabllem1a  27713  archiabllem2c  27717  dya2icoseg  28226  iwrdsplit  28304  fibp1  28318  ballotlemfp1  28408  ballotlemfc0  28409  ballotlemfcc  28410  ballotlemic  28423  ballotlem1c  28424  ballotlemsgt1  28427  ballotlemsdom  28428  ballotlemsel1i  28429  ballotlemsi  28431  ballotlemsima  28432  ballotlem1ri  28451  sgn0bi  28464  signstfvn  28504  signsvtn0  28505  signstfveq0  28512  signsvfn  28517  signsvtn  28519  signshf  28523  zetacvg  28535  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  lgam1  28584  gamfac  28587  subfacp1lem1  28601  subfacp1lem5  28606  cvxpcon  28665  sinccvglem  29016  relexpadd  29039  divcnvlin  29096  muls1d  29097  iprodgam  29101  risefacval2  29108  fallfacval2  29109  risefacp1  29127  fallfacp1  29128  risefacfac  29133  fallfacfwd  29134  binomfallfaclem2  29138  fallfacval4  29141  faclimlem1  29144  faclimlem2  29145  faclimlem3  29146  faclim  29147  iprodfac  29148  faclim2  29149  bpolydiflem  29792  opnmbllem0  30026  itg2addnclem2  30043  dvcncxp1  30076  dvcnsqrt  30077  dvasin  30079  dvacos  30080  areacirclem1  30083  areacirclem4  30086  areacirc  30088  bfp  30296  pell1qrge1  30782  rmspecfund  30821  acongeq  30897  jm2.18  30906  jm2.19lem3  30909  jm2.25  30917  jm2.16nn0  30922  jm3.1lem1  30935  jm3.1lem2  30936  itgpowd  31158  areaquad  31160  cvgdvgrat  31170  radcnvrat  31171  hashnzfzclim  31203  ofdivrec  31207  expgrowthi  31214  refsum2cnlem1  31366  adddirp1d  31440  fzisoeu  31454  fperiodmullem  31457  fzdifsuc2  31466  fmul01lt1lem2  31533  m1expeven  31539  clim1fr1  31561  isumneg  31562  climneg  31570  sumnnodd  31590  reclimc  31613  coseq0  31618  coskpi2  31620  cosknegpi  31623  fprodcncf  31658  dvmptdiv  31668  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnxpaek  31693  dvnmul  31694  dvmptfprod  31696  dvnprodlem3  31699  itgsinexp  31707  itgiccshift  31733  itgperiod  31734  itgsbtaddcnst  31735  stoweidlem1  31737  stoweidlem7  31743  stoweidlem10  31746  stoweidlem11  31747  stoweidlem14  31750  stoweidlem17  31753  stoweidlem34  31770  stoweidlem42  31778  wallispilem3  31803  wallispilem5  31805  wallispi  31806  wallispi2lem1  31807  wallispi2lem2  31808  wallispi2  31809  stirlinglem1  31810  stirlinglem3  31812  stirlinglem4  31813  stirlinglem5  31814  stirlinglem6  31815  stirlinglem7  31816  stirlinglem8  31817  stirlinglem10  31819  stirlinglem11  31820  stirlinglem12  31821  stirlinglem13  31822  stirlinglem15  31824  dirkertrigeqlem2  31835  dirkertrigeqlem3  31836  dirkertrigeq  31837  dirkercncflem1  31839  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem11  31854  fourierdlem15  31858  fourierdlem26  31869  fourierdlem36  31879  fourierdlem40  31883  fourierdlem41  31884  fourierdlem42  31885  fourierdlem48  31891  fourierdlem49  31892  fourierdlem56  31899  fourierdlem58  31901  fourierdlem59  31902  fourierdlem62  31905  fourierdlem64  31907  fourierdlem65  31908  fourierdlem78  31921  fourierdlem79  31922  sqwvfoura  31965  fourierswlem  31967  fouriersw  31968  etransclem24  31995  etransclem28  31999  etransclem35  32006  etransclem38  32009  sigaradd  32037  fzosplitpr  32296  0nodd  32451  2nodd  32453  nnsgrpnmnd  32459  1neven  32565  altgsumbc  32809  bj-bary1lem1  34555
  Copyright terms: Public domain W3C validator