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 e. RR -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. RR -> 0 e. RR )
2 id 
 |-  ( A e. RR -> A e. RR )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 3 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
5 4 addridd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A + 0 ) = A )
6 iftrue 
 |-  ( 0 <_ A -> if ( 0 <_ A , A , 0 ) = A )
7 6 adantl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ A , A , 0 ) = A )
8 le0neg2 
 |-  ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) )
9 8 biimpa 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u A <_ 0 )
10 9 adantr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A <_ 0 )
11 simpr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> 0 <_ -u A )
12 renegcl 
 |-  ( A e. RR -> -u A e. RR )
13 12 ad2antrr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A e. RR )
14 0re 
 |-  0 e. RR
15 letri3 
 |-  ( ( -u A e. RR /\ 0 e. RR ) -> ( -u A = 0 <-> ( -u A <_ 0 /\ 0 <_ -u A ) ) )
16 13 14 15 sylancl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> ( -u A = 0 <-> ( -u A <_ 0 /\ 0 <_ -u A ) ) )
17 10 11 16 mpbir2and 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ -u A ) -> -u A = 0 )
18 17 ifeq1da 
 |-  ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ -u A , -u A , 0 ) = if ( 0 <_ -u A , 0 , 0 ) )
19 ifid 
 |-  if ( 0 <_ -u A , 0 , 0 ) = 0
20 18 19 eqtrdi 
 |-  ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ -u A , -u A , 0 ) = 0 )
21 7 20 oveq12d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( A + 0 ) )
22 absid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
23 5 21 22 3eqtr4d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) )
24 3 adantr 
 |-  ( ( A e. RR /\ A <_ 0 ) -> A e. CC )
25 24 negcld 
 |-  ( ( A e. RR /\ A <_ 0 ) -> -u A e. CC )
26 25 addlidd 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( 0 + -u A ) = -u A )
27 letri3 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
28 14 27 mpan2 
 |-  ( A e. RR -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
29 28 biimprd 
 |-  ( A e. RR -> ( ( A <_ 0 /\ 0 <_ A ) -> A = 0 ) )
30 29 impl 
 |-  ( ( ( A e. RR /\ A <_ 0 ) /\ 0 <_ A ) -> A = 0 )
31 30 ifeq1da 
 |-  ( ( A e. RR /\ 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 e. RR /\ A <_ 0 ) -> if ( 0 <_ A , A , 0 ) = 0 )
34 le0neg1 
 |-  ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) )
35 34 biimpa 
 |-  ( ( A e. RR /\ A <_ 0 ) -> 0 <_ -u A )
36 35 iftrued 
 |-  ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ -u A , -u A , 0 ) = -u A )
37 33 36 oveq12d 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( 0 + -u A ) )
38 absnid 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
39 26 37 38 3eqtr4d 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) )
40 1 2 23 39 lecasei 
 |-  ( A e. RR -> ( if ( 0 <_ A , A , 0 ) + if ( 0 <_ -u A , -u A , 0 ) ) = ( abs ` A ) )