Description: Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | absvalsqi.1 | |
|
abssub.2 | |
||
abs3dif.3 | |
||
abs3lem.4 | |
||
Assertion | abs3lemi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | absvalsqi.1 | |
|
2 | abssub.2 | |
|
3 | abs3dif.3 | |
|
4 | abs3lem.4 | |
|
5 | 1 2 3 | abs3difi | |
6 | 1 3 | subcli | |
7 | 6 | abscli | |
8 | 3 2 | subcli | |
9 | 8 | abscli | |
10 | 4 | rehalfcli | |
11 | 7 9 10 10 | lt2addi | |
12 | 1 2 | subcli | |
13 | 12 | abscli | |
14 | 7 9 | readdcli | |
15 | 10 10 | readdcli | |
16 | 13 14 15 | lelttri | |
17 | 5 11 16 | sylancr | |
18 | 10 | recni | |
19 | 18 | 2timesi | |
20 | 4 | recni | |
21 | 2cn | |
|
22 | 2ne0 | |
|
23 | 20 21 22 | divcan2i | |
24 | 19 23 | eqtr3i | |
25 | 17 24 | breqtrdi | |