Theorem neg1cn 10535

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 9450	. 2 |- 1 e. CC
2	1	negcli 9786	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1758   CCcc 9390   1c1 9393   -ucneg 9706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-po 4748  df-so 4749  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-pnf 9530  df-mnf 9531  df-ltxr 9533  df-sub 9707  df-neg 9708

This theorem is referenced by:  m1expcl2  12003  iseraltlem2  13277  iseraltlem3  13278  fsumneg  13371  incexclem  13416  incexc  13417  bitsfzo  13748  bezoutlem1  13839  psgnunilem4  16121  m1expaddsub  16122  psgnuni  16123  psgnpmtr  16134  psgn0fv0  16135  psgnsn  16144  psgnprfval1  16146  cnmsgnsubg  18131  cnmsgnbas  18132  cnmsgngrp  18133  psgnghm  18134  psgninv  18136  mdetralt  18545  negcncf  20625  dvmptneg  21572  dvlipcn  21598  lhop2  21619  plysubcl  21822  coesub  21856  dgrsub  21871  quotlem  21898  quotcl2  21900  quotdgr  21901  iaa  21923  dvradcnv  22018  efipi  22067  eulerid  22068  sin2pi  22069  sinmpi  22081  cosmpi  22082  sinppi  22083  cosppi  22084  efif1olem2  22131  logneg  22168  lognegb  22170  logtayl  22237  logtayl2  22239  root1id  22324  root1eq1  22325  root1cj  22326  cxpeq  22327  angneg  22331  ang180lem1  22337  1cubrlem  22368  1cubr  22369  atandm4  22406  atandmtan  22447  atantayl3  22466  leibpi  22469  log2cnv  22471  wilthlem1  22538  wilthlem2  22539  basellem2  22551  basellem5  22554  basellem9  22558  isnsqf  22605  mule1  22618  mumul  22651  musum  22663  ppiub  22675  dchrptlem1  22735  dchrptlem2  22736  lgsneg  22790  lgsdilem  22793  lgsdir2lem3  22796  lgsdir2lem4  22797  lgsdir2  22799  lgsdir  22801  lgsdi  22803  lgsne0  22804  lgseisenlem1  22820  lgseisenlem2  22821  lgseisenlem4  22823  lgseisen  22824  lgsquadlem1  22825  lgsquadlem2  22826  lgsquadlem3  22827  lgsquad2lem1  22829  lgsquad2lem2  22830  lgsquad3  22832  m1lgs  22833  dchrisum0flblem1  22889  rpvmasum2  22893  axlowdimlem13  23351  vcsubdir  24085  vcm  24100  vcnegneg  24103  vcnegsubdi2  24104  vcsub4  24105  nvinvfval  24171  nvmval2  24174  nvzs  24176  nvmf  24177  nvmdi  24181  nvnegneg  24182  nvsubadd  24186  nvpncan2  24187  nvaddsub4  24192  nvnncan  24194  nvm1  24203  nvdif  24204  nvmtri  24210  nvabs  24212  nvge0  24213  nvnd  24230  imsmetlem  24232  smcnlem  24243  vmcn  24245  ipval2  24253  4ipval2  24254  ipval3  24255  dipcj  24263  dip0r  24266  sspmval  24282  lno0  24307  lnosub  24310  ip0i  24376  ipdirilem  24380  ipasslem2  24383  ipasslem10  24390  dipsubdir  24399  hvsubf  24568  hvsubcl  24570  hvsubid  24579  hv2neg  24581  hvm1neg  24585  hvaddsubval  24586  hvsub4  24590  hvaddsub12  24591  hvpncan  24592  hvaddsubass  24594  hvsubass  24597  hvsubdistr1  24602  hvsubdistr2  24603  hvsubsub4i  24612  hvnegdii  24615  hvsubeq0i  24616  hvsubcan2i  24617  hvaddcani  24618  hvsubaddi  24619  hvaddeq0  24622  hvsubcan  24627  hvsubcan2  24628  hvsub0  24629  his2sub  24645  hisubcomi  24657  normlem0  24662  normlem9  24671  normsubi  24694  norm3difi  24700  normpar2i  24709  hilablo  24713  shsubcl  24774  hhssabloi  24814  shsel3  24869  pjsubii  25232  pjssmii  25235  honegsubi  25351  honegneg  25361  hosubneg  25362  hosubdi  25363  honegdi  25364  honegsubdi  25365  honegsubdi2  25366  hosub4  25368  hosubsub4  25373  hosubeq0i  25381  nmopnegi  25520  lnopsubi  25529  lnophdi  25557  lnophmlem2  25572  lnfnsubi  25601  bdophdi  25652  nmoptri2i  25654  superpos  25909  cdj1i  25988  cdj3lem1  25989  qqhval2lem  26554  sgnmul  27068  signswch  27105  signlem0  27131  subfacval2  27218  subfaclim  27219  m1expevenALT  27250  risefallfac  27670  fallrisefac  27671  fallfac0  27674  0risefac  27684  binomrisefac  27688  rmym1  29423  proot1ex  29716  expgrowth  29756  m1expeven  29919  climneg  29930  altgsumbc  30896  altgsumbcALT  30897