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 addid1d
 |-  ( ( 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 addid2d
 |-  ( ( 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 ) )