Metamath Proof Explorer

Theorem max0sub

Description: Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion max0sub 
|- ( A e. RR -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = A )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. RR -> 0 e. RR )
2 id 
 |-  ( A e. RR -> A e. RR )
3 iftrue 
 |-  ( 0 <_ A -> if ( 0 <_ A , A , 0 ) = A )
4 3 adantl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ A , A , 0 ) = A )
5 0xr 
 |-  0 e. RR*
6 renegcl 
 |-  ( A e. RR -> -u A e. RR )
7 6 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u A e. RR )
8 7 rexrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u A e. RR* )
9 le0neg2 
 |-  ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) )
10 9 biimpa 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u A <_ 0 )
11 xrmaxeq 
 |-  ( ( 0 e. RR* /\ -u A e. RR* /\ -u A <_ 0 ) -> if ( 0 <_ -u A , -u A , 0 ) = 0 )
12 5 8 10 11 mp3an2i 
 |-  ( ( A e. RR /\ 0 <_ A ) -> if ( 0 <_ -u A , -u A , 0 ) = 0 )
13 4 12 oveq12d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = ( A - 0 ) )
14 recn 
 |-  ( A e. RR -> A e. CC )
15 14 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
16 15 subid1d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A - 0 ) = A )
17 13 16 eqtrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = A )
18 rexr 
 |-  ( A e. RR -> A e. RR* )
19 18 adantr 
 |-  ( ( A e. RR /\ A <_ 0 ) -> A e. RR* )
20 simpr 
 |-  ( ( A e. RR /\ A <_ 0 ) -> A <_ 0 )
21 xrmaxeq 
 |-  ( ( 0 e. RR* /\ A e. RR* /\ A <_ 0 ) -> if ( 0 <_ A , A , 0 ) = 0 )
22 5 19 20 21 mp3an2i 
 |-  ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ A , A , 0 ) = 0 )
23 le0neg1 
 |-  ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) )
24 23 biimpa 
 |-  ( ( A e. RR /\ A <_ 0 ) -> 0 <_ -u A )
25 24 iftrued 
 |-  ( ( A e. RR /\ A <_ 0 ) -> if ( 0 <_ -u A , -u A , 0 ) = -u A )
26 22 25 oveq12d 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = ( 0 - -u A ) )
27 df-neg 
 |-  -u -u A = ( 0 - -u A )
28 14 adantr 
 |-  ( ( A e. RR /\ A <_ 0 ) -> A e. CC )
29 28 negnegd 
 |-  ( ( A e. RR /\ A <_ 0 ) -> -u -u A = A )
30 27 29 eqtr3id 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( 0 - -u A ) = A )
31 26 30 eqtrd 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = A )
32 1 2 17 31 lecasei 
 |-  ( A e. RR -> ( if ( 0 <_ A , A , 0 ) - if ( 0 <_ -u A , -u A , 0 ) ) = A )