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

Theorem neg1cn 10098
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 9079 . 2  |-  1  e.  CC
21negcli 9399 1  |-  -u 1  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1727   CCcc 9019   1c1 9022   -ucneg 9323
This theorem is referenced by:  m1expcl2  11434  iseraltlem2  12507  iseraltlem3  12508  fsumneg  12601  incexclem  12647  incexc  12648  bitsfzo  12978  bezoutlem1  13069  negcncf  18979  dvmptneg  19883  dvlipcn  19909  lhop2  19930  plysubcl  20172  coesub  20206  dgrsub  20221  quotlem  20248  quotcl2  20250  quotdgr  20251  iaa  20273  dvradcnv  20368  efipi  20412  eulerid  20413  sin2pi  20414  sinmpi  20426  cosmpi  20427  sinppi  20428  cosppi  20429  efif1olem2  20476  logneg  20513  lognegb  20515  logtayl  20582  logtayl2  20584  root1id  20669  root1eq1  20670  root1cj  20671  cxpeq  20672  angneg  20676  ang180lem1  20682  1cubrlem  20712  1cubr  20713  atandm4  20750  atandmtan  20791  atantayl3  20810  leibpi  20813  log2cnv  20815  wilthlem1  20882  wilthlem2  20883  basellem2  20895  basellem5  20898  basellem9  20902  isnsqf  20949  mule1  20962  mumul  20995  musum  21007  ppiub  21019  dchrptlem1  21079  dchrptlem2  21080  lgsneg  21134  lgsdilem  21137  lgsdir2lem3  21140  lgsdir2lem4  21141  lgsdir2  21143  lgsdir  21145  lgsdi  21147  lgsne0  21148  lgseisenlem1  21164  lgseisenlem2  21165  lgseisenlem4  21167  lgseisen  21168  lgsquadlem1  21169  lgsquadlem2  21170  lgsquadlem3  21171  lgsquad2lem1  21173  lgsquad2lem2  21174  lgsquad3  21176  m1lgs  21177  dchrisum0flblem1  21233  rpvmasum2  21237  vcsubdir  22066  vcm  22081  vcnegneg  22084  vcnegsubdi2  22085  vcsub4  22086  nvinvfval  22152  nvmval2  22155  nvzs  22157  nvmf  22158  nvmdi  22162  nvnegneg  22163  nvsubadd  22167  nvpncan2  22168  nvaddsub4  22173  nvnncan  22175  nvm1  22184  nvdif  22185  nvmtri  22191  nvabs  22193  nvge0  22194  nvnd  22211  imsmetlem  22213  smcnlem  22224  vmcn  22226  ipval2  22234  4ipval2  22235  ipval3  22236  dipcj  22244  dip0r  22247  sspmval  22263  lno0  22288  lnosub  22291  ip0i  22357  ipdirilem  22361  ipasslem2  22364  ipasslem10  22371  dipsubdir  22380  hvsubf  22549  hvsubcl  22551  hvsubid  22559  hv2neg  22561  hvm1neg  22565  hvaddsubval  22566  hvsub4  22570  hvaddsub12  22571  hvpncan  22572  hvaddsubass  22574  hvsubass  22577  hvsubdistr1  22582  hvsubdistr2  22583  hvsubsub4i  22592  hvnegdii  22595  hvsubeq0i  22596  hvsubcan2i  22597  hvaddcani  22598  hvsubaddi  22599  hvaddeq0  22602  hvsubcan  22607  hvsubcan2  22608  hvsub0  22609  his2sub  22625  hisubcomi  22637  normlem0  22642  normlem9  22651  normsubi  22674  norm3difi  22680  normpar2i  22689  hilablo  22693  shsubcl  22754  hhssabloi  22793  shsel3  22848  pjsubii  23211  pjssmii  23214  honegsubi  23330  honegneg  23340  hosubneg  23341  hosubdi  23342  honegdi  23343  honegsubdi  23344  honegsubdi2  23345  hosub4  23347  hosubsub4  23352  hosubeq0i  23360  nmopnegi  23499  lnopsubi  23508  lnophdi  23536  lnophmlem2  23551  lnfnsubi  23580  bdophdi  23631  nmoptri2i  23633  superpos  23888  cdj1i  23967  cdj3lem1  23968  qqhval2lem  24396  subfacval2  24904  subfaclim  24905  m1expevenALT  24936  risefallfac  25371  fallrisefac  25372  fallfac0  25375  0risefac  25385  binomrisefac  25389  axlowdimlem13  25924  rmym1  27036  psgnunilem4  27435  m1expaddsub  27436  psgnuni  27437  psgnpmtr  27448  cnmsgnsubg  27449  cnmsgnbas  27450  cnmsgngrp  27451  psgnghm  27452  proot1ex  27535  expgrowth  27567  m1expeven  27739  climneg  27750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-mulcom 9085  ax-addass 9086  ax-mulass 9087  ax-distr 9088  ax-i2m1 9089  ax-1ne0 9090  ax-1rid 9091  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094  ax-pre-lttri 9095  ax-pre-lttrn 9096  ax-pre-ltadd 9097
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-id 4527  df-po 4532  df-so 4533  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-riota 6578  df-er 6934  df-en 7139  df-dom 7140  df-sdom 7141  df-pnf 9153  df-mnf 9154  df-ltxr 9156  df-sub 9324  df-neg 9325
  Copyright terms: Public domain W3C validator