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

Theorem neg1cn 10027
Description: -1 is a complex number. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
neg1cn  |-  -u 1  e.  CC

Proof of Theorem neg1cn
StepHypRef Expression
1 ax-1cn 9008 . 2  |-  1  e.  CC
21negcli 9328 1  |-  -u 1  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   CCcc 8948   1c1 8951   -ucneg 9252
This theorem is referenced by:  m1expcl2  11362  iseraltlem2  12435  iseraltlem3  12436  fsumneg  12529  incexclem  12575  incexc  12576  bitsfzo  12906  bezoutlem1  12997  negcncf  18905  dvmptneg  19809  dvlipcn  19835  lhop2  19856  plysubcl  20098  coesub  20132  dgrsub  20147  quotlem  20174  quotcl2  20176  quotdgr  20177  iaa  20199  dvradcnv  20294  efipi  20338  eulerid  20339  sin2pi  20340  sinmpi  20352  cosmpi  20353  sinppi  20354  cosppi  20355  efif1olem2  20402  logneg  20439  lognegb  20441  logtayl  20508  logtayl2  20510  root1id  20595  root1eq1  20596  root1cj  20597  cxpeq  20598  angneg  20602  ang180lem1  20608  1cubrlem  20638  1cubr  20639  atandm4  20676  atandmtan  20717  atantayl3  20736  leibpi  20739  log2cnv  20741  wilthlem1  20808  wilthlem2  20809  basellem2  20821  basellem5  20824  basellem9  20828  isnsqf  20875  mule1  20888  mumul  20921  musum  20933  ppiub  20945  dchrptlem1  21005  dchrptlem2  21006  lgsneg  21060  lgsdilem  21063  lgsdir2lem3  21066  lgsdir2lem4  21067  lgsdir2  21069  lgsdir  21071  lgsdi  21073  lgsne0  21074  lgseisenlem1  21090  lgseisenlem2  21091  lgseisenlem4  21093  lgseisen  21094  lgsquadlem1  21095  lgsquadlem2  21096  lgsquadlem3  21097  lgsquad2lem1  21099  lgsquad2lem2  21100  lgsquad3  21102  m1lgs  21103  dchrisum0flblem1  21159  rpvmasum2  21163  vcsubdir  21992  vcm  22007  vcnegneg  22010  vcnegsubdi2  22011  vcsub4  22012  nvinvfval  22078  nvmval2  22081  nvzs  22083  nvmf  22084  nvmdi  22088  nvnegneg  22089  nvsubadd  22093  nvpncan2  22094  nvaddsub4  22099  nvnncan  22101  nvm1  22110  nvdif  22111  nvmtri  22117  nvabs  22119  nvge0  22120  nvnd  22137  imsmetlem  22139  smcnlem  22150  vmcn  22152  ipval2  22160  4ipval2  22161  ipval3  22162  dipcj  22170  dip0r  22173  sspmval  22189  lno0  22214  lnosub  22217  ip0i  22283  ipdirilem  22287  ipasslem2  22290  ipasslem10  22297  dipsubdir  22306  hvsubf  22475  hvsubcl  22477  hvsubid  22485  hv2neg  22487  hvm1neg  22491  hvaddsubval  22492  hvsub4  22496  hvaddsub12  22497  hvpncan  22498  hvaddsubass  22500  hvsubass  22503  hvsubdistr1  22508  hvsubdistr2  22509  hvsubsub4i  22518  hvnegdii  22521  hvsubeq0i  22522  hvsubcan2i  22523  hvaddcani  22524  hvsubaddi  22525  hvaddeq0  22528  hvsubcan  22533  hvsubcan2  22534  hvsub0  22535  his2sub  22551  hisubcomi  22563  normlem0  22568  normlem9  22577  normsubi  22600  norm3difi  22606  normpar2i  22615  hilablo  22619  shsubcl  22680  hhssabloi  22719  shsel3  22774  pjsubii  23137  pjssmii  23140  honegsubi  23256  honegneg  23266  hosubneg  23267  hosubdi  23268  honegdi  23269  honegsubdi  23270  honegsubdi2  23271  hosub4  23273  hosubsub4  23278  hosubeq0i  23286  nmopnegi  23425  lnopsubi  23434  lnophdi  23462  lnophmlem2  23477  lnfnsubi  23506  bdophdi  23557  nmoptri2i  23559  superpos  23814  cdj1i  23893  cdj3lem1  23894  qqhval2lem  24322  subfacval2  24830  subfaclim  24831  m1expevenALT  24862  risefallfac  25296  fallrisefac  25297  fallfac0  25300  0risefac  25309  binomrisefac  25313  axlowdimlem13  25801  rmym1  26892  psgnunilem4  27292  m1expaddsub  27293  psgnuni  27294  psgnpmtr  27305  cnmsgnsubg  27306  cnmsgnbas  27307  cnmsgngrp  27308  psgnghm  27309  proot1ex  27392  expgrowth  27424  m1expeven  27596  climneg  27607
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-mulcom 9014  ax-addass 9015  ax-mulass 9016  ax-distr 9017  ax-i2m1 9018  ax-1ne0 9019  ax-1rid 9020  ax-rnegex 9021  ax-rrecex 9022  ax-cnre 9023  ax-pre-lttri 9024  ax-pre-lttrn 9025  ax-pre-ltadd 9026
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-po 4467  df-so 4468  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-riota 6512  df-er 6868  df-en 7073  df-dom 7074  df-sdom 7075  df-pnf 9082  df-mnf 9083  df-ltxr 9085  df-sub 9253  df-neg 9254
  Copyright terms: Public domain W3C validator