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

Theorem neg1cn 10072
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 9053 . 2  |-  1  e.  CC
21negcli 9373 1  |-  -u 1  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   CCcc 8993   1c1 8996   -ucneg 9297
This theorem is referenced by:  m1expcl2  11408  iseraltlem2  12481  iseraltlem3  12482  fsumneg  12575  incexclem  12621  incexc  12622  bitsfzo  12952  bezoutlem1  13043  negcncf  18953  dvmptneg  19857  dvlipcn  19883  lhop2  19904  plysubcl  20146  coesub  20180  dgrsub  20195  quotlem  20222  quotcl2  20224  quotdgr  20225  iaa  20247  dvradcnv  20342  efipi  20386  eulerid  20387  sin2pi  20388  sinmpi  20400  cosmpi  20401  sinppi  20402  cosppi  20403  efif1olem2  20450  logneg  20487  lognegb  20489  logtayl  20556  logtayl2  20558  root1id  20643  root1eq1  20644  root1cj  20645  cxpeq  20646  angneg  20650  ang180lem1  20656  1cubrlem  20686  1cubr  20687  atandm4  20724  atandmtan  20765  atantayl3  20784  leibpi  20787  log2cnv  20789  wilthlem1  20856  wilthlem2  20857  basellem2  20869  basellem5  20872  basellem9  20876  isnsqf  20923  mule1  20936  mumul  20969  musum  20981  ppiub  20993  dchrptlem1  21053  dchrptlem2  21054  lgsneg  21108  lgsdilem  21111  lgsdir2lem3  21114  lgsdir2lem4  21115  lgsdir2  21117  lgsdir  21119  lgsdi  21121  lgsne0  21122  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem4  21141  lgseisen  21142  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  lgsquad2lem1  21147  lgsquad2lem2  21148  lgsquad3  21150  m1lgs  21151  dchrisum0flblem1  21207  rpvmasum2  21211  vcsubdir  22040  vcm  22055  vcnegneg  22058  vcnegsubdi2  22059  vcsub4  22060  nvinvfval  22126  nvmval2  22129  nvzs  22131  nvmf  22132  nvmdi  22136  nvnegneg  22137  nvsubadd  22141  nvpncan2  22142  nvaddsub4  22147  nvnncan  22149  nvm1  22158  nvdif  22159  nvmtri  22165  nvabs  22167  nvge0  22168  nvnd  22185  imsmetlem  22187  smcnlem  22198  vmcn  22200  ipval2  22208  4ipval2  22209  ipval3  22210  dipcj  22218  dip0r  22221  sspmval  22237  lno0  22262  lnosub  22265  ip0i  22331  ipdirilem  22335  ipasslem2  22338  ipasslem10  22345  dipsubdir  22354  hvsubf  22523  hvsubcl  22525  hvsubid  22533  hv2neg  22535  hvm1neg  22539  hvaddsubval  22540  hvsub4  22544  hvaddsub12  22545  hvpncan  22546  hvaddsubass  22548  hvsubass  22551  hvsubdistr1  22556  hvsubdistr2  22557  hvsubsub4i  22566  hvnegdii  22569  hvsubeq0i  22570  hvsubcan2i  22571  hvaddcani  22572  hvsubaddi  22573  hvaddeq0  22576  hvsubcan  22581  hvsubcan2  22582  hvsub0  22583  his2sub  22599  hisubcomi  22611  normlem0  22616  normlem9  22625  normsubi  22648  norm3difi  22654  normpar2i  22663  hilablo  22667  shsubcl  22728  hhssabloi  22767  shsel3  22822  pjsubii  23185  pjssmii  23188  honegsubi  23304  honegneg  23314  hosubneg  23315  hosubdi  23316  honegdi  23317  honegsubdi  23318  honegsubdi2  23319  hosub4  23321  hosubsub4  23326  hosubeq0i  23334  nmopnegi  23473  lnopsubi  23482  lnophdi  23510  lnophmlem2  23525  lnfnsubi  23554  bdophdi  23605  nmoptri2i  23607  superpos  23862  cdj1i  23941  cdj3lem1  23942  qqhval2lem  24370  subfacval2  24878  subfaclim  24879  m1expevenALT  24910  risefallfac  25345  fallrisefac  25346  fallfac0  25349  0risefac  25359  binomrisefac  25363  axlowdimlem13  25898  rmym1  27012  psgnunilem4  27411  m1expaddsub  27412  psgnuni  27413  psgnpmtr  27424  cnmsgnsubg  27425  cnmsgnbas  27426  cnmsgngrp  27427  psgnghm  27428  proot1ex  27511  expgrowth  27543  m1expeven  27715  climneg  27726
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 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071
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 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-po 4506  df-so 4507  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-ltxr 9130  df-sub 9298  df-neg 9299
  Copyright terms: Public domain W3C validator