Proof of Theorem flhalf
Step | Hyp | Ref
| Expression |
1 | | peano2z 9248 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) |
2 | | 2nn 9039 |
. . . . . . 7
⊢ 2 ∈
ℕ |
3 | | znq 9583 |
. . . . . . 7
⊢ (((𝑁 + 1) ∈ ℤ ∧ 2
∈ ℕ) → ((𝑁
+ 1) / 2) ∈ ℚ) |
4 | 1, 2, 3 | sylancl 411 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1) / 2) ∈
ℚ) |
5 | | flqltp1 10235 |
. . . . . 6
⊢ (((𝑁 + 1) / 2) ∈ ℚ →
((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1)) |
6 | 4, 5 | syl 14 |
. . . . 5
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1)) |
7 | | zre 9216 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
8 | | peano2re 8055 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
9 | 7, 8 | syl 14 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℝ) |
10 | 4 | flqcld 10233 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℤ) |
11 | 10 | zred 9334 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℝ) |
12 | | 1red 7935 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∈
ℝ) |
13 | 11, 12 | readdcld 7949 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
((⌊‘((𝑁 + 1) /
2)) + 1) ∈ ℝ) |
14 | | 2rp 9615 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
15 | 14 | a1i 9 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ+) |
16 | 9, 13, 15 | ltdivmuld 9705 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1) ↔ (𝑁 + 1)
< (2 · ((⌊‘((𝑁 + 1) / 2)) + 1)))) |
17 | 6, 16 | mpbid 146 |
. . . 4
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) < (2 ·
((⌊‘((𝑁 + 1) /
2)) + 1))) |
18 | 12 | recnd 7948 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∈
ℂ) |
19 | 18 | 2timesd 9120 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (2
· 1) = (1 + 1)) |
20 | 19 | oveq2d 5869 |
. . . . 5
⊢ (𝑁 ∈ ℤ → ((2
· (⌊‘((𝑁
+ 1) / 2))) + (2 · 1)) = ((2 · (⌊‘((𝑁 + 1) / 2))) + (1 + 1))) |
21 | | 2cnd 8951 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) |
22 | 11 | recnd 7948 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℂ) |
23 | 21, 22, 18 | adddid 7944 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (2
· ((⌊‘((𝑁 + 1) / 2)) + 1)) = ((2 ·
(⌊‘((𝑁 + 1) /
2))) + (2 · 1))) |
24 | | 2re 8948 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
25 | 24 | a1i 9 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ) |
26 | 25, 11 | remulcld 7950 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℝ) |
27 | 26 | recnd 7948 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℂ) |
28 | 27, 18, 18 | addassd 7942 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (((2
· (⌊‘((𝑁
+ 1) / 2))) + 1) + 1) = ((2 · (⌊‘((𝑁 + 1) / 2))) + (1 + 1))) |
29 | 20, 23, 28 | 3eqtr4d 2213 |
. . . 4
⊢ (𝑁 ∈ ℤ → (2
· ((⌊‘((𝑁 + 1) / 2)) + 1)) = (((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) + 1)) |
30 | 17, 29 | breqtrd 4015 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) < (((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) + 1)) |
31 | 26, 12 | readdcld 7949 |
. . . 4
⊢ (𝑁 ∈ ℤ → ((2
· (⌊‘((𝑁
+ 1) / 2))) + 1) ∈ ℝ) |
32 | 7, 31, 12 | ltadd1d 8457 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) ↔ (𝑁 + 1)
< (((2 · (⌊‘((𝑁 + 1) / 2))) + 1) + 1))) |
33 | 30, 32 | mpbird 166 |
. 2
⊢ (𝑁 ∈ ℤ → 𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1)) |
34 | | 2z 9240 |
. . . . 5
⊢ 2 ∈
ℤ |
35 | 34 | a1i 9 |
. . . 4
⊢ (𝑁 ∈ ℤ → 2 ∈
ℤ) |
36 | 35, 10 | zmulcld 9340 |
. . 3
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℤ) |
37 | | zleltp1 9267 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℤ) → (𝑁 ≤ (2 · (⌊‘((𝑁 + 1) / 2))) ↔ 𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1))) |
38 | 36, 37 | mpdan 419 |
. 2
⊢ (𝑁 ∈ ℤ → (𝑁 ≤ (2 ·
(⌊‘((𝑁 + 1) /
2))) ↔ 𝑁 < ((2
· (⌊‘((𝑁
+ 1) / 2))) + 1))) |
39 | 33, 38 | mpbird 166 |
1
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (2 ·
(⌊‘((𝑁 + 1) /
2)))) |