Metamath Proof Explorer


Theorem dnibndlem7

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

Ref Expression
Hypothesis dnibndlem7.1 φ B
Assertion dnibndlem7 φ 1 2 B + 1 2 B B B + 1 2 1 2

Proof

Step Hyp Ref Expression
1 dnibndlem7.1 φ B
2 halfre 1 2
3 2 a1i φ 1 2
4 1 3 jca φ B 1 2
5 readdcl B 1 2 B + 1 2
6 4 5 syl φ B + 1 2
7 reflcl B + 1 2 B + 1 2
8 6 7 syl φ B + 1 2
9 8 1 jca φ B + 1 2 B
10 resubcl B + 1 2 B B + 1 2 B
11 9 10 syl φ B + 1 2 B
12 1 dnicld1 φ B + 1 2 B
13 11 leabsd φ B + 1 2 B B + 1 2 B
14 11 12 3 13 lesub2dd φ 1 2 B + 1 2 B 1 2 B + 1 2 B
15 3 recnd φ 1 2
16 8 recnd φ B + 1 2
17 1 recnd φ B
18 15 16 17 subsub3d φ 1 2 B + 1 2 B = 1 2 + B - B + 1 2
19 15 17 addcomd φ 1 2 + B = B + 1 2
20 19 oveq1d φ 1 2 + B - B + 1 2 = B + 1 2 - B + 1 2
21 17 16 15 subsub3d φ B B + 1 2 1 2 = B + 1 2 - B + 1 2
22 21 eqcomd φ B + 1 2 - B + 1 2 = B B + 1 2 1 2
23 18 20 22 3eqtrd φ 1 2 B + 1 2 B = B B + 1 2 1 2
24 14 23 breqtrd φ 1 2 B + 1 2 B B B + 1 2 1 2