Theorem neg1cn 12182

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 11501	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2144  ℂcc 11073  1c1 11076  -cneg 11417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  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 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-sub 11418  df-neg 11419

This theorem is referenced by:  m1expcl2  14100  m1expeven  14124  sgnmul  15122  iseraltlem2  15712  iseraltlem3  15713  fsumneg  15816  incexclem  15868  incexc  15869  risefallfac  16056  fallrisefac  16057  fallfac0  16060  0risefac  16070  binomrisefac  16074  n2dvdsm1  16405  m1expo  16411  m1exp1  16412  pwp1fsum  16427  bitsfzo  16471  bezoutlem1  16575  psgnunilem4  19539  m1expaddsub  19540  psgnuni  19541  psgnpmtr  19552  psgn0fv0  19553  psgnsn  19562  psgnprfval1  19564  cnmsgnsubg  21631  cnmsgnbas  21632  cnmsgngrp  21633  psgnghm  21634  psgninv  21636  mdetralt  22670  negcncf  24986  dvmptneg  26030  dvlipcn  26058  lhop2  26079  plysubcl  26284  coesub  26319  dgrsub  26334  quotlem  26366  quotcl2  26368  quotdgr  26369  iaa  26391  dvradcnv  26486  efipi  26540  eulerid  26541  sin2pi  26542  sinmpi  26554  cosmpi  26555  sinppi  26556  cosppi  26557  efif1olem2  26610  logneg  26655  lognegb  26657  logtayl  26727  logtayl2  26729  root1id  26821  root1eq1  26822  root1cj  26823  cxpeq  26824  angneg  26870  ang180lem1  26876  1cubrlem  26908  1cubr  26909  atandm4  26946  atandmtan  26987  atantayl3  27006  leibpi  27009  log2cnv  27011  wilthlem1  27134  wilthlem2  27135  basellem2  27148  basellem5  27151  basellem9  27155  isnsqf  27201  mule1  27214  mumul  27247  musum  27257  ppiub  27270  dchrptlem1  27330  dchrptlem2  27331  lgsneg  27387  lgsdilem  27390  lgsdir2lem3  27393  lgsdir2lem4  27394  lgsdir2  27396  lgsdir  27398  lgsdi  27400  lgsne0  27401  gausslemma2dlem5  27437  gausslemma2d  27440  lgseisenlem1  27441  lgseisenlem2  27442  lgseisenlem4  27444  lgseisen  27445  lgsquadlem1  27446  lgsquadlem2  27447  lgsquadlem3  27448  lgsquad2lem1  27450  lgsquad2lem2  27451  lgsquad3  27453  m1lgs  27454  addsqn2reu  27507  addsqrexnreu  27508  dchrisum0flblem1  27574  rpvmasum2  27578  axlowdimlem13  29157  vcm  30781  nvinvfval  30845  nvmval2  30848  nvmf  30850  nvmdi  30853  nvnegneg  30854  nvpncan2  30858  nvaddsub4  30862  nvm1  30870  nvdif  30871  nvmtri  30876  nvabs  30877  nvge0  30878  nvnd  30893  imsmetlem  30895  smcnlem  30902  vmcn  30904  ipval2  30912  4ipval2  30913  ipval3  30914  dipcj  30919  dip0r  30922  sspmval  30938  lno0  30961  lnosub  30964  ip0i  31030  ipdirilem  31034  ipasslem2  31037  ipasslem10  31044  dipsubdir  31053  hvsubf  31220  hvsubcl  31222  hvsubid  31231  hv2neg  31233  hvm1neg  31237  hvaddsubval  31238  hvsub4  31242  hvaddsub12  31243  hvpncan  31244  hvaddsubass  31246  hvsubass  31249  hvsubdistr1  31254  hvsubdistr2  31255  hvsubsub4i  31264  hvnegdii  31267  hvsubeq0i  31268  hvsubcan2i  31269  hvaddcani  31270  hvsubaddi  31271  hvaddeq0  31274  hvsubcan  31279  hvsubcan2  31280  hvsub0  31281  his2sub  31297  hisubcomi  31309  normlem0  31314  normlem9  31323  normsubi  31346  norm3difi  31352  normpar2i  31361  hilablo  31365  shsubcl  31425  hhssabloilem  31466  shsel3  31520  pjsubii  31883  pjssmii  31886  honegsubi  32001  honegneg  32011  hosubneg  32012  hosubdi  32013  honegdi  32014  honegsubdi  32015  honegsubdi2  32016  hosub4  32018  hosubsub4  32023  hosubeq0i  32031  nmopnegi  32170  lnopsubi  32179  lnophdi  32207  lnophmlem2  32222  lnfnsubi  32251  bdophdi  32302  nmoptri2i  32304  superpos  32559  cdj1i  32638  cdj3lem1  32639  quad3d  32953  psgnid  33279  psgnfzto1st  33287  cnmsgn0g  33328  altgnsg  33331  qqhval2lem  34280  signswch  34857  signlem0  34883  subfacval2  35542  subfaclim  35543  quad3  36025  fwddifn0  36519  fwddifnp1  36520  lcmineqlem1  42651  lcmineqlem2  42652  lcmineqlem8  42658  readvrec  42976  negexpidd  43268  rmym1  43517  proot1ex  43778  sqrtcval2  44223  expgrowth  44916  climneg  46191  dirkertrigeqlem1  46677  dirkertrigeqlem3  46679  fourierdlem24  46710  sqwvfourb  46808  fourierswlem  46809  fouriersw  46810  2pwp1prm  48203  3exp4mod41  48230  41prothprmlem2  48232  m1expevenALTV  48274  m1expoddALTV  48275  0nodd  48797  altgsumbc  48979  altgsumbcALT  48980