Metamath Proof Explorer


Theorem reabsifnpos

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

Ref Expression
Assertion reabsifnpos A A = if A 0 A A

Proof

Step Hyp Ref Expression
1 absnid A A 0 A = A
2 1 eqcomd A A 0 A = A
3 0re 0
4 ltnle 0 A 0 < A ¬ A 0
5 ltle 0 A 0 < A 0 A
6 4 5 sylbird 0 A ¬ A 0 0 A
7 3 6 mpan A ¬ A 0 0 A
8 7 imdistani A ¬ A 0 A 0 A
9 absid A 0 A A = A
10 8 9 syl A ¬ A 0 A = A
11 10 eqcomd A ¬ A 0 A = A
12 2 11 ifeqda A if A 0 A A = A
13 12 eqcomd A A = if A 0 A A