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

Theorem 1cnd 9398
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 9336 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   CCcc 9276   1c1 9279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9336
This theorem is referenced by:  rpnnen1lem5  10979  isercoll2  13142  hashiun  13281  binomlem  13288  bcxmas  13294  incexc  13296  incexc2  13297  arisum  13318  trireciplem  13320  georeclim  13328  mertenslem1  13340  ef0lem  13360  tanaddlem  13446  tanadd  13447  cos01bnd  13466  bitsf1  13638  cshwshashnsame  14126  mulgnnass  15648  odadd2  16324  srgbinomlem3  16630  srgbinomlem4  16631  cnfldmulg  17748  zringunit  17814  prmirredlem  17817  expcn  20348  iirevcn  20402  iihalf2cn  20406  icchmeo  20413  evth  20431  pjthlem1  20824  opnmbllem  20981  mbfi1fseqlem6  21098  bddibl  21217  dvnadd  21303  dvcnvlem  21348  dveflem  21351  dvsincos  21353  dvlipcn  21366  dvivthlem1  21380  lhop2  21387  dvcvx  21392  dvfsumle  21393  dvfsumabs  21395  dvfsumlem1  21398  dvfsumlem2  21399  ply1divex  21551  fta1glem1  21580  dgrcolem1  21683  dgrcolem2  21684  dvtaylp  21778  dvntaylp  21779  taylthlem1  21781  taylthlem2  21782  abelthlem1  21839  abelthlem6  21844  logdivlti  22012  advlog  22042  advlogexp  22043  logtayl  22048  cxpmul2  22077  dvcxp1  22123  dvcxp2  22124  loglesqr  22139  ang180lem4  22151  ang180lem5  22152  isosctrlem2  22160  isosctrlem3  22161  chordthmlem2  22171  chordthmlem3  22172  chordthmlem5  22174  quart  22199  atansopn  22270  dvatan  22273  leibpi  22280  birthdaylem2  22289  efrlim  22306  cxplim  22308  divsqrsumlem  22316  logdifbnd  22330  emcllem2  22333  emcllem3  22334  emcllem5  22336  ftalem5  22357  basellem3  22363  basellem5  22365  basellem8  22368  basellem9  22369  muinv  22476  logfaclbnd  22504  logfacrlim  22506  logexprlim  22507  dchrfi  22537  bposlem1  22566  bposlem9  22574  lgseisenlem4  22634  lgsquadlem1  22636  chtppilim  22667  rpvmasumlem  22679  dchrisumlem1  22681  dchrisum0re  22705  dchrisum0lem2a  22709  mudivsum  22722  mulogsumlem  22723  mulogsum  22724  2vmadivsumlem  22732  selberg4lem1  22752  pntrsumo1  22757  selberg34r  22763  pntrlog2bndlem2  22770  pntrlog2bndlem4  22772  pntrlog2bndlem5  22773  pntrlog2bndlem6  22775  pntibndlem2  22783  pntlemg  22790  pntlemr  22794  pntlemf  22797  pntlemk  22798  pntlemo  22799  pntlem3  22801  ttgcontlem1  23050  smcnlem  24011  iwrdsplit  26684  fibp1  26698  dvcncxp1  28386  dvcnsqr  28387  dvasin  28389  dvacos  28390  itgpowd  29499  areaquad  29501  stoweidlem1  29705  stoweidlem7  29711  stoweidlem10  29714  stoweidlem11  29715  stoweidlem14  29718  stoweidlem17  29721  stoweidlem34  29738  stoweidlem42  29746  bj-bary1lem1  32290
  Copyright terms: Public domain W3C validator