Metamath Proof Explorer


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 A = if A < 0 A A

Proof

Step Hyp Ref Expression
1 0re 0
2 ltle A 0 A < 0 A 0
3 1 2 mpan2 A A < 0 A 0
4 3 imdistani A A < 0 A A 0
5 absnid A A 0 A = A
6 4 5 syl A A < 0 A = A
7 6 eqcomd A A < 0 A = A
8 0red A 0
9 id A A
10 8 9 lenltd A 0 A ¬ A < 0
11 10 bicomd A ¬ A < 0 0 A
12 11 pm5.32i A ¬ A < 0 A 0 A
13 absid A 0 A A = A
14 12 13 sylbi A ¬ A < 0 A = A
15 14 eqcomd A ¬ A < 0 A = A
16 7 15 ifeqda A if A < 0 A A = A
17 16 eqcomd A A = if A < 0 A A