Theorem sgnval2

Description: Value of the signum of a real number, expresssed using absolute value. (Contributed by Thierry Arnoux, 9-Nov-2025)

	Ref	Expression
Assertion	sgnval2	|- ( ( A e. RR /\ A =/= 0 ) -> ( sgn ` A ) = ( A / ( abs ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. RR /\ A =/= 0 ) -> A e. RR )
2		0red	|- ( ( A e. RR /\ A =/= 0 ) -> 0 e. RR )
3	1	recnd	|- ( ( A e. RR /\ A =/= 0 ) -> A e. CC )
4	3	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> A e. CC )
5		simplr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> A =/= 0 )
6	4 4 5	divneg2d	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> -u ( A / A ) = ( A / -u A ) )
7		simpr	|- ( ( A e. RR /\ A =/= 0 ) -> A =/= 0 )
8	3 7	dividd	|- ( ( A e. RR /\ A =/= 0 ) -> ( A / A ) = 1 )
9	8	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( A / A ) = 1 )
10	9	negeqd	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> -u ( A / A ) = -u 1 )
11	6 10	eqtr3d	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( A / -u A ) = -u 1 )
12		absnid	|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
13	12	adantlr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( abs ` A ) = -u A )
14	13	oveq2d	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( A / ( abs ` A ) ) = ( A / -u A ) )
15	1	rexrd	|- ( ( A e. RR /\ A =/= 0 ) -> A e. RR* )
16	1	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> A e. RR )
17		0red	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> 0 e. RR )
18		simpr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> A <_ 0 )
19	7	necomd	|- ( ( A e. RR /\ A =/= 0 ) -> 0 =/= A )
20	19	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> 0 =/= A )
21	16 17 18 20	leneltd	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> A < 0 )
22		sgnn	|- ( ( A e. RR* /\ A < 0 ) -> ( sgn ` A ) = -u 1 )
23	15 21 22	syl2an2r	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( sgn ` A ) = -u 1 )
24	11 14 23	3eqtr4rd	|- ( ( ( A e. RR /\ A =/= 0 ) /\ A <_ 0 ) -> ( sgn ` A ) = ( A / ( abs ` A ) ) )
25	8	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> ( A / A ) = 1 )
26	1	adantr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> A e. RR )
27		simpr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> 0 <_ A )
28	26 27	absidd	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> ( abs ` A ) = A )
29	28	oveq2d	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> ( A / ( abs ` A ) ) = ( A / A ) )
30		simplr	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> A =/= 0 )
31	26 27 30	ne0gt0d	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> 0 < A )
32		sgnp	|- ( ( A e. RR* /\ 0 < A ) -> ( sgn ` A ) = 1 )
33	15 31 32	syl2an2r	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> ( sgn ` A ) = 1 )
34	25 29 33	3eqtr4rd	|- ( ( ( A e. RR /\ A =/= 0 ) /\ 0 <_ A ) -> ( sgn ` A ) = ( A / ( abs ` A ) ) )
35	1 2 24 34	lecasei	|- ( ( A e. RR /\ A =/= 0 ) -> ( sgn ` A ) = ( A / ( abs ` A ) ) )