Metamath Proof Explorer

Theorem dnibndlem6

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

Ref Expression
Hypotheses dnibndlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dnibndlem6.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion dnibndlem6 ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem6.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dnibndlem6.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 2 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ )
4 3 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℂ )
5 1 dnicld1 ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ )
7 4 6 subcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℂ )
8 7 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
9 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
10 9 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
11 4 10 subcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ∈ ℂ )
12 11 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) ∈ ℝ )
13 10 6 subcld ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
15 12 14 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) + ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ) ∈ ℝ )
16 halfre ⊢ ( 1 / 2 ) ∈ ℝ
17 16 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
18 17 3 jca ⊢ ( 𝜑 → ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ ) )
19 resubcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℝ ) → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ∈ ℝ )
20 18 19 syl ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ∈ ℝ )
21 17 5 jca ⊢ ( 𝜑 → ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ ) )
22 resubcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ ) → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
23 21 22 syl ⊢ ( 𝜑 → ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ∈ ℝ )
24 20 23 readdcld ⊢ ( 𝜑 → ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ∈ ℝ )
25 4 6 10 3jca ⊢ ( 𝜑 → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℂ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) )
26 abs3dif ⊢ ( ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ∈ ℂ ∧ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) + ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ) )
27 25 26 syl ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) + ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ) )
28 4 10 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) = ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ) )
29 rddif2 ⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
30 2 29 syl ⊢ ( 𝜑 → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
31 20 30 absidd ⊢ ( 𝜑 → ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) ) = ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
32 28 31 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) = ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) )
33 rddif2 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
34 1 33 syl ⊢ ( 𝜑 → 0 ≤ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
35 23 34 absidd ⊢ ( 𝜑 → ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) = ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) )
36 32 35 oveq12d ⊢ ( 𝜑 → ( ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) + ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ) = ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) )
37 15 36 eqled ⊢ ( 𝜑 → ( ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( 1 / 2 ) ) ) + ( abs ‘ ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ) ≤ ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) )
38 8 15 24 27 37 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) ≤ ( ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − 𝐵 ) ) ) + ( ( 1 / 2 ) − ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ) ) )