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

Theorem 1cnd 9612
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 9550 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CCcc 9490   1c1 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9550
This theorem is referenced by:  rpnnen1lem5  11212  isercoll2  13454  hashiun  13599  binomlem  13604  bcxmas  13610  incexc  13612  incexc2  13613  arisum  13634  trireciplem  13636  georeclim  13644  mertenslem1  13656  ef0lem  13676  tanaddlem  13762  tanadd  13763  cos01bnd  13782  bitsf1  13955  cshwshashnsame  14446  mulgnnass  15980  odadd2  16658  srgbinomlem3  16995  srgbinomlem4  16996  cnfldmulg  18249  zringunit  18315  prmirredlem  18318  cayhamlem1  19162  expcn  21139  iirevcn  21193  iihalf2cn  21197  icchmeo  21204  evth  21222  pjthlem1  21615  opnmbllem  21773  mbfi1fseqlem6  21890  bddibl  22009  dvnadd  22095  dvcnvlem  22140  dveflem  22143  dvsincos  22145  dvlipcn  22158  dvivthlem1  22172  lhop2  22179  dvcvx  22184  dvfsumle  22185  dvfsumabs  22187  dvfsumlem1  22190  dvfsumlem2  22191  ply1divex  22300  fta1glem1  22329  dgrcolem1  22432  dgrcolem2  22433  dvtaylp  22527  dvntaylp  22528  taylthlem1  22530  taylthlem2  22531  abelthlem1  22588  abelthlem6  22593  logdivlti  22761  advlog  22791  advlogexp  22792  logtayl  22797  cxpmul2  22826  dvcxp1  22872  dvcxp2  22873  loglesqrt  22888  ang180lem4  22900  ang180lem5  22901  isosctrlem2  22909  isosctrlem3  22910  chordthmlem2  22920  chordthmlem3  22921  chordthmlem5  22923  quart  22948  atansopn  23019  dvatan  23022  leibpi  23029  birthdaylem2  23038  efrlim  23055  cxplim  23057  divsqrtsumlem  23065  logdifbnd  23079  emcllem2  23082  emcllem3  23083  emcllem5  23085  ftalem5  23106  basellem3  23112  basellem5  23114  basellem8  23117  basellem9  23118  muinv  23225  logfaclbnd  23253  logfacrlim  23255  logexprlim  23256  dchrfi  23286  bposlem1  23315  bposlem9  23323  lgseisenlem4  23383  lgsquadlem1  23385  chtppilim  23416  rpvmasumlem  23428  dchrisumlem1  23430  dchrisum0re  23454  dchrisum0lem2a  23458  mudivsum  23471  mulogsumlem  23472  mulogsum  23473  2vmadivsumlem  23481  selberg4lem1  23501  pntrsumo1  23506  selberg34r  23512  pntrlog2bndlem2  23519  pntrlog2bndlem4  23521  pntrlog2bndlem5  23522  pntrlog2bndlem6  23524  pntibndlem2  23532  pntlemg  23539  pntlemr  23543  pntlemf  23546  pntlemk  23547  pntlemo  23548  pntlem3  23550  ttgcontlem1  23892  clwlkisclwwlklem1  24491  clwlkisclwwlk  24493  smcnlem  25311  iwrdsplit  27994  fibp1  28008  signsvtn0  28195  dvcncxp1  29705  dvcnsqrt  29706  dvasin  29708  dvacos  29709  itgpowd  30815  areaquad  30817  hashnzfzclim  30855  adddirp1d  31091  sumnnodd  31200  coskpi2  31230  cosknegpi  31233  ioodvbdlimc1lem2  31290  ioodvbdlimc2lem  31292  stoweidlem1  31329  stoweidlem7  31335  stoweidlem10  31338  stoweidlem11  31339  stoweidlem14  31342  stoweidlem17  31345  stoweidlem34  31362  stoweidlem42  31370  fourierdlem41  31476  fourierdlem48  31483  sqwvfoura  31557  fourierswlem  31559  fouriersw  31560  altgsumbc  32037  bj-bary1lem1  33770
  Copyright terms: Public domain W3C validator