Theorem neg1ne0 12222

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 11175	. 2 ⊢ 1 ∈ ℂ
2		ax-1ne0 11186	. 2 ⊢ 1 ≠ 0
3	1, 2	negne0i 11550	1 ⊢ -1 ≠ 0

This proof depends on syntax axioms:   ≠ wne 2960  0cc0 11117  1c1 11118  -cneg 11459

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 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193

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 11262  df-mnf 11263  df-ltxr 11265  df-sub 11460  df-neg 11461

This theorem is used by:  m1expcl2  14141  m1expeven  14165  sgnnbi  15167  iseraltlem2  15760  iseraltlem3  15761  iseralt  15762  m1expo  16457  m1exp1  16458  psgnunilem4  19613  m1expaddsub  19614  psgnuni  19615  cnmsgnsubg  21779  cnmsgngrp  21781  psgninv  21784  iblcnlem1  26000  itgcnlem  26002  dgrsub  26482  coseq00topi  26720  logtayl2  26880  root1eq1  26973  root1cj  26974  cxpeq  26975  angneg  27021  ang180lem1  27027  1cubrlem  27059  atantayl2  27156  basellem2  27299  isnsqf  27352  dchrfi  27472  dchrptlem1  27481  dchrptlem2  27482  lgsne0  27552  lgseisenlem1  27592  lgseisenlem2  27593  lgseisenlem4  27595  lgseisen  27596  lgsquadlem1  27597  lgsquad2lem1  27601  lgsquad3  27604  m1lgs  27605  hvsubcan  31499  hvsubcan2  31500  superpos  32779  cos9thpiminplylem1  34238  signswch  35015  signstfvcl  35027  fwddifnp1  36696  proot1ex  43983  m1expevenALTV  48472  m1expoddALTV  48473