Metamath Proof Explorer

Theorem dnibndlem9

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem9.1 ⊢T=x∈ℝ⟼x+12−x
2 dnibndlem9.2 ⊢φ→A∈ℝ
3 dnibndlem9.3 ⊢φ→B∈ℝ
4 dnibndlem9.4 ⊢φ→B+12=A+12+1
5 3 dnicld1 ⊢φ→B+12−B∈ℝ
6 5 recnd ⊢φ→B+12−B∈ℂ
7 2 dnicld1 ⊢φ→A+12−A∈ℝ
8 7 recnd ⊢φ→A+12−A∈ℂ
9 6 8 subcld ⊢φ→B+12−B−A+12−A∈ℂ
10 9 abscld ⊢φ→B+12−B−A+12−A∈ℝ
11 halfre ⊢12∈ℝ
12 11 a1i ⊢φ→12∈ℝ
13 12 5 jca ⊢φ→12∈ℝ∧B+12−B∈ℝ
14 resubcl ⊢12∈ℝ∧B+12−B∈ℝ→12−B+12−B∈ℝ
15 13 14 syl ⊢φ→12−B+12−B∈ℝ
16 12 7 jca ⊢φ→12∈ℝ∧A+12−A∈ℝ
17 resubcl ⊢12∈ℝ∧A+12−A∈ℝ→12−A+12−A∈ℝ
18 16 17 syl ⊢φ→12−A+12−A∈ℝ
19 15 18 readdcld ⊢φ→12−B+12−B+12-A+12−A∈ℝ
20 3 recnd ⊢φ→B∈ℂ
21 3 12 readdcld ⊢φ→B+12∈ℝ
22 reflcl ⊢B+12∈ℝ→B+12∈ℝ
23 21 22 syl ⊢φ→B+12∈ℝ
24 23 recnd ⊢φ→B+12∈ℂ
25 12 recnd ⊢φ→12∈ℂ
26 24 25 subcld ⊢φ→B+12−12∈ℂ
27 20 26 subcld ⊢φ→B−B+12−12∈ℂ
28 2 12 readdcld ⊢φ→A+12∈ℝ
29 reflcl ⊢A+12∈ℝ→A+12∈ℝ
30 28 29 syl ⊢φ→A+12∈ℝ
31 30 recnd ⊢φ→A+12∈ℂ
32 31 25 addcld ⊢φ→A+12+12∈ℂ
33 2 recnd ⊢φ→A∈ℂ
34 32 33 subcld ⊢φ→A+12+12-A∈ℂ
35 27 34 addcld ⊢φ→B−B+12−12+A+12+12-A∈ℂ
36 35 abscld ⊢φ→B−B+12−12+A+12+12-A∈ℝ
37 2 3 dnibndlem6 ⊢φ→B+12−B−A+12−A≤12−B+12−B+12-A+12−A
38 23 12 jca ⊢φ→B+12∈ℝ∧12∈ℝ
39 resubcl ⊢B+12∈ℝ∧12∈ℝ→B+12−12∈ℝ
40 38 39 syl ⊢φ→B+12−12∈ℝ
41 3 40 jca ⊢φ→B∈ℝ∧B+12−12∈ℝ
42 resubcl ⊢B∈ℝ∧B+12−12∈ℝ→B−B+12−12∈ℝ
43 41 42 syl ⊢φ→B−B+12−12∈ℝ
44 30 12 readdcld ⊢φ→A+12+12∈ℝ
45 44 2 jca ⊢φ→A+12+12∈ℝ∧A∈ℝ
46 resubcl ⊢A+12+12∈ℝ∧A∈ℝ→A+12+12-A∈ℝ
47 45 46 syl ⊢φ→A+12+12-A∈ℝ
48 3 dnibndlem7 ⊢φ→12−B+12−B≤B−B+12−12
49 2 dnibndlem8 ⊢φ→12−A+12−A≤A+12+12-A
50 15 18 43 47 48 49 le2addd ⊢φ→12−B+12−B+12-A+12−A≤B−B+12−12+A+12+12-A
51 43 47 readdcld ⊢φ→B−B+12−12+A+12+12-A∈ℝ
52 dnibndlem4 ⊢B∈ℝ→0≤B−B+12−12
53 3 52 syl ⊢φ→0≤B−B+12−12
54 0red ⊢φ→0∈ℝ
55 dnibndlem5 ⊢A∈ℝ→0<A+12+12-A
56 2 55 syl ⊢φ→0<A+12+12-A
57 54 47 56 ltled ⊢φ→0≤A+12+12-A
58 43 47 53 57 addge0d ⊢φ→0≤B−B+12−12+A+12+12-A
59 51 58 absidd ⊢φ→B−B+12−12+A+12+12-A=B−B+12−12+A+12+12-A
60 59 eqcomd ⊢φ→B−B+12−12+A+12+12-A=B−B+12−12+A+12+12-A
61 50 60 breqtrd ⊢φ→12−B+12−B+12-A+12−A≤B−B+12−12+A+12+12-A
62 10 19 36 37 61 letrd ⊢φ→B+12−B−A+12−A≤B−B+12−12+A+12+12-A
63 1 2 3 4 dnibndlem3 ⊢φ→B−A=B−B+12−12+A+12+12-A
64 63 eqcomd ⊢φ→B−B+12−12+A+12+12-A=B−A
65 62 64 breqtrd ⊢φ→B+12−B−A+12−A≤B−A
66 1 2 3 dnibndlem1 ⊢φ→T⁡B−T⁡A≤B−A↔B+12−B−A+12−A≤B−A
67 65 66 mpbird ⊢φ→T⁡B−T⁡A≤B−A