Theorem neg1cn 10417

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 9332	. 2 |- 1 e. CC
2	1	negcli 9668	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1756   CCcc 9272   1c1 9275   -ucneg 9588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415  df-sub 9589  df-neg 9590

This theorem is referenced by:  m1expcl2  11879  iseraltlem2  13152  iseraltlem3  13153  fsumneg  13246  incexclem  13291  incexc  13292  bitsfzo  13623  bezoutlem1  13714  psgnunilem4  15994  m1expaddsub  15995  psgnuni  15996  psgnpmtr  16007  psgn0fv0  16008  psgnprfval1  16017  cnmsgnsubg  17982  cnmsgnbas  17983  cnmsgngrp  17984  psgnghm  17985  psgninv  17987  mdetralt  18389  negcncf  20469  dvmptneg  21415  dvlipcn  21441  lhop2  21462  plysubcl  21665  coesub  21699  dgrsub  21714  quotlem  21741  quotcl2  21743  quotdgr  21744  iaa  21766  dvradcnv  21861  efipi  21910  eulerid  21911  sin2pi  21912  sinmpi  21924  cosmpi  21925  sinppi  21926  cosppi  21927  efif1olem2  21974  logneg  22011  lognegb  22013  logtayl  22080  logtayl2  22082  root1id  22167  root1eq1  22168  root1cj  22169  cxpeq  22170  angneg  22174  ang180lem1  22180  1cubrlem  22211  1cubr  22212  atandm4  22249  atandmtan  22290  atantayl3  22309  leibpi  22312  log2cnv  22314  wilthlem1  22381  wilthlem2  22382  basellem2  22394  basellem5  22397  basellem9  22401  isnsqf  22448  mule1  22461  mumul  22494  musum  22506  ppiub  22518  dchrptlem1  22578  dchrptlem2  22579  lgsneg  22633  lgsdilem  22636  lgsdir2lem3  22639  lgsdir2lem4  22640  lgsdir2  22642  lgsdir  22644  lgsdi  22646  lgsne0  22647  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem4  22666  lgseisen  22667  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  lgsquad2lem1  22672  lgsquad2lem2  22673  lgsquad3  22675  m1lgs  22676  dchrisum0flblem1  22732  rpvmasum2  22736  axlowdimlem13  23151  vcsubdir  23885  vcm  23900  vcnegneg  23903  vcnegsubdi2  23904  vcsub4  23905  nvinvfval  23971  nvmval2  23974  nvzs  23976  nvmf  23977  nvmdi  23981  nvnegneg  23982  nvsubadd  23986  nvpncan2  23987  nvaddsub4  23992  nvnncan  23994  nvm1  24003  nvdif  24004  nvmtri  24010  nvabs  24012  nvge0  24013  nvnd  24030  imsmetlem  24032  smcnlem  24043  vmcn  24045  ipval2  24053  4ipval2  24054  ipval3  24055  dipcj  24063  dip0r  24066  sspmval  24082  lno0  24107  lnosub  24110  ip0i  24176  ipdirilem  24180  ipasslem2  24183  ipasslem10  24190  dipsubdir  24199  hvsubf  24368  hvsubcl  24370  hvsubid  24379  hv2neg  24381  hvm1neg  24385  hvaddsubval  24386  hvsub4  24390  hvaddsub12  24391  hvpncan  24392  hvaddsubass  24394  hvsubass  24397  hvsubdistr1  24402  hvsubdistr2  24403  hvsubsub4i  24412  hvnegdii  24415  hvsubeq0i  24416  hvsubcan2i  24417  hvaddcani  24418  hvsubaddi  24419  hvaddeq0  24422  hvsubcan  24427  hvsubcan2  24428  hvsub0  24429  his2sub  24445  hisubcomi  24457  normlem0  24462  normlem9  24471  normsubi  24494  norm3difi  24500  normpar2i  24509  hilablo  24513  shsubcl  24574  hhssabloi  24614  shsel3  24669  pjsubii  25032  pjssmii  25035  honegsubi  25151  honegneg  25161  hosubneg  25162  hosubdi  25163  honegdi  25164  honegsubdi  25165  honegsubdi2  25166  hosub4  25168  hosubsub4  25173  hosubeq0i  25181  nmopnegi  25320  lnopsubi  25329  lnophdi  25357  lnophmlem2  25372  lnfnsubi  25401  bdophdi  25452  nmoptri2i  25454  superpos  25709  cdj1i  25788  cdj3lem1  25789  qqhval2lem  26362  sgnmul  26877  signswch  26914  signlem0  26940  subfacval2  27027  subfaclim  27028  m1expevenALT  27059  risefallfac  27478  fallrisefac  27479  fallfac0  27482  0risefac  27492  binomrisefac  27496  rmym1  29229  proot1ex  29522  expgrowth  29562  m1expeven  29725  climneg  29736  altgsumbc  30700  altgsumbcALT  30701  psgnsn  30722