Metamath Proof Explorer


Theorem dnibndlem6

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibndlem6.1 φ A
dnibndlem6.2 φ B
Assertion dnibndlem6 φ B + 1 2 B A + 1 2 A 1 2 B + 1 2 B + 1 2 - A + 1 2 A

Proof

Step Hyp Ref Expression
1 dnibndlem6.1 φ A
2 dnibndlem6.2 φ B
3 2 dnicld1 φ B + 1 2 B
4 3 recnd φ B + 1 2 B
5 1 dnicld1 φ A + 1 2 A
6 5 recnd φ A + 1 2 A
7 4 6 subcld φ B + 1 2 B A + 1 2 A
8 7 abscld φ B + 1 2 B A + 1 2 A
9 halfcn 1 2
10 9 a1i φ 1 2
11 4 10 subcld φ B + 1 2 B 1 2
12 11 abscld φ B + 1 2 B 1 2
13 10 6 subcld φ 1 2 A + 1 2 A
14 13 abscld φ 1 2 A + 1 2 A
15 12 14 readdcld φ B + 1 2 B 1 2 + 1 2 A + 1 2 A
16 halfre 1 2
17 16 a1i φ 1 2
18 17 3 jca φ 1 2 B + 1 2 B
19 resubcl 1 2 B + 1 2 B 1 2 B + 1 2 B
20 18 19 syl φ 1 2 B + 1 2 B
21 17 5 jca φ 1 2 A + 1 2 A
22 resubcl 1 2 A + 1 2 A 1 2 A + 1 2 A
23 21 22 syl φ 1 2 A + 1 2 A
24 20 23 readdcld φ 1 2 B + 1 2 B + 1 2 - A + 1 2 A
25 4 6 10 3jca φ B + 1 2 B A + 1 2 A 1 2
26 abs3dif B + 1 2 B A + 1 2 A 1 2 B + 1 2 B A + 1 2 A B + 1 2 B 1 2 + 1 2 A + 1 2 A
27 25 26 syl φ B + 1 2 B A + 1 2 A B + 1 2 B 1 2 + 1 2 A + 1 2 A
28 4 10 abssubd φ B + 1 2 B 1 2 = 1 2 B + 1 2 B
29 rddif2 B 0 1 2 B + 1 2 B
30 2 29 syl φ 0 1 2 B + 1 2 B
31 20 30 absidd φ 1 2 B + 1 2 B = 1 2 B + 1 2 B
32 28 31 eqtrd φ B + 1 2 B 1 2 = 1 2 B + 1 2 B
33 rddif2 A 0 1 2 A + 1 2 A
34 1 33 syl φ 0 1 2 A + 1 2 A
35 23 34 absidd φ 1 2 A + 1 2 A = 1 2 A + 1 2 A
36 32 35 oveq12d φ B + 1 2 B 1 2 + 1 2 A + 1 2 A = 1 2 B + 1 2 B + 1 2 - A + 1 2 A
37 15 36 eqled φ B + 1 2 B 1 2 + 1 2 A + 1 2 A 1 2 B + 1 2 B + 1 2 - A + 1 2 A
38 8 15 24 27 37 letrd φ B + 1 2 B A + 1 2 A 1 2 B + 1 2 B + 1 2 - A + 1 2 A