Theorem neg1cn 12222

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 11177	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11545	1 ⊢ -1 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  ℂcc 11117  1c1 11120  -cneg 11461

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11176  ax-1cn 11177  ax-icn 11178  ax-addcl 11179  ax-addrcl 11180  ax-mulcl 11181  ax-mulrcl 11182  ax-mulcom 11183  ax-addass 11184  ax-mulass 11185  ax-distr 11186  ax-i2m1 11187  ax-1ne0 11188  ax-1rid 11189  ax-rnegex 11190  ax-rrecex 11191  ax-cnre 11192  ax-pre-lttri 11193  ax-pre-lttrn 11194  ax-pre-ltadd 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11264  df-mnf 11265  df-ltxr 11267  df-sub 11462  df-neg 11463

This theorem is used by:  m1expcl2  14143  m1expeven  14167  sgnmul  15172  iseraltlem2  15762  iseraltlem3  15763  fsumneg  15865  incexclem  15917  incexc  15918  risefallfac  16105  fallrisefac  16106  fallfac0  16108  0risefac  16118  binomrisefac  16122  n2dvdsm1  16453  m1expo  16459  m1exp1  16460  pwp1fsum  16475  bitsfzo  16519  bezoutlem1  16623  psgnunilem4  19615  m1expaddsub  19616  psgnuni  19617  psgnpmtr  19628  psgn0fv0  19629  psgnsn  19638  psgnprfval1  19640  cnmsgnsubg  21781  cnmsgnbas  21782  cnmsgngrp  21783  psgnghm  21784  psgninv  21786  mdetralt  22819  negcncf  25136  dvmptneg  26180  dvlipcn  26208  lhop2  26229  plysubcl  26434  coesub  26469  dgrsub  26484  quotlem  26516  quotcl2  26518  quotdgr  26519  iaa  26543  dvradcnv  26639  efipi  26693  eulerid  26694  sin2pi  26695  sinmpi  26707  cosmpi  26708  sinppi  26709  cosppi  26710  efif1olem2  26763  logneg  26808  lognegb  26810  logtayl  26880  logtayl2  26882  root1id  26974  root1eq1  26975  root1cj  26976  cxpeq  26977  angneg  27023  ang180lem1  27029  1cubrlem  27061  1cubr  27062  atandm4  27099  atandmtan  27140  atantayl3  27159  leibpi  27162  log2cnv  27164  wilthlem1  27287  wilthlem2  27288  basellem2  27301  basellem5  27304  basellem9  27308  isnsqf  27354  mule1  27367  mumul  27400  musum  27410  ppiub  27423  dchrptlem1  27483  dchrptlem2  27484  lgsneg  27540  lgsdilem  27543  lgsdir2lem3  27546  lgsdir2lem4  27547  lgsdir2  27549  lgsdir  27551  lgsdi  27553  lgsne0  27554  gausslemma2dlem5  27590  gausslemma2d  27593  lgseisenlem1  27594  lgseisenlem2  27595  lgseisenlem4  27597  lgseisen  27598  lgsquadlem1  27599  lgsquadlem2  27600  lgsquadlem3  27601  lgsquad2lem1  27603  lgsquad2lem2  27604  lgsquad3  27606  m1lgs  27607  addsqn2reu  27660  addsqrexnreu  27661  dchrisum0flblem1  27727  rpvmasum2  27731  axlowdimlem13  29363  vcm  31003  nvinvfval  31067  nvmval2  31070  nvmf  31072  nvmdi  31075  nvnegneg  31076  nvpncan2  31080  nvaddsub4  31084  nvm1  31092  nvdif  31093  nvmtri  31098  nvabs  31099  nvge0  31100  nvnd  31115  imsmetlem  31117  smcnlem  31124  vmcn  31126  ipval2  31134  4ipval2  31135  ipval3  31136  dipcj  31141  dip0r  31144  sspmval  31160  lno0  31183  lnosub  31186  ip0i  31252  ipdirilem  31256  ipasslem2  31259  ipasslem10  31266  dipsubdir  31275  hvsubf  31442  hvsubcl  31444  hvsubid  31453  hv2neg  31455  hvm1neg  31459  hvaddsubval  31460  hvsub4  31464  hvaddsub12  31465  hvpncan  31466  hvaddsubass  31468  hvsubass  31471  hvsubdistr1  31476  hvsubdistr2  31477  hvsubsub4i  31486  hvnegdii  31489  hvsubeq0i  31490  hvsubcan2i  31491  hvaddcani  31492  hvsubaddi  31493  hvaddeq0  31496  hvsubcan  31501  hvsubcan2  31502  hvsub0  31503  his2sub  31519  hisubcomi  31531  normlem0  31536  normlem9  31545  normsubi  31568  norm3difi  31574  normpar2i  31583  hilablo  31587  shsubcl  31647  hhssabloilem  31688  shsel3  31742  pjsubii  32105  pjssmii  32108  honegsubi  32223  honegneg  32233  hosubneg  32234  hosubdi  32235  honegdi  32236  honegsubdi  32237  honegsubdi2  32238  hosub4  32240  hosubsub4  32245  hosubeq0i  32253  nmopnegi  32392  lnopsubi  32401  lnophdi  32429  lnophmlem2  32444  lnfnsubi  32473  bdophdi  32524  nmoptri2i  32526  superpos  32781  cdj1i  32860  cdj3lem1  32861  quad3d  33168  psgnid  33485  psgnfzto1st  33493  cnmsgn0g  33534  altgnsg  33537  qqhval2lem  34439  signswch  35017  signlem0  35043  subfacval2  35720  subfaclim  35721  quad3  36203  fwddifn0  36697  fwddifnp1  36698  lcmineqlem1  42858  lcmineqlem2  42859  lcmineqlem8  42865  readvrec  43200  negexpidd  43490  rmym1  43739  proot1ex  44000  sqrtcval2  44445  expgrowth  45122  climneg  46403  dirkertrigeqlem1  46889  dirkertrigeqlem3  46891  fourierdlem24  46922  sqwvfourb  47020  fourierswlem  47021  fouriersw  47022  2pwp1prm  48418  3exp4mod41  48445  41prothprmlem2  48447  m1expevenALTV  48489  m1expoddALTV  48490  0nodd  49011  altgsumbc  49208  altgsumbcALT  49209