Proof of Theorem flnn0div2ge
Step | Hyp | Ref
| Expression |
1 | | nn0eo 45874 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 / 2) ∈
ℕ0 ∨ ((𝑁 + 1) / 2) ∈
ℕ0)) |
2 | | nn0re 12242 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
3 | | peano2rem 11288 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℝ) |
5 | 4 | adantl 482 |
. . . . . 6
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 1) ∈ ℝ) |
6 | 2 | adantl 482 |
. . . . . 6
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℝ) |
7 | | 2rp 12735 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℝ+) |
9 | 2 | lem1d 11908 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ≤
𝑁) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 1) ≤ 𝑁) |
11 | 5, 6, 8, 10 | lediv1dd 12830 |
. . . . 5
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 − 1) / 2) ≤ (𝑁 / 2)) |
12 | | nn0z 12343 |
. . . . . . 7
⊢ ((𝑁 / 2) ∈ ℕ0
→ (𝑁 / 2) ∈
ℤ) |
13 | | flid 13528 |
. . . . . . 7
⊢ ((𝑁 / 2) ∈ ℤ →
(⌊‘(𝑁 / 2)) =
(𝑁 / 2)) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝑁 / 2) ∈ ℕ0
→ (⌊‘(𝑁 /
2)) = (𝑁 /
2)) |
15 | 14 | adantr 481 |
. . . . 5
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝑁 / 2)) = (𝑁 / 2)) |
16 | 11, 15 | breqtrrd 5102 |
. . . 4
⊢ (((𝑁 / 2) ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2))) |
17 | 16 | ex 413 |
. . 3
⊢ ((𝑁 / 2) ∈ ℕ0
→ (𝑁 ∈
ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2)))) |
18 | | nn0o 16092 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 − 1) / 2) ∈
ℕ0) |
19 | 18 | ex 413 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) / 2)
∈ ℕ0 → ((𝑁 − 1) / 2) ∈
ℕ0)) |
20 | | nn0z 12343 |
. . . . . . . 8
⊢ (((𝑁 − 1) / 2) ∈
ℕ0 → ((𝑁 − 1) / 2) ∈
ℤ) |
21 | 20 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → ((𝑁 − 1) / 2) ∈
ℤ) |
22 | | flid 13528 |
. . . . . . 7
⊢ (((𝑁 − 1) / 2) ∈ ℤ
→ (⌊‘((𝑁
− 1) / 2)) = ((𝑁
− 1) / 2)) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → (⌊‘((𝑁 − 1) / 2)) = ((𝑁 − 1) / 2)) |
24 | 4 | rehalfcld 12220 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) / 2)
∈ ℝ) |
25 | 24 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → ((𝑁 − 1) / 2) ∈
ℝ) |
26 | 2 | rehalfcld 12220 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 / 2) ∈
ℝ) |
27 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → (𝑁 / 2) ∈ ℝ) |
28 | | 2re 12047 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
29 | | 2pos 12076 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
30 | 28, 29 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (2 ∈ ℝ ∧ 0 < 2)) |
32 | | lediv1 11840 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((𝑁 − 1) ≤ 𝑁 ↔ ((𝑁 − 1) / 2) ≤ (𝑁 / 2))) |
33 | 4, 2, 31, 32 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) ≤
𝑁 ↔ ((𝑁 − 1) / 2) ≤ (𝑁 / 2))) |
34 | 9, 33 | mpbid 231 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) / 2)
≤ (𝑁 /
2)) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → ((𝑁 − 1) / 2) ≤ (𝑁 / 2)) |
36 | | flwordi 13532 |
. . . . . . 7
⊢ ((((𝑁 − 1) / 2) ∈ ℝ
∧ (𝑁 / 2) ∈
ℝ ∧ ((𝑁 −
1) / 2) ≤ (𝑁 / 2))
→ (⌊‘((𝑁
− 1) / 2)) ≤ (⌊‘(𝑁 / 2))) |
37 | 25, 27, 35, 36 | syl3anc 1370 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → (⌊‘((𝑁 − 1) / 2)) ≤ (⌊‘(𝑁 / 2))) |
38 | 23, 37 | eqbrtrrd 5098 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 − 1) / 2)
∈ ℕ0) → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2))) |
39 | 38 | ex 413 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 − 1) / 2)
∈ ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2)))) |
40 | 19, 39 | syldc 48 |
. . 3
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤
(⌊‘(𝑁 /
2)))) |
41 | 17, 40 | jaoi 854 |
. 2
⊢ (((𝑁 / 2) ∈ ℕ0
∨ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤
(⌊‘(𝑁 /
2)))) |
42 | 1, 41 | mpcom 38 |
1
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) / 2)
≤ (⌊‘(𝑁 /
2))) |