Theorem neg1cn 12178

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

Assertion

Ref	Expression
neg1cn	⊢ -1 ∈ ℂ

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 11133	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11497	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2109  ℂcc 11073  1c1 11076  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-neg 11415

This theorem is referenced by:  m1expcl2  14057  m1expeven  14081  iseraltlem2  15656  iseraltlem3  15657  fsumneg  15760  incexclem  15809  incexc  15810  risefallfac  15997  fallrisefac  15998  fallfac0  16001  0risefac  16011  binomrisefac  16015  n2dvdsm1  16346  m1expo  16352  m1exp1  16353  pwp1fsum  16368  bitsfzo  16412  bezoutlem1  16516  psgnunilem4  19434  m1expaddsub  19435  psgnuni  19436  psgnpmtr  19447  psgn0fv0  19448  psgnsn  19457  psgnprfval1  19459  cnmsgnsubg  21493  cnmsgnbas  21494  cnmsgngrp  21495  psgnghm  21496  psgninv  21498  mdetralt  22502  negcncf  24822  negcncfOLD  24823  dvmptneg  25877  dvlipcn  25906  lhop2  25927  plysubcl  26134  coesub  26169  dgrsub  26185  quotlem  26215  quotcl2  26217  quotdgr  26218  iaa  26240  dvradcnv  26337  efipi  26389  eulerid  26390  sin2pi  26391  sinmpi  26403  cosmpi  26404  sinppi  26405  cosppi  26406  efif1olem2  26459  logneg  26504  lognegb  26506  logtayl  26576  logtayl2  26578  root1id  26671  root1eq1  26672  root1cj  26673  cxpeq  26674  angneg  26720  ang180lem1  26726  1cubrlem  26758  1cubr  26759  atandm4  26796  atandmtan  26837  atantayl3  26856  leibpi  26859  log2cnv  26861  wilthlem1  26985  wilthlem2  26986  basellem2  26999  basellem5  27002  basellem9  27006  isnsqf  27052  mule1  27065  mumul  27098  musum  27108  ppiub  27122  dchrptlem1  27182  dchrptlem2  27183  lgsneg  27239  lgsdilem  27242  lgsdir2lem3  27245  lgsdir2lem4  27246  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsne0  27253  gausslemma2dlem5  27289  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem1  27302  lgsquad2lem2  27303  lgsquad3  27305  m1lgs  27306  addsqn2reu  27359  addsqrexnreu  27360  dchrisum0flblem1  27426  rpvmasum2  27430  axlowdimlem13  28888  vcm  30512  nvinvfval  30576  nvmval2  30579  nvmf  30581  nvmdi  30584  nvnegneg  30585  nvpncan2  30589  nvaddsub4  30593  nvm1  30601  nvdif  30602  nvmtri  30607  nvabs  30608  nvge0  30609  nvnd  30624  imsmetlem  30626  smcnlem  30633  vmcn  30635  ipval2  30643  4ipval2  30644  ipval3  30645  dipcj  30650  dip0r  30653  sspmval  30669  lno0  30692  lnosub  30695  ip0i  30761  ipdirilem  30765  ipasslem2  30768  ipasslem10  30775  dipsubdir  30784  hvsubf  30951  hvsubcl  30953  hvsubid  30962  hv2neg  30964  hvm1neg  30968  hvaddsubval  30969  hvsub4  30973  hvaddsub12  30974  hvpncan  30975  hvaddsubass  30977  hvsubass  30980  hvsubdistr1  30985  hvsubdistr2  30986  hvsubsub4i  30995  hvnegdii  30998  hvsubeq0i  30999  hvsubcan2i  31000  hvaddcani  31001  hvsubaddi  31002  hvaddeq0  31005  hvsubcan  31010  hvsubcan2  31011  hvsub0  31012  his2sub  31028  hisubcomi  31040  normlem0  31045  normlem9  31054  normsubi  31077  norm3difi  31083  normpar2i  31092  hilablo  31096  shsubcl  31156  hhssabloilem  31197  shsel3  31251  pjsubii  31614  pjssmii  31617  honegsubi  31732  honegneg  31742  hosubneg  31743  hosubdi  31744  honegdi  31745  honegsubdi  31746  honegsubdi2  31747  hosub4  31749  hosubsub4  31754  hosubeq0i  31762  nmopnegi  31901  lnopsubi  31910  lnophdi  31938  lnophmlem2  31953  lnfnsubi  31982  bdophdi  32033  nmoptri2i  32035  superpos  32290  cdj1i  32369  cdj3lem1  32370  quad3d  32680  sgnmul  32767  psgnid  33061  psgnfzto1st  33069  cnmsgn0g  33110  altgnsg  33113  qqhval2lem  33978  signswch  34559  signlem0  34585  subfacval2  35181  subfaclim  35182  quad3  35664  fwddifn0  36159  fwddifnp1  36160  lcmineqlem1  42024  lcmineqlem2  42025  lcmineqlem8  42031  readvrec  42357  negexpidd  42677  rmym1  42931  proot1ex  43192  sqrtcval2  43638  expgrowth  44331  climneg  45615  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  fourierdlem24  46136  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  2pwp1prm  47594  3exp4mod41  47621  41prothprmlem2  47623  m1expevenALTV  47652  m1expoddALTV  47653  0nodd  48162  altgsumbc  48344  altgsumbcALT  48345