Theorem neg1cn 10415

Description: -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
neg1cn	|- -u 1 e. CC

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 9330	. 2 |- 1 e. CC
2	1	negcli 9666	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1757   CCcc 9270   1c1 9273   -ucneg 9586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-po 4630  df-so 4631  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-ltxr 9413  df-sub 9587  df-neg 9588

This theorem is referenced by:  m1expcl2  11873  iseraltlem2  13146  iseraltlem3  13147  fsumneg  13239  incexclem  13284  incexc  13285  bitsfzo  13616  bezoutlem1  13707  psgnunilem4  15985  m1expaddsub  15986  psgnuni  15987  psgnpmtr  15998  psgn0fv0  15999  psgnprfval1  16008  cnmsgnsubg  17851  cnmsgnbas  17852  cnmsgngrp  17853  psgnghm  17854  psgninv  17856  mdetralt  18258  negcncf  20338  dvmptneg  21284  dvlipcn  21310  lhop2  21331  plysubcl  21577  coesub  21611  dgrsub  21626  quotlem  21653  quotcl2  21655  quotdgr  21656  iaa  21678  dvradcnv  21773  efipi  21822  eulerid  21823  sin2pi  21824  sinmpi  21836  cosmpi  21837  sinppi  21838  cosppi  21839  efif1olem2  21886  logneg  21923  lognegb  21925  logtayl  21992  logtayl2  21994  root1id  22079  root1eq1  22080  root1cj  22081  cxpeq  22082  angneg  22086  ang180lem1  22092  1cubrlem  22123  1cubr  22124  atandm4  22161  atandmtan  22202  atantayl3  22221  leibpi  22224  log2cnv  22226  wilthlem1  22293  wilthlem2  22294  basellem2  22306  basellem5  22309  basellem9  22313  isnsqf  22360  mule1  22373  mumul  22406  musum  22418  ppiub  22430  dchrptlem1  22490  dchrptlem2  22491  lgsneg  22545  lgsdilem  22548  lgsdir2lem3  22551  lgsdir2lem4  22552  lgsdir2  22554  lgsdir  22556  lgsdi  22558  lgsne0  22559  lgseisenlem1  22575  lgseisenlem2  22576  lgseisenlem4  22578  lgseisen  22579  lgsquadlem1  22580  lgsquadlem2  22581  lgsquadlem3  22582  lgsquad2lem1  22584  lgsquad2lem2  22585  lgsquad3  22587  m1lgs  22588  dchrisum0flblem1  22644  rpvmasum2  22648  axlowdimlem13  23025  vcsubdir  23759  vcm  23774  vcnegneg  23777  vcnegsubdi2  23778  vcsub4  23779  nvinvfval  23845  nvmval2  23848  nvzs  23850  nvmf  23851  nvmdi  23855  nvnegneg  23856  nvsubadd  23860  nvpncan2  23861  nvaddsub4  23866  nvnncan  23868  nvm1  23877  nvdif  23878  nvmtri  23884  nvabs  23886  nvge0  23887  nvnd  23904  imsmetlem  23906  smcnlem  23917  vmcn  23919  ipval2  23927  4ipval2  23928  ipval3  23929  dipcj  23937  dip0r  23940  sspmval  23956  lno0  23981  lnosub  23984  ip0i  24050  ipdirilem  24054  ipasslem2  24057  ipasslem10  24064  dipsubdir  24073  hvsubf  24242  hvsubcl  24244  hvsubid  24253  hv2neg  24255  hvm1neg  24259  hvaddsubval  24260  hvsub4  24264  hvaddsub12  24265  hvpncan  24266  hvaddsubass  24268  hvsubass  24271  hvsubdistr1  24276  hvsubdistr2  24277  hvsubsub4i  24286  hvnegdii  24289  hvsubeq0i  24290  hvsubcan2i  24291  hvaddcani  24292  hvsubaddi  24293  hvaddeq0  24296  hvsubcan  24301  hvsubcan2  24302  hvsub0  24303  his2sub  24319  hisubcomi  24331  normlem0  24336  normlem9  24345  normsubi  24368  norm3difi  24374  normpar2i  24383  hilablo  24387  shsubcl  24448  hhssabloi  24488  shsel3  24543  pjsubii  24906  pjssmii  24909  honegsubi  25025  honegneg  25035  hosubneg  25036  hosubdi  25037  honegdi  25038  honegsubdi  25039  honegsubdi2  25040  hosub4  25042  hosubsub4  25047  hosubeq0i  25055  nmopnegi  25194  lnopsubi  25203  lnophdi  25231  lnophmlem2  25246  lnfnsubi  25275  bdophdi  25326  nmoptri2i  25328  superpos  25583  cdj1i  25662  cdj3lem1  25663  qqhval2lem  26266  sgnmul  26775  signswch  26812  signlem0  26838  subfacval2  26925  subfaclim  26926  m1expevenALT  26957  risefallfac  27376  fallrisefac  27377  fallfac0  27380  0risefac  27390  binomrisefac  27394  rmym1  29123  proot1ex  29416  expgrowth  29456  m1expeven  29620  climneg  29631  psgnsn  30605