Proof of Theorem fldiv4lem1div2uz2
Step | Hyp | Ref
| Expression |
1 | | eluzelz 11573 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
2 | | zre 11258 |
. . . 4
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
3 | | id 22 |
. . . . 5
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
4 | | 4re 10974 |
. . . . . 6
⊢ 4 ∈
ℝ |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℝ → 4 ∈
ℝ) |
6 | | 4ne0 10994 |
. . . . . 6
⊢ 4 ≠
0 |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℝ → 4 ≠
0) |
8 | 3, 5, 7 | redivcld 10732 |
. . . 4
⊢ (𝑁 ∈ ℝ → (𝑁 / 4) ∈
ℝ) |
9 | 2, 8 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 / 4) ∈
ℝ) |
10 | | flle 12462 |
. . 3
⊢ ((𝑁 / 4) ∈ ℝ →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) |
11 | 1, 9, 10 | 3syl 18 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ (𝑁 / 4)) |
12 | | 1red 9934 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℝ) |
13 | | eluzelre 11574 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
14 | | rehalfcl 11135 |
. . . . 5
⊢ (𝑁 ∈ ℝ → (𝑁 / 2) ∈
ℝ) |
15 | 1, 2, 14 | 3syl 18 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ∈ ℝ) |
16 | | 2rp 11713 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℝ+) |
18 | | eluzle 11576 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
19 | | divge1 11774 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 ≤ (𝑁 / 2)) |
20 | 17, 13, 18, 19 | syl3anc 1318 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (𝑁 / 2)) |
21 | | eluzelcn 11575 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
22 | | subhalfhalf 11143 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → (𝑁 − (𝑁 / 2)) = (𝑁 / 2)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (𝑁 / 2)) = (𝑁 / 2)) |
24 | 20, 23 | breqtrrd 4611 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (𝑁 − (𝑁 / 2))) |
25 | 12, 13, 15, 24 | lesubd 10510 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ≤ (𝑁 − 1)) |
26 | | 2t2e4 11054 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
27 | 26 | eqcomi 2619 |
. . . . . . . 8
⊢ 4 = (2
· 2) |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 = (2 · 2)) |
29 | 28 | oveq2d 6565 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = (𝑁 / (2 · 2))) |
30 | | 2cnne0 11119 |
. . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ∈ ℂ ∧ 2 ≠
0)) |
32 | | divdiv1 10615 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) |
33 | 21, 31, 31, 32 | syl3anc 1318 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) |
34 | 29, 33 | eqtr4d 2647 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = ((𝑁 / 2) / 2)) |
35 | 34 | breq1d 4593 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) |
36 | | peano2rem 10227 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
37 | | 2re 10967 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
38 | | 2pos 10989 |
. . . . . . . . 9
⊢ 0 <
2 |
39 | 37, 38 | pm3.2i 470 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 0 < 2) |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → (2 ∈
ℝ ∧ 0 < 2)) |
41 | 14, 36, 40 | 3jca 1235 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → ((𝑁 / 2) ∈ ℝ ∧
(𝑁 − 1) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2))) |
42 | 1, 2, 41 | 3syl 18 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2))) |
43 | | lediv1 10767 |
. . . . 5
⊢ (((𝑁 / 2) ∈ ℝ ∧
(𝑁 − 1) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 2) ≤ (𝑁 − 1) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) |
44 | 42, 43 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) ≤ (𝑁 − 1) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) |
45 | 35, 44 | bitr4d 270 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ (𝑁 / 2) ≤ (𝑁 − 1))) |
46 | 25, 45 | mpbird 246 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) ≤ ((𝑁 − 1) / 2)) |
47 | 8 | flcld 12461 |
. . . . . 6
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℤ) |
48 | 47 | zred 11358 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℝ) |
49 | 36 | rehalfcld 11156 |
. . . . 5
⊢ (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈
ℝ) |
50 | 48, 8, 49 | 3jca 1235 |
. . . 4
⊢ (𝑁 ∈ ℝ →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ ((𝑁
− 1) / 2) ∈ ℝ)) |
51 | 1, 2, 50 | 3syl 18 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((⌊‘(𝑁 / 4)) ∈ ℝ ∧ (𝑁 / 4) ∈ ℝ ∧
((𝑁 − 1) / 2) ∈
ℝ)) |
52 | | letr 10010 |
. . 3
⊢
(((⌊‘(𝑁
/ 4)) ∈ ℝ ∧ (𝑁 / 4) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈ ℝ)
→ (((⌊‘(𝑁
/ 4)) ≤ (𝑁 / 4) ∧
(𝑁 / 4) ≤ ((𝑁 − 1) / 2)) →
(⌊‘(𝑁 / 4))
≤ ((𝑁 − 1) /
2))) |
53 | 51, 52 | syl 17 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((⌊‘(𝑁 / 4)) ≤ (𝑁 / 4) ∧ (𝑁 / 4) ≤ ((𝑁 − 1) / 2)) →
(⌊‘(𝑁 / 4))
≤ ((𝑁 − 1) /
2))) |
54 | 11, 46, 53 | mp2and 711 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2)) |