Metamath Proof Explorer

Theorem absmax

Description: The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008)

Ref Expression
Assertion absmax 
|- ( ( A e. RR /\ B e. RR ) -> if ( A <_ B , B , A ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 divcan3 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. A ) / 2 ) = A )
5 2 3 4 mp3an23 
 |-  ( A e. CC -> ( ( 2 x. A ) / 2 ) = A )
6 1 5 syl 
 |-  ( A e. RR -> ( ( 2 x. A ) / 2 ) = A )
7 6 ad2antlr 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( ( 2 x. A ) / 2 ) = A )
8 ltle 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A -> B <_ A ) )
9 8 imp 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> B <_ A )
10 abssubge0 
 |-  ( ( B e. RR /\ A e. RR /\ B <_ A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
11 10 3expa 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B <_ A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
12 9 11 syldan 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( abs ` ( A - B ) ) = ( A - B ) )
13 12 oveq2d 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( ( A + B ) + ( abs ` ( A - B ) ) ) = ( ( A + B ) + ( A - B ) ) )
14 recn 
 |-  ( B e. RR -> B e. CC )
15 simpr 
 |-  ( ( B e. CC /\ A e. CC ) -> A e. CC )
16 simpl 
 |-  ( ( B e. CC /\ A e. CC ) -> B e. CC )
17 15 16 15 ppncand 
 |-  ( ( B e. CC /\ A e. CC ) -> ( ( A + B ) + ( A - B ) ) = ( A + A ) )
18 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
19 18 adantl 
 |-  ( ( B e. CC /\ A e. CC ) -> ( 2 x. A ) = ( A + A ) )
20 17 19 eqtr4d 
 |-  ( ( B e. CC /\ A e. CC ) -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
21 14 1 20 syl2an 
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
22 21 adantr 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
23 13 22 eqtrd 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( ( A + B ) + ( abs ` ( A - B ) ) ) = ( 2 x. A ) )
24 23 oveq1d 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = ( ( 2 x. A ) / 2 ) )
25 ltnle 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A <-> -. A <_ B ) )
26 25 biimpa 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> -. A <_ B )
27 26 iffalsed 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> if ( A <_ B , B , A ) = A )
28 7 24 27 3eqtr4rd 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ B < A ) -> if ( A <_ B , B , A ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
29 28 ancom1s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> if ( A <_ B , B , A ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
30 divcan3 
 |-  ( ( B e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. B ) / 2 ) = B )
31 2 3 30 mp3an23 
 |-  ( B e. CC -> ( ( 2 x. B ) / 2 ) = B )
32 14 31 syl 
 |-  ( B e. RR -> ( ( 2 x. B ) / 2 ) = B )
33 32 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( 2 x. B ) / 2 ) = B )
34 abssuble0 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )
35 34 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )
36 35 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( A + B ) + ( abs ` ( A - B ) ) ) = ( ( A + B ) + ( B - A ) ) )
37 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
38 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
39 37 38 37 ppncand 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( B + A ) + ( B - A ) ) = ( B + B ) )
40 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
41 40 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( B - A ) ) = ( ( B + A ) + ( B - A ) ) )
42 2times 
 |-  ( B e. CC -> ( 2 x. B ) = ( B + B ) )
43 42 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. B ) = ( B + B ) )
44 39 41 43 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) + ( B - A ) ) = ( 2 x. B ) )
45 1 14 44 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) + ( B - A ) ) = ( 2 x. B ) )
46 45 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( A + B ) + ( B - A ) ) = ( 2 x. B ) )
47 36 46 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( A + B ) + ( abs ` ( A - B ) ) ) = ( 2 x. B ) )
48 47 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = ( ( 2 x. B ) / 2 ) )
49 iftrue 
 |-  ( A <_ B -> if ( A <_ B , B , A ) = B )
50 49 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> if ( A <_ B , B , A ) = B )
51 33 48 50 3eqtr4rd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> if ( A <_ B , B , A ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
52 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
53 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
54 29 51 52 53 ltlecasei 
 |-  ( ( A e. RR /\ B e. RR ) -> if ( A <_ B , B , A ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )