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

Theorem 1cnd 9523
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 9461 . 2  |-  1  e.  CC
21a1i 11 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   CCcc 9401   1c1 9404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 9461
This theorem is referenced by:  1p1times  9662  addcom  9677  addcomd  9693  pncan1  9901  npcan1  9902  mulsubfacd  9934  recrec  10158  rec11  10159  rec11r  10160  rereccl  10179  subrec  10290  nn1m1nn  10472  add1p1  10705  sub1m1  10706  cnm2m1cnm3  10707  nn0n0n1ge2  10776  zneo  10862  rpnnen1lem5  11131  lincmb01cmp  11584  iccf1o  11585  xov1plusxeqvd  11587  zpnn0elfzo1  11788  ubmelm1fzo  11807  fzoshftral  11822  fladdz  11858  ltdifltdiv  11866  dfceil2  11868  modvalp1  11915  negmod  11938  modnegd  11945  binom3  12189  zesq  12191  bcm1k  12295  bcp1n  12296  bcp1m1  12300  bcpasc  12301  bcn2m1  12304  hashfz  12389  hashfzo  12391  hashf1lem2  12409  hashf1  12410  brfi1indlem  12435  lswccatn0lsw  12516  swrdccatwrd  12604  revccat  12651  repswrevw  12669  cshwidxm1  12688  cshwidxn  12690  cshweqrep  12700  swrd2lsw  12801  relexpaddnn  12886  absexpz  13140  reccn2  13421  rlimno1  13478  isercolllem1  13489  isercoll2  13493  iseraltlem2  13507  iseraltlem3  13508  hashiun  13638  binomlem  13643  bcxmas  13649  incexc  13651  incexc2  13652  climcndslem1  13663  arisum  13673  trireciplem  13675  geolim2  13682  georeclim  13683  mertenslem1  13695  prodfrec  13706  ntrivcvg  13708  ntrivcvgtail  13711  prodrblem  13738  prodmolem2a  13743  fprodntriv  13751  prod1  13753  fprodser  13758  fprodcl  13761  fprodm1  13773  fprodp1  13775  ef0lem  13816  tanaddlem  13903  tanadd  13904  cos01bnd  13923  oddm1even  14049  oddp1even  14050  oexpneg  14051  bitsp1o  14085  bitsf1  14098  sadcp1  14107  qredeu  14250  prmdiv  14317  prmdiveq  14318  pcexp  14385  pc2dvds  14404  4sqlem11  14475  4sqlem12  14476  vdwapun  14494  vdwlem3  14503  vdwlem6  14506  vdwlem9  14509  ramub1lem2  14547  cshwshashnsame  14590  gsumccat  16126  mulgnnass  16287  psgnunilem5  16636  psgnunilem2  16637  sylow1lem1  16735  efgredlemc  16880  odadd2  16972  srgbinomlem3  17306  srgbinomlem4  17307  cncrng  18552  cnfldmulg  18563  gzrngunit  18596  zringunit  18621  prmirredlem  18623  cayhamlem1  19452  expcn  21461  iirevcn  21515  iihalf2cn  21519  icchmeo  21526  icopnfcnv  21527  icopnfhmeo  21528  evth  21544  pjthlem1  21937  ovolunlem1a  21992  ovolunlem1  21993  opnmbllem  22095  mbfi1fseqlem6  22212  bddibl  22331  dvnadd  22417  dvmptid  22445  dvcnvlem  22462  dveflem  22465  dvsincos  22467  dvlipcn  22480  dvivthlem1  22494  lhop2  22501  dvcvx  22506  dvfsumle  22507  dvfsumabs  22509  dvfsumlem1  22512  dvfsumlem2  22513  ply1divex  22622  fta1glem1  22651  dgrcolem1  22755  dgrcolem2  22756  aaliou3lem2  22824  aaliou3lem8  22826  dvtaylp  22850  dvntaylp  22851  taylthlem1  22853  taylthlem2  22854  abelthlem1  22911  abelthlem2  22912  abelthlem6  22916  abelthlem7  22918  logdivlti  23092  advlog  23122  advlogexp  23123  logtayl  23128  cxpmul2  23157  dvcxp1  23203  dvcxp2  23204  loglesqrt  23219  relogbdiv  23237  ang180lem4  23262  ang180lem5  23263  isosctrlem2  23269  isosctrlem3  23270  affineequiv  23273  affineequiv2  23274  angpieqvdlem  23275  chordthmlem2  23280  chordthmlem3  23281  chordthmlem5  23283  dcubic2  23291  dcubic  23293  quart1lem  23302  quart1  23303  quart  23308  asinlem  23315  asinlem3  23318  atansopn  23379  dvatan  23382  leibpi  23389  birthdaylem2  23399  efrlim  23416  cxplim  23418  divsqrtsumlem  23426  logdifbnd  23440  emcllem2  23443  emcllem3  23444  emcllem5  23446  ftalem5  23467  basellem3  23473  basellem5  23475  basellem8  23478  basellem9  23479  sqff1o  23573  muinv  23586  logfaclbnd  23614  logfacrlim  23616  logexprlim  23617  dchr1cl  23643  dchrinvcl  23645  dchrfi  23647  dchr1  23649  dchrsum2  23660  bcmono  23669  bcp1ctr  23671  bclbnd  23672  bposlem1  23676  bposlem9  23684  lgseisenlem4  23744  lgsquadlem1  23746  m1lgs  23754  2sqlem8  23764  chtppilim  23777  rpvmasumlem  23789  dchrisumlem1  23791  dchrisum0re  23815  dchrisum0lem2a  23819  mudivsum  23832  mulogsumlem  23833  mulogsum  23834  2vmadivsumlem  23842  selberg4lem1  23862  pntrsumo1  23867  selberg34r  23873  pntrlog2bndlem2  23880  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntibndlem2  23893  pntlemg  23900  pntlemr  23904  pntlemf  23907  pntlemk  23908  pntlemo  23909  pntlem3  23911  ostth2lem2  23936  ttgcontlem1  24309  cusgrasizeinds  24597  cusgrasize2inds  24598  wlkdvspthlem  24730  fargshiftf1  24758  fargshiftfo  24759  wwlknimp  24808  wlklniswwlkn2  24821  wwlknred  24844  wwlknextbi  24846  wwlknredwwlkn  24847  wwlkextwrd  24849  wwlkextinj  24851  wwlkextproplem2  24863  wwlkextproplem3  24864  clwlkisclwwlklem2a1  24900  clwlkisclwwlklem2a4  24905  clwlkisclwwlklem2a  24906  clwlkisclwwlklem1  24908  clwlkisclwwlklem0  24909  clwlkisclwwlk  24910  clwwlkel  24914  clwwlkf  24915  clwwlkext2edg  24923  clwwisshclwwlem1  24926  clwwisshclww  24928  wlklenvclwlk  24960  nbhashuvtx1  25036  rusgra0edg  25076  eupatrl  25089  frghash2spot  25184  frgregordn0  25191  extwwlkfablem1  25195  extwwlkfablem2  25199  numclwwlkovf2ex  25207  numclwlk1lem2foa  25212  numclwlk1lem2fo  25216  numclwlk2lem2f  25224  numclwlk2lem2f1o  25226  smcnlem  25724  bcm1n  27753  ltesubnnd  27765  omndmul2  27855  archirngz  27886  archiabllem1a  27888  archiabllem2c  27892  dya2icoseg  28404  iwrdsplit  28509  fibp1  28523  ballotlemfp1  28613  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemic  28628  ballotlem1c  28629  ballotlemsgt1  28632  ballotlemsdom  28633  ballotlemsel1i  28634  ballotlemsi  28636  ballotlemsima  28637  ballotlem1ri  28656  sgn0bi  28669  signstfvn  28709  signsvtn0  28710  signstfveq0  28717  signsvfn  28722  signsvtn  28724  signshf  28728  zetacvg  28746  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem4  28763  lgamgulmlem5  28764  lgamgulmlem6  28765  lgamgulm2  28767  lgamcvg2  28786  gamcvg  28787  gamcvg2lem  28790  lgam1  28795  gamfac  28798  subfacp1lem1  28812  subfacp1lem5  28817  cvxpcon  28876  sinccvglem  29227  divcnvlin  29284  muls1d  29285  iprodgam  29291  risefacval2  29298  fallfacval2  29299  risefacp1  29317  fallfacp1  29318  risefacfac  29323  fallfacfwd  29324  binomfallfaclem2  29328  fallfacval4  29331  faclimlem1  29334  faclimlem2  29335  faclimlem3  29336  faclim  29337  iprodfac  29338  faclim2  29339  bpolydiflem  29969  opnmbllem0  30215  itg2addnclem2  30233  dvcncxp1  30266  dvcnsqrt  30267  dvasin  30269  dvacos  30270  areacirclem1  30273  areacirclem4  30276  areacirc  30278  bfp  30486  pell1qrge1  30971  rmspecfund  31010  acongeq  31086  jm2.18  31096  jm2.19lem3  31099  jm2.25  31107  jm2.16nn0  31112  jm3.1lem1  31125  jm3.1lem2  31126  itgpowd  31350  areaquad  31352  cvgdvgrat  31362  radcnvrat  31363  hashnzfzclim  31395  ofdivrec  31399  expgrowthi  31406  bccm1k  31415  dvradcnv2  31420  binomcxplemwb  31421  binomcxplemnn0  31422  binomcxplemrat  31423  binomcxplemfrat  31424  binomcxplemdvbinom  31426  binomcxplemnotnn0  31429  refsum2cnlem1  31579  adddirp1d  31653  fzisoeu  31666  fperiodmullem  31669  fzdifsuc2  31678  fmul01lt1lem2  31745  m1expeven  31751  clim1fr1  31773  isumneg  31774  climneg  31782  sumnnodd  31802  reclimc  31825  coseq0  31830  coskpi2  31832  cosknegpi  31835  fprodcncf  31870  dvmptdiv  31880  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnxpaek  31905  dvnmul  31906  dvmptfprod  31908  dvnprodlem3  31911  itgsinexp  31919  itgiccshift  31945  itgperiod  31946  itgsbtaddcnst  31947  stoweidlem1  31949  stoweidlem7  31955  stoweidlem10  31958  stoweidlem11  31959  stoweidlem14  31962  stoweidlem17  31965  stoweidlem34  31982  stoweidlem42  31990  wallispilem3  32015  wallispilem5  32017  wallispi  32018  wallispi2lem1  32019  wallispi2lem2  32020  wallispi2  32021  stirlinglem1  32022  stirlinglem3  32024  stirlinglem4  32025  stirlinglem5  32026  stirlinglem6  32027  stirlinglem7  32028  stirlinglem8  32029  stirlinglem10  32031  stirlinglem11  32032  stirlinglem12  32033  stirlinglem13  32034  stirlinglem15  32036  dirkertrigeqlem2  32047  dirkertrigeqlem3  32048  dirkertrigeq  32049  dirkercncflem1  32051  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem11  32066  fourierdlem15  32070  fourierdlem26  32081  fourierdlem36  32091  fourierdlem40  32095  fourierdlem41  32096  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem56  32111  fourierdlem58  32113  fourierdlem59  32114  fourierdlem62  32117  fourierdlem64  32119  fourierdlem65  32120  fourierdlem78  32133  fourierdlem79  32134  sqwvfoura  32177  fourierswlem  32179  fouriersw  32180  etransclem23  32206  etransclem24  32207  etransclem28  32211  etransclem35  32218  etransclem38  32221  sigaradd  32249  xp1d2m1eqxm1d2  32459  onego  32489  zofldiv2ALTV  32504  oexpnegALTV  32519  opoeALTV  32525  opeoALTV  32526  perfectALTVlem1  32543  fzosplitpr  32662  0nodd  32816  2nodd  32818  nnsgrpnmnd  32824  1neven  32938  altgsumbc  33141  pw2m1lepw2m1  33327  m1modmmod  33334  nn0ob  33340  zofldiv2  33348  nnpw2pmod  33404  blen1b  33409  blennn0em1  33412  dignn0flhalflem1  33436  dignn0flhalflem2  33437  nn0sumshdiglemB  33441  nn0sumshdiglem1  33442  nn0sumshdiglem2  33443  bj-bary1lem1  35024  relexpaddss  38223  relexpmulnn  38245
  Copyright terms: Public domain W3C validator