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

Theorem neg1cn 9813
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 8795 . 2  |-  1  e.  CC
21negcli 9114 1  |-  -u 1  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   CCcc 8735   1c1 8738   -ucneg 9038
This theorem is referenced by:  m1expcl2  11125  iseraltlem2  12155  iseraltlem3  12156  fsumneg  12249  incexclem  12295  bitsfzo  12626  bezoutlem1  12717  negcncf  18421  dvmptneg  19315  dvlipcn  19341  lhop2  19362  plysubcl  19604  coesub  19638  dgrsub  19653  quotlem  19680  quotcl2  19682  quotdgr  19683  iaa  19705  dvradcnv  19797  efipi  19841  eulerid  19842  sin2pi  19843  sinmpi  19855  cosmpi  19856  sinppi  19857  cosppi  19858  efif1olem2  19905  logneg  19941  lognegb  19943  logtayl  20007  logtayl2  20009  root1id  20094  root1eq1  20095  root1cj  20096  cxpeq  20097  angneg  20101  ang180lem1  20107  1cubrlem  20137  1cubr  20138  atandm4  20175  atandmtan  20216  atantayl3  20235  leibpi  20238  log2cnv  20240  wilthlem1  20306  wilthlem2  20307  basellem2  20319  basellem5  20322  basellem9  20326  isnsqf  20373  mule1  20386  mumul  20419  musum  20431  ppiub  20443  dchrptlem1  20503  dchrptlem2  20504  lgsneg  20558  lgsdilem  20561  lgsdir2lem3  20564  lgsdir2lem4  20565  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsne0  20572  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem1  20597  lgsquad2lem2  20598  lgsquad3  20600  m1lgs  20601  dchrisum0flblem1  20657  rpvmasum2  20661  vcsubdir  21112  vcm  21127  vcnegneg  21130  vcnegsubdi2  21131  vcsub4  21132  nvinvfval  21198  nvmval2  21201  nvzs  21203  nvmf  21204  nvmdi  21208  nvnegneg  21209  nvsubadd  21213  nvpncan2  21214  nvaddsub4  21219  nvnncan  21221  nvm1  21230  nvdif  21231  nvmtri  21237  nvabs  21239  nvge0  21240  nvnd  21257  imsmetlem  21259  smcnlem  21270  vmcn  21272  ipval2  21280  4ipval2  21281  ipval3  21282  dipcj  21290  dip0r  21293  sspmval  21309  lno0  21334  lnosub  21337  ip0i  21403  ipdirilem  21407  ipasslem2  21410  ipasslem10  21417  dipsubdir  21426  hvsubf  21595  hvsubcl  21597  hvsubid  21605  hv2neg  21607  hvm1neg  21611  hvaddsubval  21612  hvsub4  21616  hvaddsub12  21617  hvpncan  21618  hvaddsubass  21620  hvsubass  21623  hvsubdistr1  21628  hvsubdistr2  21629  hvsubsub4i  21638  hvnegdii  21641  hvsubeq0i  21642  hvsubcan2i  21643  hvaddcani  21644  hvsubaddi  21645  hvaddeq0  21648  hvsubcan  21653  hvsubcan2  21654  hvsub0  21655  his2sub  21671  hisubcomi  21683  normlem0  21688  normlem9  21697  normsubi  21720  norm3difi  21726  normpar2i  21735  hilablo  21739  shsubcl  21800  hhssabloi  21839  shsel3  21894  pjsubii  22257  pjssmii  22260  honegsubi  22376  honegneg  22386  hosubneg  22387  hosubdi  22388  honegdi  22389  honegsubdi  22390  honegsubdi2  22391  hosub4  22393  hosubsub4  22398  hosubeq0i  22406  nmopnegi  22545  lnopsubi  22554  lnophdi  22582  lnophmlem2  22597  lnfnsubi  22626  bdophdi  22677  nmoptri2i  22679  superpos  22934  cdj1i  23013  cdj3lem1  23014  subfacval2  23718  subfaclim  23719  axlowdimlem13  24582  rmym1  27020  psgnunilem4  27420  m1expaddsub  27421  psgnuni  27422  psgnpmtr  27433  cnmsgnsubg  27434  cnmsgnbas  27435  cnmsgngrp  27436  psgnghm  27437  proot1ex  27520  expgrowth  27552  m1expeven  27725  climneg  27736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-po 4314  df-so 4315  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-riota 6304  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-ltxr 8872  df-sub 9039  df-neg 9040
  Copyright terms: Public domain W3C validator