Description: The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | absmax | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | 2cn | |
|
3 | 2ne0 | |
|
4 | divcan3 | |
|
5 | 2 3 4 | mp3an23 | |
6 | 1 5 | syl | |
7 | 6 | ad2antlr | |
8 | ltle | |
|
9 | 8 | imp | |
10 | abssubge0 | |
|
11 | 10 | 3expa | |
12 | 9 11 | syldan | |
13 | 12 | oveq2d | |
14 | recn | |
|
15 | simpr | |
|
16 | simpl | |
|
17 | 15 16 15 | ppncand | |
18 | 2times | |
|
19 | 18 | adantl | |
20 | 17 19 | eqtr4d | |
21 | 14 1 20 | syl2an | |
22 | 21 | adantr | |
23 | 13 22 | eqtrd | |
24 | 23 | oveq1d | |
25 | ltnle | |
|
26 | 25 | biimpa | |
27 | 26 | iffalsed | |
28 | 7 24 27 | 3eqtr4rd | |
29 | 28 | ancom1s | |
30 | divcan3 | |
|
31 | 2 3 30 | mp3an23 | |
32 | 14 31 | syl | |
33 | 32 | ad2antlr | |
34 | abssuble0 | |
|
35 | 34 | 3expa | |
36 | 35 | oveq2d | |
37 | simpr | |
|
38 | simpl | |
|
39 | 37 38 37 | ppncand | |
40 | addcom | |
|
41 | 40 | oveq1d | |
42 | 2times | |
|
43 | 42 | adantl | |
44 | 39 41 43 | 3eqtr4d | |
45 | 1 14 44 | syl2an | |
46 | 45 | adantr | |
47 | 36 46 | eqtrd | |
48 | 47 | oveq1d | |
49 | iftrue | |
|
50 | 49 | adantl | |
51 | 33 48 50 | 3eqtr4rd | |
52 | simpr | |
|
53 | simpl | |
|
54 | 29 51 52 53 | ltlecasei | |