Theorem neg1cn 12144

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 11098	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11463	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 11038  1c1 11041  -cneg 11379

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185  df-sub 11380  df-neg 11381

This theorem is referenced by:  m1expcl2  14022  m1expeven  14046  iseraltlem2  15620  iseraltlem3  15621  fsumneg  15724  incexclem  15773  incexc  15774  risefallfac  15961  fallrisefac  15962  fallfac0  15965  0risefac  15975  binomrisefac  15979  n2dvdsm1  16310  m1expo  16316  m1exp1  16317  pwp1fsum  16332  bitsfzo  16376  bezoutlem1  16480  psgnunilem4  19443  m1expaddsub  19444  psgnuni  19445  psgnpmtr  19456  psgn0fv0  19457  psgnsn  19466  psgnprfval1  19468  cnmsgnsubg  21549  cnmsgnbas  21550  cnmsgngrp  21551  psgnghm  21552  psgninv  21554  mdetralt  22569  negcncf  24888  negcncfOLD  24889  dvmptneg  25943  dvlipcn  25972  lhop2  25993  plysubcl  26200  coesub  26235  dgrsub  26251  quotlem  26281  quotcl2  26283  quotdgr  26284  iaa  26306  dvradcnv  26403  efipi  26455  eulerid  26456  sin2pi  26457  sinmpi  26469  cosmpi  26470  sinppi  26471  cosppi  26472  efif1olem2  26525  logneg  26570  lognegb  26572  logtayl  26642  logtayl2  26644  root1id  26737  root1eq1  26738  root1cj  26739  cxpeq  26740  angneg  26786  ang180lem1  26792  1cubrlem  26824  1cubr  26825  atandm4  26862  atandmtan  26903  atantayl3  26922  leibpi  26925  log2cnv  26927  wilthlem1  27051  wilthlem2  27052  basellem2  27065  basellem5  27068  basellem9  27072  isnsqf  27118  mule1  27131  mumul  27164  musum  27174  ppiub  27188  dchrptlem1  27248  dchrptlem2  27249  lgsneg  27305  lgsdilem  27308  lgsdir2lem3  27311  lgsdir2lem4  27312  lgsdir2  27314  lgsdir  27316  lgsdi  27318  lgsne0  27319  gausslemma2dlem5  27355  gausslemma2d  27358  lgseisenlem1  27359  lgseisenlem2  27360  lgseisenlem4  27362  lgseisen  27363  lgsquadlem1  27364  lgsquadlem2  27365  lgsquadlem3  27366  lgsquad2lem1  27368  lgsquad2lem2  27369  lgsquad3  27371  m1lgs  27372  addsqn2reu  27425  addsqrexnreu  27426  dchrisum0flblem1  27492  rpvmasum2  27496  axlowdimlem13  29045  vcm  30670  nvinvfval  30734  nvmval2  30737  nvmf  30739  nvmdi  30742  nvnegneg  30743  nvpncan2  30747  nvaddsub4  30751  nvm1  30759  nvdif  30760  nvmtri  30765  nvabs  30766  nvge0  30767  nvnd  30782  imsmetlem  30784  smcnlem  30791  vmcn  30793  ipval2  30801  4ipval2  30802  ipval3  30803  dipcj  30808  dip0r  30811  sspmval  30827  lno0  30850  lnosub  30853  ip0i  30919  ipdirilem  30923  ipasslem2  30926  ipasslem10  30933  dipsubdir  30942  hvsubf  31109  hvsubcl  31111  hvsubid  31120  hv2neg  31122  hvm1neg  31126  hvaddsubval  31127  hvsub4  31131  hvaddsub12  31132  hvpncan  31133  hvaddsubass  31135  hvsubass  31138  hvsubdistr1  31143  hvsubdistr2  31144  hvsubsub4i  31153  hvnegdii  31156  hvsubeq0i  31157  hvsubcan2i  31158  hvaddcani  31159  hvsubaddi  31160  hvaddeq0  31163  hvsubcan  31168  hvsubcan2  31169  hvsub0  31170  his2sub  31186  hisubcomi  31198  normlem0  31203  normlem9  31212  normsubi  31235  norm3difi  31241  normpar2i  31250  hilablo  31254  shsubcl  31314  hhssabloilem  31355  shsel3  31409  pjsubii  31772  pjssmii  31775  honegsubi  31890  honegneg  31900  hosubneg  31901  hosubdi  31902  honegdi  31903  honegsubdi  31904  honegsubdi2  31905  hosub4  31907  hosubsub4  31912  hosubeq0i  31920  nmopnegi  32059  lnopsubi  32068  lnophdi  32096  lnophmlem2  32111  lnfnsubi  32140  bdophdi  32191  nmoptri2i  32193  superpos  32448  cdj1i  32527  cdj3lem1  32528  quad3d  32846  sgnmul  32933  psgnid  33197  psgnfzto1st  33205  cnmsgn0g  33246  altgnsg  33249  qqhval2lem  34165  signswch  34745  signlem0  34771  subfacval2  35409  subfaclim  35410  quad3  35892  fwddifn0  36386  fwddifnp1  36387  lcmineqlem1  42428  lcmineqlem2  42429  lcmineqlem8  42435  readvrec  42761  negexpidd  43068  rmym1  43321  proot1ex  43582  sqrtcval2  44027  expgrowth  44720  climneg  45999  dirkertrigeqlem1  46485  dirkertrigeqlem3  46487  fourierdlem24  46518  sqwvfourb  46616  fourierswlem  46617  fouriersw  46618  2pwp1prm  47978  3exp4mod41  48005  41prothprmlem2  48007  m1expevenALTV  48036  m1expoddALTV  48037  0nodd  48559  altgsumbc  48741  altgsumbcALT  48742