Theorem neg1cn 11738

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 10581	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 10940	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 10521  1c1 10524  -cneg 10857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-ltxr 10666  df-sub 10858  df-neg 10859

This theorem is referenced by:  m1expcl2  13441  m1expeven  13466  iseraltlem2  15024  iseraltlem3  15025  fsumneg  15127  incexclem  15176  incexc  15177  risefallfac  15363  fallrisefac  15364  fallfac0  15367  0risefac  15377  binomrisefac  15381  n2dvdsm1  15703  m1expo  15709  m1exp1  15710  pwp1fsum  15725  bitsfzo  15767  bezoutlem1  15870  psgnunilem4  18608  m1expaddsub  18609  psgnuni  18610  psgnpmtr  18621  psgn0fv0  18622  psgnsn  18631  psgnprfval1  18633  cnmsgnsubg  20704  cnmsgnbas  20705  cnmsgngrp  20706  psgnghm  20707  psgninv  20709  mdetralt  21200  negcncf  23509  dvmptneg  24548  dvlipcn  24576  lhop2  24597  plysubcl  24798  coesub  24833  dgrsub  24848  quotlem  24875  quotcl2  24877  quotdgr  24878  iaa  24900  dvradcnv  24995  efipi  25045  eulerid  25046  sin2pi  25047  sinmpi  25059  cosmpi  25060  sinppi  25061  cosppi  25062  efif1olem2  25113  logneg  25157  lognegb  25159  logtayl  25229  logtayl2  25231  root1id  25321  root1eq1  25322  root1cj  25323  cxpeq  25324  angneg  25367  ang180lem1  25373  1cubrlem  25405  1cubr  25406  atandm4  25443  atandmtan  25484  atantayl3  25503  leibpi  25506  log2cnv  25508  wilthlem1  25631  wilthlem2  25632  basellem2  25645  basellem5  25648  basellem9  25652  isnsqf  25698  mule1  25711  mumul  25744  musum  25754  ppiub  25766  dchrptlem1  25826  dchrptlem2  25827  lgsneg  25883  lgsdilem  25886  lgsdir2lem3  25889  lgsdir2lem4  25890  lgsdir2  25892  lgsdir  25894  lgsdi  25896  lgsne0  25897  gausslemma2dlem5  25933  gausslemma2d  25936  lgseisenlem1  25937  lgseisenlem2  25938  lgseisenlem4  25940  lgseisen  25941  lgsquadlem1  25942  lgsquadlem2  25943  lgsquadlem3  25944  lgsquad2lem1  25946  lgsquad2lem2  25947  lgsquad3  25949  m1lgs  25950  addsqn2reu  26003  addsqrexnreu  26004  dchrisum0flblem1  26070  rpvmasum2  26074  axlowdimlem13  26726  vcm  28337  nvinvfval  28401  nvmval2  28404  nvmf  28406  nvmdi  28409  nvnegneg  28410  nvpncan2  28414  nvaddsub4  28418  nvm1  28426  nvdif  28427  nvmtri  28432  nvabs  28433  nvge0  28434  nvnd  28449  imsmetlem  28451  smcnlem  28458  vmcn  28460  ipval2  28468  4ipval2  28469  ipval3  28470  dipcj  28475  dip0r  28478  sspmval  28494  lno0  28517  lnosub  28520  ip0i  28586  ipdirilem  28590  ipasslem2  28593  ipasslem10  28600  dipsubdir  28609  hvsubf  28776  hvsubcl  28778  hvsubid  28787  hv2neg  28789  hvm1neg  28793  hvaddsubval  28794  hvsub4  28798  hvaddsub12  28799  hvpncan  28800  hvaddsubass  28802  hvsubass  28805  hvsubdistr1  28810  hvsubdistr2  28811  hvsubsub4i  28820  hvnegdii  28823  hvsubeq0i  28824  hvsubcan2i  28825  hvaddcani  28826  hvsubaddi  28827  hvaddeq0  28830  hvsubcan  28835  hvsubcan2  28836  hvsub0  28837  his2sub  28853  hisubcomi  28865  normlem0  28870  normlem9  28879  normsubi  28902  norm3difi  28908  normpar2i  28917  hilablo  28921  shsubcl  28981  hhssabloilem  29022  shsel3  29076  pjsubii  29439  pjssmii  29442  honegsubi  29557  honegneg  29567  hosubneg  29568  hosubdi  29569  honegdi  29570  honegsubdi  29571  honegsubdi2  29572  hosub4  29574  hosubsub4  29579  hosubeq0i  29587  nmopnegi  29726  lnopsubi  29735  lnophdi  29763  lnophmlem2  29778  lnfnsubi  29807  bdophdi  29858  nmoptri2i  29860  superpos  30115  cdj1i  30194  cdj3lem1  30195  psgnid  30746  psgnfzto1st  30754  cnmsgn0g  30795  altgnsg  30798  qqhval2lem  31229  sgnmul  31807  signswch  31838  signlem0  31864  subfacval2  32441  subfaclim  32442  quad3  32920  fwddifn0  33632  fwddifnp1  33633  lcmineqlem1  39156  lcmineqlem2  39157  2xp3dxp2ge1d  39172  negexpidd  39371  rmym1  39624  proot1ex  39893  expgrowth  40757  climneg  41981  dirkertrigeqlem1  42473  dirkertrigeqlem3  42475  fourierdlem24  42506  sqwvfourb  42604  fourierswlem  42605  fouriersw  42606  2pwp1prm  43836  3exp4mod41  43866  41prothprmlem2  43868  m1expevenALTV  43897  m1expoddALTV  43898  0nodd  44162  altgsumbc  44485  altgsumbcALT  44486