Metamath Proof Explorer


Theorem absmax

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

Ref Expression
Assertion absmax ABifABBA=A+B+AB2

Proof

Step Hyp Ref Expression
1 recn AA
2 2cn 2
3 2ne0 20
4 divcan3 A2202A2=A
5 2 3 4 mp3an23 A2A2=A
6 1 5 syl A2A2=A
7 6 ad2antlr BAB<A2A2=A
8 ltle BAB<ABA
9 8 imp BAB<ABA
10 abssubge0 BABAAB=AB
11 10 3expa BABAAB=AB
12 9 11 syldan BAB<AAB=AB
13 12 oveq2d BAB<AA+B+AB=A+B+AB
14 recn BB
15 simpr BAA
16 simpl BAB
17 15 16 15 ppncand BAA+B+AB=A+A
18 2times A2A=A+A
19 18 adantl BA2A=A+A
20 17 19 eqtr4d BAA+B+AB=2A
21 14 1 20 syl2an BAA+B+AB=2A
22 21 adantr BAB<AA+B+AB=2A
23 13 22 eqtrd BAB<AA+B+AB=2A
24 23 oveq1d BAB<AA+B+AB2=2A2
25 ltnle BAB<A¬AB
26 25 biimpa BAB<A¬AB
27 26 iffalsed BAB<AifABBA=A
28 7 24 27 3eqtr4rd BAB<AifABBA=A+B+AB2
29 28 ancom1s ABB<AifABBA=A+B+AB2
30 divcan3 B2202B2=B
31 2 3 30 mp3an23 B2B2=B
32 14 31 syl B2B2=B
33 32 ad2antlr ABAB2B2=B
34 abssuble0 ABABAB=BA
35 34 3expa ABABAB=BA
36 35 oveq2d ABABA+B+AB=A+B+BA
37 simpr ABB
38 simpl ABA
39 37 38 37 ppncand ABB+A+BA=B+B
40 addcom ABA+B=B+A
41 40 oveq1d ABA+B+BA=B+A+BA
42 2times B2B=B+B
43 42 adantl AB2B=B+B
44 39 41 43 3eqtr4d ABA+B+BA=2B
45 1 14 44 syl2an ABA+B+BA=2B
46 45 adantr ABABA+B+BA=2B
47 36 46 eqtrd ABABA+B+AB=2B
48 47 oveq1d ABABA+B+AB2=2B2
49 iftrue ABifABBA=B
50 49 adantl ABABifABBA=B
51 33 48 50 3eqtr4rd ABABifABBA=A+B+AB2
52 simpr ABB
53 simpl ABA
54 29 51 52 53 ltlecasei ABifABBA=A+B+AB2