Proof of Theorem dnibndlem10
| Step | Hyp | Ref
| Expression |
| 1 | | 1red 11262 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
| 2 | | dnibndlem10.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 3 | | halfre 12480 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
| 4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 5 | 2, 4 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + (1 / 2)) ∈ ℝ) |
| 6 | | reflcl 13836 |
. . . . . . 7
⊢ ((𝐵 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐵 +
(1 / 2))) ∈ ℝ) |
| 7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℝ) |
| 8 | 7, 4 | jca 511 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) ∈ ℝ
∧ (1 / 2) ∈ ℝ)) |
| 9 | | resubcl 11573 |
. . . . 5
⊢
(((⌊‘(𝐵
+ (1 / 2))) ∈ ℝ ∧ (1 / 2) ∈ ℝ) →
((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) ∈ ℝ) |
| 10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℝ) |
| 11 | | dnibndlem10.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 12 | 11, 4 | readdcld 11290 |
. . . . . 6
⊢ (𝜑 → (𝐴 + (1 / 2)) ∈ ℝ) |
| 13 | | reflcl 13836 |
. . . . . 6
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
| 14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℝ) |
| 15 | 14, 4 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℝ) |
| 16 | 10, 15 | jca 511 |
. . 3
⊢ (𝜑 → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℝ ∧ ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℝ)) |
| 17 | | resubcl 11573 |
. . 3
⊢
((((⌊‘(𝐵
+ (1 / 2))) − (1 / 2)) ∈ ℝ ∧ ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℝ) → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2)) −
((⌊‘(𝐴 + (1 /
2))) + (1 / 2))) ∈ ℝ) |
| 18 | 16, 17 | syl 17 |
. 2
⊢ (𝜑 → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
− ((⌊‘(𝐴
+ (1 / 2))) + (1 / 2))) ∈ ℝ) |
| 19 | 2, 11 | resubcld 11691 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
| 20 | 14 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℂ) |
| 21 | | 2cnd 12344 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℂ) |
| 22 | 4 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
| 23 | 20, 21, 22 | addsubassd 11640 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) = ((⌊‘(𝐴 +
(1 / 2))) + (2 − (1 / 2)))) |
| 24 | 23 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2))) =
(((⌊‘(𝐴 + (1 /
2))) + (2 − (1 / 2))) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)))) |
| 25 | 21, 22 | subcld 11620 |
. . . . . 6
⊢ (𝜑 → (2 − (1 / 2)) ∈
ℂ) |
| 26 | 20, 25, 22 | pnpcand 11657 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (2 − (1 /
2))) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2))) = ((2 − (1 /
2)) − (1 / 2))) |
| 27 | 21, 22, 22 | subsub4d 11651 |
. . . . . 6
⊢ (𝜑 → ((2 − (1 / 2))
− (1 / 2)) = (2 − ((1 / 2) + (1 / 2)))) |
| 28 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 29 | | 2halves 12494 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . 8
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
| 31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) + (1 / 2)) =
1) |
| 32 | 31 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (2 − ((1 / 2) + (1 /
2))) = (2 − 1)) |
| 33 | | 2m1e1 12392 |
. . . . . . 7
⊢ (2
− 1) = 1 |
| 34 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (2 − 1) =
1) |
| 35 | 27, 32, 34 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((2 − (1 / 2))
− (1 / 2)) = 1) |
| 36 | 24, 26, 35 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2))) =
1) |
| 37 | 36 | eqcomd 2743 |
. . 3
⊢ (𝜑 → 1 =
((((⌊‘(𝐴 + (1 /
2))) + 2) − (1 / 2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)))) |
| 38 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 39 | 38 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) |
| 40 | 14, 39 | readdcld 11290 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ∈
ℝ) |
| 41 | 40, 4 | jca 511 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + 2) ∈ ℝ
∧ (1 / 2) ∈ ℝ)) |
| 42 | | resubcl 11573 |
. . . . 5
⊢
((((⌊‘(𝐴
+ (1 / 2))) + 2) ∈ ℝ ∧ (1 / 2) ∈ ℝ) →
(((⌊‘(𝐴 + (1 /
2))) + 2) − (1 / 2)) ∈ ℝ) |
| 43 | 41, 42 | syl 17 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) ∈ ℝ) |
| 44 | | dnibndlem10.3 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤
(⌊‘(𝐵 + (1 /
2)))) |
| 45 | 40, 7, 4, 44 | lesub1dd 11879 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) ≤ ((⌊‘(𝐵
+ (1 / 2))) − (1 / 2))) |
| 46 | 43, 10, 15, 45 | lesub1dd 11879 |
. . 3
⊢ (𝜑 → ((((⌊‘(𝐴 + (1 / 2))) + 2) − (1 /
2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2))) ≤
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)))) |
| 47 | 37, 46 | eqbrtrd 5165 |
. 2
⊢ (𝜑 → 1 ≤
(((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) − ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)))) |
| 48 | | flle 13839 |
. . . . 5
⊢ ((𝐵 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐵 +
(1 / 2))) ≤ (𝐵 + (1 /
2))) |
| 49 | 5, 48 | syl 17 |
. . . 4
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ≤ (𝐵 + (1 / 2))) |
| 50 | 7, 4, 2 | lesubaddd 11860 |
. . . 4
⊢ (𝜑 → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
≤ 𝐵 ↔
(⌊‘(𝐵 + (1 /
2))) ≤ (𝐵 + (1 /
2)))) |
| 51 | 49, 50 | mpbird 257 |
. . 3
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
≤ 𝐵) |
| 52 | | fllep1 13841 |
. . . . . 6
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (𝐴 + (1 / 2)) ≤
((⌊‘(𝐴 + (1 /
2))) + 1)) |
| 53 | 12, 52 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 + (1 / 2)) ≤ ((⌊‘(𝐴 + (1 / 2))) +
1)) |
| 54 | 20, 22, 22 | addassd 11283 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 /
2)) = ((⌊‘(𝐴 +
(1 / 2))) + ((1 / 2) + (1 / 2)))) |
| 55 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + ((1 / 2) + (1 /
2))) = ((⌊‘(𝐴 +
(1 / 2))) + 1)) |
| 56 | 54, 55 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 /
2)) = ((⌊‘(𝐴 +
(1 / 2))) + 1)) |
| 57 | 56 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 1) =
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) + (1 / 2))) |
| 58 | 53, 57 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → (𝐴 + (1 / 2)) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 /
2))) |
| 59 | 11, 15, 4 | leadd1d 11857 |
. . . 4
⊢ (𝜑 → (𝐴 ≤ ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ↔ (𝐴 + (1 / 2)) ≤
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) + (1 / 2)))) |
| 60 | 58, 59 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐴 ≤ ((⌊‘(𝐴 + (1 / 2))) + (1 / 2))) |
| 61 | 10, 11, 2, 15, 51, 60 | le2subd 11883 |
. 2
⊢ (𝜑 → (((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
− ((⌊‘(𝐴
+ (1 / 2))) + (1 / 2))) ≤ (𝐵 − 𝐴)) |
| 62 | 1, 18, 19, 47, 61 | letrd 11418 |
1
⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴)) |