Theorem negne0bd

Description: A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypothesis	negidd.1	|- ( ph -> A e. CC )
Assertion	negne0bd	|- ( ph -> ( A =/= 0 <-> -u A =/= 0 ) )

Proof

Step	Hyp	Ref	Expression
1		negidd.1	|- ( ph -> A e. CC )
2	1	negeq0d	|- ( ph -> ( A = 0 <-> -u A = 0 ) )
3	2	necon3bid	|- ( ph -> ( A =/= 0 <-> -u A =/= 0 ) )