Metamath Proof Explorer

Theorem dnibndlem2

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem2.1 ⊢T=x∈ℝ⟼x+12−x
2 dnibndlem2.2 ⊢φ→A∈ℝ
3 dnibndlem2.3 ⊢φ→B∈ℝ
4 dnibndlem2.4 ⊢φ→B+12=A+12
5 halfre ⊢12∈ℝ
6 5 a1i ⊢φ→12∈ℝ
7 3 6 jca ⊢φ→B∈ℝ∧12∈ℝ
8 readdcl ⊢B∈ℝ∧12∈ℝ→B+12∈ℝ
9 7 8 syl ⊢φ→B+12∈ℝ
10 reflcl ⊢B+12∈ℝ→B+12∈ℝ
11 9 10 syl ⊢φ→B+12∈ℝ
12 11 recnd ⊢φ→B+12∈ℂ
13 3 recnd ⊢φ→B∈ℂ
14 12 13 subcld ⊢φ→B+12−B∈ℂ
15 14 abscld ⊢φ→B+12−B∈ℝ
16 15 recnd ⊢φ→B+12−B∈ℂ
17 4 12 eqeltrrd ⊢φ→A+12∈ℂ
18 2 recnd ⊢φ→A∈ℂ
19 17 18 subcld ⊢φ→A+12−A∈ℂ
20 19 abscld ⊢φ→A+12−A∈ℝ
21 20 recnd ⊢φ→A+12−A∈ℂ
22 16 21 subcld ⊢φ→B+12−B−A+12−A∈ℂ
23 22 abscld ⊢φ→B+12−B−A+12−A∈ℝ
24 14 19 subcld ⊢φ→B+12-B-A+12−A∈ℂ
25 24 abscld ⊢φ→B+12-B-A+12−A∈ℝ
26 13 18 subcld ⊢φ→B−A∈ℂ
27 26 abscld ⊢φ→B−A∈ℝ
28 14 19 abs2difabsd ⊢φ→B+12−B−A+12−A≤B+12-B-A+12−A
29 12 18 13 nnncan1d ⊢φ→B+12-A-B+12−B=B−A
30 29 eqcomd ⊢φ→B−A=B+12-A-B+12−B
31 30 fveq2d ⊢φ→B−A=B+12-A-B+12−B
32 4 oveq1d ⊢φ→B+12−A=A+12−A
33 32 oveq1d ⊢φ→B+12-A-B+12−B=A+12-A-B+12−B
34 33 fveq2d ⊢φ→B+12-A-B+12−B=A+12-A-B+12−B
35 19 14 abssubd ⊢φ→A+12-A-B+12−B=B+12-B-A+12−A
36 31 34 35 3eqtrd ⊢φ→B−A=B+12-B-A+12−A
37 27 leidd ⊢φ→B−A≤B−A
38 36 37 eqbrtrrd ⊢φ→B+12-B-A+12−A≤B−A
39 23 25 27 28 38 letrd ⊢φ→B+12−B−A+12−A≤B−A
40 1 2 3 dnibndlem1 ⊢φ→T⁡B−T⁡A≤B−A↔B+12−B−A+12−A≤B−A
41 39 40 mpbird ⊢φ→T⁡B−T⁡A≤B−A