Theorem sgn0bi

Description: Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018)

	Ref	Expression
Assertion	sgn0bi	|- ( A e. RR* -> ( ( sgn ` A ) = 0 <-> A = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A e. RR* -> A e. RR* )
2		eqeq1	|- ( ( sgn ` A ) = 0 -> ( ( sgn ` A ) = 0 <-> 0 = 0 ) )
3	2	bibi1d	|- ( ( sgn ` A ) = 0 -> ( ( ( sgn ` A ) = 0 <-> A = 0 ) <-> ( 0 = 0 <-> A = 0 ) ) )
4		eqeq1	|- ( ( sgn ` A ) = 1 -> ( ( sgn ` A ) = 0 <-> 1 = 0 ) )
5	4	bibi1d	|- ( ( sgn ` A ) = 1 -> ( ( ( sgn ` A ) = 0 <-> A = 0 ) <-> ( 1 = 0 <-> A = 0 ) ) )
6		eqeq1	|- ( ( sgn ` A ) = -u 1 -> ( ( sgn ` A ) = 0 <-> -u 1 = 0 ) )
7	6	bibi1d	|- ( ( sgn ` A ) = -u 1 -> ( ( ( sgn ` A ) = 0 <-> A = 0 ) <-> ( -u 1 = 0 <-> A = 0 ) ) )
8		simpr	|- ( ( A e. RR* /\ A = 0 ) -> A = 0 )
9	8	eqcomd	|- ( ( A e. RR* /\ A = 0 ) -> 0 = A )
10	9	eqeq1d	|- ( ( A e. RR* /\ A = 0 ) -> ( 0 = 0 <-> A = 0 ) )
11		ax-1ne0	|- 1 =/= 0
12	11	a1i	|- ( ( A e. RR* /\ 0 < A ) -> 1 =/= 0 )
13	12	neneqd	|- ( ( A e. RR* /\ 0 < A ) -> -. 1 = 0 )
14		simpr	|- ( ( A e. RR* /\ 0 < A ) -> 0 < A )
15	14	gt0ne0d	|- ( ( A e. RR* /\ 0 < A ) -> A =/= 0 )
16	15	neneqd	|- ( ( A e. RR* /\ 0 < A ) -> -. A = 0 )
17	13 16	2falsed	|- ( ( A e. RR* /\ 0 < A ) -> ( 1 = 0 <-> A = 0 ) )
18		1cnd	|- ( ( A e. RR* /\ A < 0 ) -> 1 e. CC )
19	11	a1i	|- ( ( A e. RR* /\ A < 0 ) -> 1 =/= 0 )
20	18 19	negne0d	|- ( ( A e. RR* /\ A < 0 ) -> -u 1 =/= 0 )
21	20	neneqd	|- ( ( A e. RR* /\ A < 0 ) -> -. -u 1 = 0 )
22		simpr	|- ( ( A e. RR* /\ A < 0 ) -> A < 0 )
23	22	lt0ne0d	|- ( ( A e. RR* /\ A < 0 ) -> A =/= 0 )
24	23	neneqd	|- ( ( A e. RR* /\ A < 0 ) -> -. A = 0 )
25	21 24	2falsed	|- ( ( A e. RR* /\ A < 0 ) -> ( -u 1 = 0 <-> A = 0 ) )
26	1 3 5 7 10 17 25	sgn3da	|- ( A e. RR* -> ( ( sgn ` A ) = 0 <-> A = 0 ) )