Metamath Proof Explorer


Theorem max0add

Description: The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Mario Carneiro, 24-Aug-2014)

Ref Expression
Assertion max0add A if 0 A A 0 + if 0 A A 0 = A

Proof

Step Hyp Ref Expression
1 0red A 0
2 id A A
3 recn A A
4 3 adantr A 0 A A
5 4 addid1d A 0 A A + 0 = A
6 iftrue 0 A if 0 A A 0 = A
7 6 adantl A 0 A if 0 A A 0 = A
8 le0neg2 A 0 A A 0
9 8 biimpa A 0 A A 0
10 9 adantr A 0 A 0 A A 0
11 simpr A 0 A 0 A 0 A
12 renegcl A A
13 12 ad2antrr A 0 A 0 A A
14 0re 0
15 letri3 A 0 A = 0 A 0 0 A
16 13 14 15 sylancl A 0 A 0 A A = 0 A 0 0 A
17 10 11 16 mpbir2and A 0 A 0 A A = 0
18 17 ifeq1da A 0 A if 0 A A 0 = if 0 A 0 0
19 ifid if 0 A 0 0 = 0
20 18 19 eqtrdi A 0 A if 0 A A 0 = 0
21 7 20 oveq12d A 0 A if 0 A A 0 + if 0 A A 0 = A + 0
22 absid A 0 A A = A
23 5 21 22 3eqtr4d A 0 A if 0 A A 0 + if 0 A A 0 = A
24 3 adantr A A 0 A
25 24 negcld A A 0 A
26 25 addid2d A A 0 0 + A = A
27 letri3 A 0 A = 0 A 0 0 A
28 14 27 mpan2 A A = 0 A 0 0 A
29 28 biimprd A A 0 0 A A = 0
30 29 impl A A 0 0 A A = 0
31 30 ifeq1da A A 0 if 0 A A 0 = if 0 A 0 0
32 ifid if 0 A 0 0 = 0
33 31 32 eqtrdi A A 0 if 0 A A 0 = 0
34 le0neg1 A A 0 0 A
35 34 biimpa A A 0 0 A
36 35 iftrued A A 0 if 0 A A 0 = A
37 33 36 oveq12d A A 0 if 0 A A 0 + if 0 A A 0 = 0 + A
38 absnid A A 0 A = A
39 26 37 38 3eqtr4d A A 0 if 0 A A 0 + if 0 A A 0 = A
40 1 2 23 39 lecasei A if 0 A A 0 + if 0 A A 0 = A