Theorem neg1cn 12276

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 11118	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11478	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2106  ℂcc 11058  1c1 11061  -cneg 11395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-ltxr 11203  df-sub 11396  df-neg 11397

This theorem is referenced by:  m1expcl2  14001  m1expeven  14025  iseraltlem2  15579  iseraltlem3  15580  fsumneg  15683  incexclem  15732  incexc  15733  risefallfac  15918  fallrisefac  15919  fallfac0  15922  0risefac  15932  binomrisefac  15936  n2dvdsm1  16262  m1expo  16268  m1exp1  16269  pwp1fsum  16284  bitsfzo  16326  bezoutlem1  16431  psgnunilem4  19293  m1expaddsub  19294  psgnuni  19295  psgnpmtr  19306  psgn0fv0  19307  psgnsn  19316  psgnprfval1  19318  cnmsgnsubg  21018  cnmsgnbas  21019  cnmsgngrp  21020  psgnghm  21021  psgninv  21023  mdetralt  21994  negcncf  24322  dvmptneg  25367  dvlipcn  25395  lhop2  25416  plysubcl  25620  coesub  25655  dgrsub  25670  quotlem  25697  quotcl2  25699  quotdgr  25700  iaa  25722  dvradcnv  25817  efipi  25867  eulerid  25868  sin2pi  25869  sinmpi  25881  cosmpi  25882  sinppi  25883  cosppi  25884  efif1olem2  25936  logneg  25980  lognegb  25982  logtayl  26052  logtayl2  26054  root1id  26144  root1eq1  26145  root1cj  26146  cxpeq  26147  angneg  26190  ang180lem1  26196  1cubrlem  26228  1cubr  26229  atandm4  26266  atandmtan  26307  atantayl3  26326  leibpi  26329  log2cnv  26331  wilthlem1  26454  wilthlem2  26455  basellem2  26468  basellem5  26471  basellem9  26475  isnsqf  26521  mule1  26534  mumul  26567  musum  26577  ppiub  26589  dchrptlem1  26649  dchrptlem2  26650  lgsneg  26706  lgsdilem  26709  lgsdir2lem3  26712  lgsdir2lem4  26713  lgsdir2  26715  lgsdir  26717  lgsdi  26719  lgsne0  26720  gausslemma2dlem5  26756  gausslemma2d  26759  lgseisenlem1  26760  lgseisenlem2  26761  lgseisenlem4  26763  lgseisen  26764  lgsquadlem1  26765  lgsquadlem2  26766  lgsquadlem3  26767  lgsquad2lem1  26769  lgsquad2lem2  26770  lgsquad3  26772  m1lgs  26773  addsqn2reu  26826  addsqrexnreu  26827  dchrisum0flblem1  26893  rpvmasum2  26897  axlowdimlem13  27966  vcm  29581  nvinvfval  29645  nvmval2  29648  nvmf  29650  nvmdi  29653  nvnegneg  29654  nvpncan2  29658  nvaddsub4  29662  nvm1  29670  nvdif  29671  nvmtri  29676  nvabs  29677  nvge0  29678  nvnd  29693  imsmetlem  29695  smcnlem  29702  vmcn  29704  ipval2  29712  4ipval2  29713  ipval3  29714  dipcj  29719  dip0r  29722  sspmval  29738  lno0  29761  lnosub  29764  ip0i  29830  ipdirilem  29834  ipasslem2  29837  ipasslem10  29844  dipsubdir  29853  hvsubf  30020  hvsubcl  30022  hvsubid  30031  hv2neg  30033  hvm1neg  30037  hvaddsubval  30038  hvsub4  30042  hvaddsub12  30043  hvpncan  30044  hvaddsubass  30046  hvsubass  30049  hvsubdistr1  30054  hvsubdistr2  30055  hvsubsub4i  30064  hvnegdii  30067  hvsubeq0i  30068  hvsubcan2i  30069  hvaddcani  30070  hvsubaddi  30071  hvaddeq0  30074  hvsubcan  30079  hvsubcan2  30080  hvsub0  30081  his2sub  30097  hisubcomi  30109  normlem0  30114  normlem9  30123  normsubi  30146  norm3difi  30152  normpar2i  30161  hilablo  30165  shsubcl  30225  hhssabloilem  30266  shsel3  30320  pjsubii  30683  pjssmii  30686  honegsubi  30801  honegneg  30811  hosubneg  30812  hosubdi  30813  honegdi  30814  honegsubdi  30815  honegsubdi2  30816  hosub4  30818  hosubsub4  30823  hosubeq0i  30831  nmopnegi  30970  lnopsubi  30979  lnophdi  31007  lnophmlem2  31022  lnfnsubi  31051  bdophdi  31102  nmoptri2i  31104  superpos  31359  cdj1i  31438  cdj3lem1  31439  psgnid  32016  psgnfzto1st  32024  cnmsgn0g  32065  altgnsg  32068  qqhval2lem  32651  sgnmul  33231  signswch  33262  signlem0  33288  subfacval2  33868  subfaclim  33869  quad3  34345  fwddifn0  34825  fwddifnp1  34826  lcmineqlem1  40559  lcmineqlem2  40560  lcmineqlem8  40566  2xp3dxp2ge1d  40687  negexpidd  41063  rmym1  41317  proot1ex  41586  sqrtcval2  42036  expgrowth  42737  climneg  43971  dirkertrigeqlem1  44459  dirkertrigeqlem3  44461  fourierdlem24  44492  sqwvfourb  44590  fourierswlem  44591  fouriersw  44592  2pwp1prm  45901  3exp4mod41  45928  41prothprmlem2  45930  m1expevenALTV  45959  m1expoddALTV  45960  0nodd  46224  altgsumbc  46548  altgsumbcALT  46549