Proof of Theorem dnibndlem5
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
2 | | halfre 11123 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (1 / 2)
∈ ℝ) |
4 | 1, 3 | jca 553 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℝ ∧ (1 / 2)
∈ ℝ)) |
5 | | readdcl 9898 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝐴 +
(1 / 2)) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 + (1 / 2)) ∈
ℝ) |
7 | | flltp1 12463 |
. . . . 5
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (𝐴 + (1 / 2)) <
((⌊‘(𝐴 + (1 /
2))) + 1)) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴 + (1 / 2)) <
((⌊‘(𝐴 + (1 /
2))) + 1)) |
9 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
10 | | 2halves 11137 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
12 | 11 | eqcomi 2619 |
. . . . . . 7
⊢ 1 = ((1 /
2) + (1 / 2)) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 1 = ((1 /
2) + (1 / 2))) |
14 | 13 | oveq2d 6565 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) + 1) = ((⌊‘(𝐴 + (1 / 2))) + ((1 / 2) + (1 /
2)))) |
15 | | reflcl 12459 |
. . . . . . . . . 10
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
16 | 6, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℝ) |
17 | 16 | recnd 9947 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℂ) |
18 | 3 | recnd 9947 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (1 / 2)
∈ ℂ) |
19 | 17, 18, 18 | 3jca 1235 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (1 / 2) ∈
ℂ)) |
20 | | addass 9902 |
. . . . . . 7
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (1 / 2) ∈
ℂ) → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 / 2)) =
((⌊‘(𝐴 + (1 /
2))) + ((1 / 2) + (1 / 2)))) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) + (1 / 2)) = ((⌊‘(𝐴 + (1 / 2))) + ((1 / 2) + (1 /
2)))) |
22 | 21 | eqcomd 2616 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) + ((1 / 2) + (1 / 2))) = (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 /
2))) |
23 | 14, 22 | eqtrd 2644 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) + 1) = (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) + (1 /
2))) |
24 | 8, 23 | breqtrd 4609 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐴 + (1 / 2)) <
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) + (1 / 2))) |
25 | 16, 3 | jca 553 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) ∈ ℝ ∧ (1 / 2) ∈ ℝ)) |
26 | | readdcl 9898 |
. . . . 5
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℝ ∧ (1 / 2) ∈ ℝ) →
((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) ∈ ℝ) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) ∈ ℝ) |
28 | 1, 27, 3 | ltadd1d 10499 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐴 < ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ↔
(𝐴 + (1 / 2)) <
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) + (1 / 2)))) |
29 | 24, 28 | mpbird 246 |
. 2
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘(𝐴 + (1 / 2))) + (1 /
2))) |
30 | 1, 27 | posdifd 10493 |
. 2
⊢ (𝐴 ∈ ℝ → (𝐴 < ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ↔ 0
< (((⌊‘(𝐴 +
(1 / 2))) + (1 / 2)) − 𝐴))) |
31 | 29, 30 | mpbid 221 |
1
⊢ (𝐴 ∈ ℝ → 0 <
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)) |