Theorem neg1ne0 12140

Description: -1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
neg1ne0	⊢ -1 ≠ 0

Proof of Theorem neg1ne0

Step	Hyp	Ref	Expression
1		ax-1cn 11090	. 2 ⊢ 1 ∈ ℂ
2		ax-1ne0 11101	. 2 ⊢ 1 ≠ 0
3	1, 2	negne0i 11463	1 ⊢ -1 ≠ 0

Syntax hints:   ≠ wne 2933  0cc0 11032  1c1 11033  -cneg 11372

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 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374

This theorem is referenced by:  m1expcl2  14041  m1expeven  14065  iseraltlem2  15639  iseraltlem3  15640  iseralt  15641  m1expo  16338  m1exp1  16339  psgnunilem4  19466  m1expaddsub  19467  psgnuni  19468  cnmsgnsubg  21570  cnmsgngrp  21572  psgninv  21575  iblcnlem1  25768  itgcnlem  25770  dgrsub  26250  coseq00topi  26482  logtayl2  26642  root1eq1  26735  root1cj  26736  cxpeq  26737  angneg  26783  ang180lem1  26789  1cubrlem  26821  atantayl2  26918  basellem2  27062  isnsqf  27115  dchrfi  27235  dchrptlem1  27244  dchrptlem2  27245  lgsne0  27315  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem4  27358  lgseisen  27359  lgsquadlem1  27360  lgsquad2lem1  27364  lgsquad3  27367  m1lgs  27368  hvsubcan  31163  hvsubcan2  31164  superpos  32443  sgnnbi  32929  cos9thpiminplylem1  33945  signswch  34724  signstfvcl  34736  fwddifnp1  36366  proot1ex  43645  m1expevenALTV  48138  m1expoddALTV  48139