Theorem neg1cn 12017

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 10860	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11219	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2108  ℂcc 10800  1c1 10803  -cneg 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137  df-neg 11138

This theorem is referenced by:  m1expcl2  13732  m1expeven  13758  iseraltlem2  15322  iseraltlem3  15323  fsumneg  15427  incexclem  15476  incexc  15477  risefallfac  15662  fallrisefac  15663  fallfac0  15666  0risefac  15676  binomrisefac  15680  n2dvdsm1  16006  m1expo  16012  m1exp1  16013  pwp1fsum  16028  bitsfzo  16070  bezoutlem1  16175  psgnunilem4  19020  m1expaddsub  19021  psgnuni  19022  psgnpmtr  19033  psgn0fv0  19034  psgnsn  19043  psgnprfval1  19045  cnmsgnsubg  20694  cnmsgnbas  20695  cnmsgngrp  20696  psgnghm  20697  psgninv  20699  mdetralt  21665  negcncf  23991  dvmptneg  25035  dvlipcn  25063  lhop2  25084  plysubcl  25288  coesub  25323  dgrsub  25338  quotlem  25365  quotcl2  25367  quotdgr  25368  iaa  25390  dvradcnv  25485  efipi  25535  eulerid  25536  sin2pi  25537  sinmpi  25549  cosmpi  25550  sinppi  25551  cosppi  25552  efif1olem2  25604  logneg  25648  lognegb  25650  logtayl  25720  logtayl2  25722  root1id  25812  root1eq1  25813  root1cj  25814  cxpeq  25815  angneg  25858  ang180lem1  25864  1cubrlem  25896  1cubr  25897  atandm4  25934  atandmtan  25975  atantayl3  25994  leibpi  25997  log2cnv  25999  wilthlem1  26122  wilthlem2  26123  basellem2  26136  basellem5  26139  basellem9  26143  isnsqf  26189  mule1  26202  mumul  26235  musum  26245  ppiub  26257  dchrptlem1  26317  dchrptlem2  26318  lgsneg  26374  lgsdilem  26377  lgsdir2lem3  26380  lgsdir2lem4  26381  lgsdir2  26383  lgsdir  26385  lgsdi  26387  lgsne0  26388  gausslemma2dlem5  26424  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem1  26437  lgsquad2lem2  26438  lgsquad3  26440  m1lgs  26441  addsqn2reu  26494  addsqrexnreu  26495  dchrisum0flblem1  26561  rpvmasum2  26565  axlowdimlem13  27225  vcm  28839  nvinvfval  28903  nvmval2  28906  nvmf  28908  nvmdi  28911  nvnegneg  28912  nvpncan2  28916  nvaddsub4  28920  nvm1  28928  nvdif  28929  nvmtri  28934  nvabs  28935  nvge0  28936  nvnd  28951  imsmetlem  28953  smcnlem  28960  vmcn  28962  ipval2  28970  4ipval2  28971  ipval3  28972  dipcj  28977  dip0r  28980  sspmval  28996  lno0  29019  lnosub  29022  ip0i  29088  ipdirilem  29092  ipasslem2  29095  ipasslem10  29102  dipsubdir  29111  hvsubf  29278  hvsubcl  29280  hvsubid  29289  hv2neg  29291  hvm1neg  29295  hvaddsubval  29296  hvsub4  29300  hvaddsub12  29301  hvpncan  29302  hvaddsubass  29304  hvsubass  29307  hvsubdistr1  29312  hvsubdistr2  29313  hvsubsub4i  29322  hvnegdii  29325  hvsubeq0i  29326  hvsubcan2i  29327  hvaddcani  29328  hvsubaddi  29329  hvaddeq0  29332  hvsubcan  29337  hvsubcan2  29338  hvsub0  29339  his2sub  29355  hisubcomi  29367  normlem0  29372  normlem9  29381  normsubi  29404  norm3difi  29410  normpar2i  29419  hilablo  29423  shsubcl  29483  hhssabloilem  29524  shsel3  29578  pjsubii  29941  pjssmii  29944  honegsubi  30059  honegneg  30069  hosubneg  30070  hosubdi  30071  honegdi  30072  honegsubdi  30073  honegsubdi2  30074  hosub4  30076  hosubsub4  30081  hosubeq0i  30089  nmopnegi  30228  lnopsubi  30237  lnophdi  30265  lnophmlem2  30280  lnfnsubi  30309  bdophdi  30360  nmoptri2i  30362  superpos  30617  cdj1i  30696  cdj3lem1  30697  psgnid  31266  psgnfzto1st  31274  cnmsgn0g  31315  altgnsg  31318  qqhval2lem  31831  sgnmul  32409  signswch  32440  signlem0  32466  subfacval2  33049  subfaclim  33050  quad3  33528  fwddifn0  34393  fwddifnp1  34394  lcmineqlem1  39965  lcmineqlem2  39966  lcmineqlem8  39972  2xp3dxp2ge1d  40090  negexpidd  40420  rmym1  40673  proot1ex  40942  sqrtcval2  41139  expgrowth  41842  climneg  43041  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  fourierdlem24  43562  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  2pwp1prm  44929  3exp4mod41  44956  41prothprmlem2  44958  m1expevenALTV  44987  m1expoddALTV  44988  0nodd  45252  altgsumbc  45576  altgsumbcALT  45577