Theorem neg1cn 12231

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 11186	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11554	1 ⊢ -1 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  ℂcc 11126  1c1 11129  -cneg 11470

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276  df-sub 11471  df-neg 11472

This theorem is used by:  m1expcl2  14153  m1expeven  14177  sgnmul  15184  iseraltlem2  15774  iseraltlem3  15775  fsumneg  15877  incexclem  15929  incexc  15930  risefallfac  16117  fallrisefac  16118  fallfac0  16120  0risefac  16130  binomrisefac  16134  n2dvdsm1  16465  m1expo  16471  m1exp1  16472  pwp1fsum  16487  bitsfzo  16531  bezoutlem1  16635  psgnunilem4  19630  m1expaddsub  19631  psgnuni  19632  psgnpmtr  19643  psgn0fv0  19644  psgnsn  19653  psgnprfval1  19655  cnmsgnsubg  21796  cnmsgnbas  21797  cnmsgngrp  21798  psgnghm  21799  psgninv  21801  mdetralt  22836  negcncf  25156  dvmptneg  26200  dvlipcn  26228  lhop2  26249  plysubcl  26455  coesub  26490  dgrsub  26505  quotlem  26537  quotcl2  26539  quotdgr  26540  iaaOLD  26568  dvradcnv  26664  efipi  26718  eulerid  26719  sin2pi  26720  sinmpi  26732  cosmpi  26733  sinppi  26734  cosppi  26735  efif1olem2  26788  logneg  26833  lognegb  26835  logtayl  26905  logtayl2  26907  root1id  26999  root1eq1  27000  root1cj  27001  cxpeq  27002  angneg  27048  ang180lem1  27054  1cubrlem  27086  1cubr  27087  atandm4  27124  atandmtan  27165  atantayl3  27184  leibpi  27187  log2cnv  27189  wilthlem1  27312  wilthlem2  27313  basellem2  27326  basellem5  27329  basellem9  27333  isnsqf  27379  mule1  27392  mumul  27425  musum  27435  ppiub  27448  dchrptlem1  27508  dchrptlem2  27509  lgsneg  27565  lgsdilem  27568  lgsdir2lem3  27571  lgsdir2lem4  27572  lgsdir2  27574  lgsdir  27576  lgsdi  27578  lgsne0  27579  gausslemma2dlem5  27615  gausslemma2d  27618  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem4  27622  lgseisen  27623  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  lgsquad2lem1  27628  lgsquad2lem2  27629  lgsquad3  27631  m1lgs  27632  addsqn2reu  27685  addsqrexnreu  27686  dchrisum0flblem1  27752  rpvmasum2  27756  axlowdimlem13  29419  vcm  31065  nvinvfval  31129  nvmval2  31132  nvmf  31134  nvmdi  31137  nvnegneg  31138  nvpncan2  31142  nvaddsub4  31146  nvm1  31154  nvdif  31155  nvmtri  31160  nvabs  31161  nvge0  31162  nvnd  31177  imsmetlem  31179  smcnlem  31186  vmcn  31188  ipval2  31196  4ipval2  31197  ipval3  31198  dipcj  31203  dip0r  31206  sspmval  31222  lno0  31245  lnosub  31248  ip0i  31314  ipdirilem  31318  ipasslem2  31321  ipasslem10  31328  dipsubdir  31337  hvsubf  31504  hvsubcl  31506  hvsubid  31515  hv2neg  31517  hvm1neg  31521  hvaddsubval  31522  hvsub4  31526  hvaddsub12  31527  hvpncan  31528  hvaddsubass  31530  hvsubass  31533  hvsubdistr1  31538  hvsubdistr2  31539  hvsubsub4i  31548  hvnegdii  31551  hvsubeq0i  31552  hvsubcan2i  31553  hvaddcani  31554  hvsubaddi  31555  hvaddeq0  31558  hvsubcan  31563  hvsubcan2  31564  hvsub0  31565  his2sub  31581  hisubcomi  31593  normlem0  31598  normlem9  31607  normsubi  31630  norm3difi  31636  normpar2i  31645  hilablo  31649  shsubcl  31709  hhssabloilem  31750  shsel3  31804  pjsubii  32167  pjssmii  32170  honegsubi  32285  honegneg  32295  hosubneg  32296  hosubdi  32297  honegdi  32298  honegsubdi  32299  honegsubdi2  32300  hosub4  32302  hosubsub4  32307  hosubeq0i  32315  nmopnegi  32454  lnopsubi  32463  lnophdi  32491  lnophmlem2  32506  lnfnsubi  32535  bdophdi  32586  nmoptri2i  32588  superpos  32843  cdj1i  32922  cdj3lem1  32923  quad3d  33228  psgnid  33545  psgnfzto1st  33553  cnmsgn0g  33594  altgnsg  33597  qqhval2lem  34499  signswch  35077  signlem0  35103  subfacval2  35774  subfaclim  35775  quad3  36257  fwddifn0  36752  fwddifnp1  36753  lcmineqlem1  42903  lcmineqlem2  42904  lcmineqlem8  42910  readvrec  43245  negexpidd  43535  rmym1  43784  proot1ex  44045  sqrtcval2  44490  expgrowth  45167  climneg  46448  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  fourierdlem24  46967  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  goldratval  47762  2pwp1prm  48500  3exp4mod41  48527  41prothprmlem2  48529  m1expevenALTV  48571  m1expoddALTV  48572  0nodd  49093  altgsumbc  49290  altgsumbcALT  49291