Theorem sgncl

Description: Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018)

	Ref	Expression
Assertion	sgncl	|- ( A e. RR* -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A e. RR* /\ A = 0 ) -> A = 0 )
2	1	fveq2d	|- ( ( A e. RR* /\ A = 0 ) -> ( sgn ` A ) = ( sgn ` 0 ) )
3		sgn0	|- ( sgn ` 0 ) = 0
4	2 3	eqtrdi	|- ( ( A e. RR* /\ A = 0 ) -> ( sgn ` A ) = 0 )
5		c0ex	|- 0 e. _V
6	5	tpid2	|- 0 e. { -u 1 , 0 , 1 }
7	4 6	eqeltrdi	|- ( ( A e. RR* /\ A = 0 ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
8		sgnn	|- ( ( A e. RR* /\ A < 0 ) -> ( sgn ` A ) = -u 1 )
9		negex	|- -u 1 e. _V
10	9	tpid1	|- -u 1 e. { -u 1 , 0 , 1 }
11	8 10	eqeltrdi	|- ( ( A e. RR* /\ A < 0 ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
12	11	adantlr	|- ( ( ( A e. RR* /\ A =/= 0 ) /\ A < 0 ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
13		sgnp	|- ( ( A e. RR* /\ 0 < A ) -> ( sgn ` A ) = 1 )
14		1ex	|- 1 e. _V
15	14	tpid3	|- 1 e. { -u 1 , 0 , 1 }
16	13 15	eqeltrdi	|- ( ( A e. RR* /\ 0 < A ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
17	16	adantlr	|- ( ( ( A e. RR* /\ A =/= 0 ) /\ 0 < A ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
18		0xr	|- 0 e. RR*
19		xrlttri2	|- ( ( A e. RR* /\ 0 e. RR* ) -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
20	19	biimpa	|- ( ( ( A e. RR* /\ 0 e. RR* ) /\ A =/= 0 ) -> ( A < 0 \/ 0 < A ) )
21	18 20	mpanl2	|- ( ( A e. RR* /\ A =/= 0 ) -> ( A < 0 \/ 0 < A ) )
22	12 17 21	mpjaodan	|- ( ( A e. RR* /\ A =/= 0 ) -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
23	7 22	pm2.61dane	|- ( A e. RR* -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )