Metamath Proof Explorer

Theorem dnibndlem3

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

Ref Expression
Hypotheses dnibndlem3.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
dnibndlem3.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dnibndlem3.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dnibndlem3.4 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
Assertion dnibndlem3 ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem3.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnibndlem3.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dnibndlem3.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 dnibndlem3.4 ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
5 3 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6 halfre ⊢ ( 1 / 2 ) ∈ ℝ
7 6 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
8 3 7 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
9 readdcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
10 8 9 syl ⊢ ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
11 reflcl ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
12 10 11 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
13 12 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℂ )
14 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
15 14 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
16 13 15 subcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℂ )
17 2 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
18 5 16 17 3jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
19 npncan ⊢ ( ( 𝐵 ∈ ℂ ∧ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
20 18 19 syl ⊢ ( 𝜑 → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
21 20 eqcomd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − 𝐴 ) ) )
22 4 oveq1d ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) − ( 1 / 2 ) ) )
23 2 7 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
24 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
25 23 24 syl ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
26 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
27 25 26 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
28 27 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
29 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
30 28 29 15 3jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) )
31 addsubass ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) − ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 − ( 1 / 2 ) ) ) )
32 30 31 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) − ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 − ( 1 / 2 ) ) ) )
33 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
34 33 a1i ⊢ ( 𝜑 → ( 1 − ( 1 / 2 ) ) = ( 1 / 2 ) )
35 34 oveq2d ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 − ( 1 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
36 22 32 35 3eqtrd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
37 36 oveq1d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − 𝐴 ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )
38 37 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − 𝐴 ) ) = ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
39 21 38 eqtrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
40 39 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( 𝐵 − ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ) + ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) ) )