Metamath Proof Explorer


Theorem abs3lemi

Description: Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypotheses absvalsqi.1 A
abssub.2 B
abs3dif.3 C
abs3lem.4 D
Assertion abs3lemi AC<D2CB<D2AB<D

Proof

Step Hyp Ref Expression
1 absvalsqi.1 A
2 abssub.2 B
3 abs3dif.3 C
4 abs3lem.4 D
5 1 2 3 abs3difi ABAC+CB
6 1 3 subcli AC
7 6 abscli AC
8 3 2 subcli CB
9 8 abscli CB
10 4 rehalfcli D2
11 7 9 10 10 lt2addi AC<D2CB<D2AC+CB<D2+D2
12 1 2 subcli AB
13 12 abscli AB
14 7 9 readdcli AC+CB
15 10 10 readdcli D2+D2
16 13 14 15 lelttri ABAC+CBAC+CB<D2+D2AB<D2+D2
17 5 11 16 sylancr AC<D2CB<D2AB<D2+D2
18 10 recni D2
19 18 2timesi 2D2=D2+D2
20 4 recni D
21 2cn 2
22 2ne0 20
23 20 21 22 divcan2i 2D2=D
24 19 23 eqtr3i D2+D2=D
25 17 24 breqtrdi AC<D2CB<D2AB<D