Proof of Theorem dnibndlem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dnibndlem3.3 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 2 | 1 | recnd 11290 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 3 |  | halfre 12481 | . . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ | 
| 4 | 3 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (1 / 2) ∈
ℝ) | 
| 5 | 1, 4 | jca 511 | . . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1 / 2) ∈
ℝ)) | 
| 6 |  | readdcl 11239 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝐵 +
(1 / 2)) ∈ ℝ) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 + (1 / 2)) ∈ ℝ) | 
| 8 |  | reflcl 13837 | . . . . . . . . 9
⊢ ((𝐵 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐵 +
(1 / 2))) ∈ ℝ) | 
| 9 | 7, 8 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℝ) | 
| 10 | 9 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℂ) | 
| 11 |  | halfcn 12482 | . . . . . . . 8
⊢ (1 / 2)
∈ ℂ | 
| 12 | 11 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (1 / 2) ∈
ℂ) | 
| 13 | 10, 12 | subcld 11621 | . . . . . 6
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℂ) | 
| 14 |  | dnibndlem3.2 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 15 | 14 | recnd 11290 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 16 | 2, 13, 15 | 3jca 1128 | . . . . 5
⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℂ ∧ 𝐴
∈ ℂ)) | 
| 17 |  | npncan 11531 | . . . . 5
⊢ ((𝐵 ∈ ℂ ∧
((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − 𝐴)) = (𝐵 − 𝐴)) | 
| 18 | 16, 17 | syl 17 | . . . 4
⊢ (𝜑 → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − 𝐴)) = (𝐵 − 𝐴)) | 
| 19 | 18 | eqcomd 2742 | . . 3
⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − 𝐴))) | 
| 20 |  | dnibndlem3.4 | . . . . . . 7
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) =
((⌊‘(𝐴 + (1 /
2))) + 1)) | 
| 21 | 20 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)) =
(((⌊‘(𝐴 + (1 /
2))) + 1) − (1 / 2))) | 
| 22 | 14, 4 | jca 511 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1 / 2) ∈
ℝ)) | 
| 23 |  | readdcl 11239 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝐴 +
(1 / 2)) ∈ ℝ) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / 2)) ∈ ℝ) | 
| 25 |  | reflcl 13837 | . . . . . . . . . 10
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℝ) | 
| 27 | 26 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℂ) | 
| 28 |  | 1cnd 11257 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) | 
| 29 | 27, 28, 12 | 3jca 1128 | . . . . . . 7
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) ∈ ℂ
∧ 1 ∈ ℂ ∧ (1 / 2) ∈ ℂ)) | 
| 30 |  | addsubass 11519 | . . . . . . 7
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℂ ∧ 1 ∈ ℂ ∧ (1 / 2) ∈ ℂ)
→ (((⌊‘(𝐴
+ (1 / 2))) + 1) − (1 / 2)) = ((⌊‘(𝐴 + (1 / 2))) + (1 − (1 /
2)))) | 
| 31 | 29, 30 | syl 17 | . . . . . 6
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + 1) − (1 /
2)) = ((⌊‘(𝐴 +
(1 / 2))) + (1 − (1 / 2)))) | 
| 32 |  | 1mhlfehlf 12487 | . . . . . . . 8
⊢ (1
− (1 / 2)) = (1 / 2) | 
| 33 | 32 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (1 − (1 / 2)) = (1 /
2)) | 
| 34 | 33 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + (1 − (1 /
2))) = ((⌊‘(𝐴 +
(1 / 2))) + (1 / 2))) | 
| 35 | 21, 31, 34 | 3eqtrd 2780 | . . . . 5
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2)) =
((⌊‘(𝐴 + (1 /
2))) + (1 / 2))) | 
| 36 | 35 | oveq1d 7447 | . . . 4
⊢ (𝜑 → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
− 𝐴) =
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)) | 
| 37 | 36 | oveq2d 7448 | . . 3
⊢ (𝜑 → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − 𝐴)) = ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) | 
| 38 | 19, 37 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝐵 − 𝐴) = ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) | 
| 39 | 38 | fveq2d 6909 | 1
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)))) |