Proof of Theorem flhalf
Step | Hyp | Ref
| Expression |
1 | | zre 11973 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
2 | | peano2re 10801 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℝ) |
4 | 3 | rehalfcld 11872 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1) / 2) ∈
ℝ) |
5 | | flltp1 13158 |
. . . . . 6
⊢ (((𝑁 + 1) / 2) ∈ ℝ →
((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1)) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1)) |
7 | 4 | flcld 13156 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℤ) |
8 | 7 | zred 12075 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℝ) |
9 | | 1red 10630 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∈
ℝ) |
10 | 8, 9 | readdcld 10658 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
((⌊‘((𝑁 + 1) /
2)) + 1) ∈ ℝ) |
11 | | 2rp 12382 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
12 | 11 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ+) |
13 | 3, 10, 12 | ltdivmuld 12470 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) <
((⌊‘((𝑁 + 1) /
2)) + 1) ↔ (𝑁 + 1)
< (2 · ((⌊‘((𝑁 + 1) / 2)) + 1)))) |
14 | 6, 13 | mpbid 233 |
. . . 4
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) < (2 ·
((⌊‘((𝑁 + 1) /
2)) + 1))) |
15 | 9 | recnd 10657 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∈
ℂ) |
16 | 15 | 2timesd 11868 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (2
· 1) = (1 + 1)) |
17 | 16 | oveq2d 7161 |
. . . . 5
⊢ (𝑁 ∈ ℤ → ((2
· (⌊‘((𝑁
+ 1) / 2))) + (2 · 1)) = ((2 · (⌊‘((𝑁 + 1) / 2))) + (1 + 1))) |
18 | | 2cnd 11703 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) |
19 | 8 | recnd 10657 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(⌊‘((𝑁 + 1) /
2)) ∈ ℂ) |
20 | 18, 19, 15 | adddid 10653 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (2
· ((⌊‘((𝑁 + 1) / 2)) + 1)) = ((2 ·
(⌊‘((𝑁 + 1) /
2))) + (2 · 1))) |
21 | | 2re 11699 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ) |
23 | 22, 8 | remulcld 10659 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℝ) |
24 | 23 | recnd 10657 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℂ) |
25 | 24, 15, 15 | addassd 10651 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (((2
· (⌊‘((𝑁
+ 1) / 2))) + 1) + 1) = ((2 · (⌊‘((𝑁 + 1) / 2))) + (1 + 1))) |
26 | 17, 20, 25 | 3eqtr4d 2863 |
. . . 4
⊢ (𝑁 ∈ ℤ → (2
· ((⌊‘((𝑁 + 1) / 2)) + 1)) = (((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) + 1)) |
27 | 14, 26 | breqtrd 5083 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) < (((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) + 1)) |
28 | 23, 9 | readdcld 10658 |
. . . 4
⊢ (𝑁 ∈ ℤ → ((2
· (⌊‘((𝑁
+ 1) / 2))) + 1) ∈ ℝ) |
29 | 1, 28, 9 | ltadd1d 11221 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1) ↔ (𝑁 + 1)
< (((2 · (⌊‘((𝑁 + 1) / 2))) + 1) + 1))) |
30 | 27, 29 | mpbird 258 |
. 2
⊢ (𝑁 ∈ ℤ → 𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1)) |
31 | | 2z 12002 |
. . . . 5
⊢ 2 ∈
ℤ |
32 | 31 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℤ → 2 ∈
ℤ) |
33 | 32, 7 | zmulcld 12081 |
. . 3
⊢ (𝑁 ∈ ℤ → (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℤ) |
34 | | zleltp1 12021 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ (2
· (⌊‘((𝑁
+ 1) / 2))) ∈ ℤ) → (𝑁 ≤ (2 · (⌊‘((𝑁 + 1) / 2))) ↔ 𝑁 < ((2 ·
(⌊‘((𝑁 + 1) /
2))) + 1))) |
35 | 33, 34 | mpdan 683 |
. 2
⊢ (𝑁 ∈ ℤ → (𝑁 ≤ (2 ·
(⌊‘((𝑁 + 1) /
2))) ↔ 𝑁 < ((2
· (⌊‘((𝑁
+ 1) / 2))) + 1))) |
36 | 30, 35 | mpbird 258 |
1
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (2 ·
(⌊‘((𝑁 + 1) /
2)))) |