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

Theorem 1cnd 9402
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 9340 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9280   1c1 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9340
This theorem is referenced by:  rpnnen1lem5  10983  isercoll2  13146  hashiun  13285  binomlem  13292  bcxmas  13298  incexc  13300  incexc2  13301  arisum  13322  trireciplem  13324  georeclim  13332  mertenslem1  13344  ef0lem  13364  tanaddlem  13450  tanadd  13451  cos01bnd  13470  bitsf1  13642  cshwshashnsame  14130  mulgnnass  15655  odadd2  16331  srgbinomlem3  16640  srgbinomlem4  16641  cnfldmulg  17848  zringunit  17914  prmirredlem  17917  expcn  20448  iirevcn  20502  iihalf2cn  20506  icchmeo  20513  evth  20531  pjthlem1  20924  opnmbllem  21081  mbfi1fseqlem6  21198  bddibl  21317  dvnadd  21403  dvcnvlem  21448  dveflem  21451  dvsincos  21453  dvlipcn  21466  dvivthlem1  21480  lhop2  21487  dvcvx  21492  dvfsumle  21493  dvfsumabs  21495  dvfsumlem1  21498  dvfsumlem2  21499  ply1divex  21608  fta1glem1  21637  dgrcolem1  21740  dgrcolem2  21741  dvtaylp  21835  dvntaylp  21836  taylthlem1  21838  taylthlem2  21839  abelthlem1  21896  abelthlem6  21901  logdivlti  22069  advlog  22099  advlogexp  22100  logtayl  22105  cxpmul2  22134  dvcxp1  22180  dvcxp2  22181  loglesqr  22196  ang180lem4  22208  ang180lem5  22209  isosctrlem2  22217  isosctrlem3  22218  chordthmlem2  22228  chordthmlem3  22229  chordthmlem5  22231  quart  22256  atansopn  22327  dvatan  22330  leibpi  22337  birthdaylem2  22346  efrlim  22363  cxplim  22365  divsqrsumlem  22373  logdifbnd  22387  emcllem2  22390  emcllem3  22391  emcllem5  22393  ftalem5  22414  basellem3  22420  basellem5  22422  basellem8  22425  basellem9  22426  muinv  22533  logfaclbnd  22561  logfacrlim  22563  logexprlim  22564  dchrfi  22594  bposlem1  22623  bposlem9  22631  lgseisenlem4  22691  lgsquadlem1  22693  chtppilim  22724  rpvmasumlem  22736  dchrisumlem1  22738  dchrisum0re  22762  dchrisum0lem2a  22766  mudivsum  22779  mulogsumlem  22780  mulogsum  22781  2vmadivsumlem  22789  selberg4lem1  22809  pntrsumo1  22814  selberg34r  22820  pntrlog2bndlem2  22827  pntrlog2bndlem4  22829  pntrlog2bndlem5  22830  pntrlog2bndlem6  22832  pntibndlem2  22840  pntlemg  22847  pntlemr  22851  pntlemf  22854  pntlemk  22855  pntlemo  22856  pntlem3  22858  ttgcontlem1  23131  smcnlem  24092  iwrdsplit  26770  fibp1  26784  dvcncxp1  28477  dvcnsqr  28478  dvasin  28480  dvacos  28481  itgpowd  29590  areaquad  29592  stoweidlem1  29796  stoweidlem7  29802  stoweidlem10  29805  stoweidlem11  29806  stoweidlem14  29809  stoweidlem17  29812  stoweidlem34  29829  stoweidlem42  29837  altgsumbc  30749  bj-bary1lem1  32600
  Copyright terms: Public domain W3C validator