Theorem reabsifneg

Description: Alternate expression for the absolute value of a real number. Lemma for sqrtcval . (Contributed by RP, 11-May-2024)

	Ref	Expression
Assertion	reabsifneg	|- ( A e. RR -> ( abs ` A ) = if ( A < 0 , -u A , A ) )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		ltle	|- ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 -> A <_ 0 ) )
3	1 2	mpan2	|- ( A e. RR -> ( A < 0 -> A <_ 0 ) )
4	3	imdistani	|- ( ( A e. RR /\ A < 0 ) -> ( A e. RR /\ A <_ 0 ) )
5		absnid	|- ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
6	4 5	syl	|- ( ( A e. RR /\ A < 0 ) -> ( abs ` A ) = -u A )
7	6	eqcomd	|- ( ( A e. RR /\ A < 0 ) -> -u A = ( abs ` A ) )
8		0red	|- ( A e. RR -> 0 e. RR )
9		id	|- ( A e. RR -> A e. RR )
10	8 9	lenltd	|- ( A e. RR -> ( 0 <_ A <-> -. A < 0 ) )
11	10	bicomd	|- ( A e. RR -> ( -. A < 0 <-> 0 <_ A ) )
12	11	pm5.32i	|- ( ( A e. RR /\ -. A < 0 ) <-> ( A e. RR /\ 0 <_ A ) )
13		absid	|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
14	12 13	sylbi	|- ( ( A e. RR /\ -. A < 0 ) -> ( abs ` A ) = A )
15	14	eqcomd	|- ( ( A e. RR /\ -. A < 0 ) -> A = ( abs ` A ) )
16	7 15	ifeqda	|- ( A e. RR -> if ( A < 0 , -u A , A ) = ( abs ` A ) )
17	16	eqcomd	|- ( A e. RR -> ( abs ` A ) = if ( A < 0 , -u A , A ) )