Metamath Proof Explorer

Theorem dnibndlem12

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

Ref Expression
Hypotheses dnibndlem12.1 ⊢T=x∈ℝ⟼x+12−x
dnibndlem12.2 ⊢φ→A∈ℝ
dnibndlem12.3 ⊢φ→B∈ℝ
dnibndlem12.4 ⊢φ→A+12+2≤B+12
Assertion dnibndlem12 ⊢φ→T⁡B−T⁡A≤B−A

Proof

Step Hyp Ref Expression
1 dnibndlem12.1 ⊢T=x∈ℝ⟼x+12−x
2 dnibndlem12.2 ⊢φ→A∈ℝ
3 dnibndlem12.3 ⊢φ→B∈ℝ
4 dnibndlem12.4 ⊢φ→A+12+2≤B+12
5 3 dnicld1 ⊢φ→B+12−B∈ℝ
6 2 dnicld1 ⊢φ→A+12−A∈ℝ
7 5 6 resubcld ⊢φ→B+12−B−A+12−A∈ℝ
8 7 recnd ⊢φ→B+12−B−A+12−A∈ℂ
9 8 abscld ⊢φ→B+12−B−A+12−A∈ℝ
10 1red ⊢φ→1∈ℝ
11 3 2 resubcld ⊢φ→B−A∈ℝ
12 11 recnd ⊢φ→B−A∈ℂ
13 12 abscld ⊢φ→B−A∈ℝ
14 10 rehalfcld ⊢φ→12∈ℝ
15 2 3 dnibndlem11 ⊢φ→B+12−B−A+12−A≤12
16 halflt1 ⊢12<1
17 halfre ⊢12∈ℝ
18 1re ⊢1∈ℝ
19 17 18 pm3.2i ⊢12∈ℝ∧1∈ℝ
20 ltle ⊢12∈ℝ∧1∈ℝ→12<1→12≤1
21 19 20 ax-mp ⊢12<1→12≤1
22 16 21 ax-mp ⊢12≤1
23 22 a1i ⊢φ→12≤1
24 9 14 10 15 23 letrd ⊢φ→B+12−B−A+12−A≤1
25 2 3 4 dnibndlem10 ⊢φ→1≤B−A
26 11 leabsd ⊢φ→B−A≤B−A
27 10 11 13 25 26 letrd ⊢φ→1≤B−A
28 9 10 13 24 27 letrd ⊢φ→B+12−B−A+12−A≤B−A
29 1 2 3 dnibndlem1 ⊢φ→T⁡B−T⁡A≤B−A↔B+12−B−A+12−A≤B−A
30 28 29 mpbird ⊢φ→T⁡B−T⁡A≤B−A