Metamath Proof Explorer

Theorem dnibndlem11

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

Ref Expression
Hypotheses dnibndlem11.1 ⊢φ→A∈ℝ
dnibndlem11.2 ⊢φ→B∈ℝ
Assertion dnibndlem11 ⊢φ→B+12−B−A+12−A≤12

Proof

Step Hyp Ref Expression
1 dnibndlem11.1 ⊢φ→A∈ℝ
2 dnibndlem11.2 ⊢φ→B∈ℝ
3 2 dnicld1 ⊢φ→B+12−B∈ℝ
4 1 dnicld1 ⊢φ→A+12−A∈ℝ
5 3 4 resubcld ⊢φ→B+12−B−A+12−A∈ℝ
6 halfre ⊢12∈ℝ
7 6 a1i ⊢φ→12∈ℝ
8 3 recnd ⊢φ→B+12−B∈ℂ
9 4 recnd ⊢φ→A+12−A∈ℂ
10 8 9 negsubdi2d ⊢φ→−B+12−B−A+12−A=A+12−A−B+12−B
11 4 3 resubcld ⊢φ→A+12−A−B+12−B∈ℝ
12 2 7 readdcld ⊢φ→B+12∈ℝ
13 reflcl ⊢B+12∈ℝ→B+12∈ℝ
14 12 13 syl ⊢φ→B+12∈ℝ
15 14 recnd ⊢φ→B+12∈ℂ
16 2 recnd ⊢φ→B∈ℂ
17 15 16 subcld ⊢φ→B+12−B∈ℂ
18 17 absge0d ⊢φ→0≤B+12−B
19 4 3 subge02d ⊢φ→0≤B+12−B↔A+12−A−B+12−B≤A+12−A
20 18 19 mpbid ⊢φ→A+12−A−B+12−B≤A+12−A
21 rddif ⊢A∈ℝ→A+12−A≤12
22 1 21 syl ⊢φ→A+12−A≤12
23 11 4 7 20 22 letrd ⊢φ→A+12−A−B+12−B≤12
24 10 23 eqbrtrd ⊢φ→−B+12−B−A+12−A≤12
25 5 7 24 lenegcon1d ⊢φ→−12≤B+12−B−A+12−A
26 1 7 readdcld ⊢φ→A+12∈ℝ
27 reflcl ⊢A+12∈ℝ→A+12∈ℝ
28 26 27 syl ⊢φ→A+12∈ℝ
29 28 recnd ⊢φ→A+12∈ℂ
30 1 recnd ⊢φ→A∈ℂ
31 29 30 subcld ⊢φ→A+12−A∈ℂ
32 31 absge0d ⊢φ→0≤A+12−A
33 3 4 subge02d ⊢φ→0≤A+12−A↔B+12−B−A+12−A≤B+12−B
34 32 33 mpbid ⊢φ→B+12−B−A+12−A≤B+12−B
35 rddif ⊢B∈ℝ→B+12−B≤12
36 2 35 syl ⊢φ→B+12−B≤12
37 5 3 7 34 36 letrd ⊢φ→B+12−B−A+12−A≤12
38 25 37 jca ⊢φ→−12≤B+12−B−A+12−A∧B+12−B−A+12−A≤12
39 5 7 absled ⊢φ→B+12−B−A+12−A≤12↔−12≤B+12−B−A+12−A∧B+12−B−A+12−A≤12
40 38 39 mpbird ⊢φ→B+12−B−A+12−A≤12