Proof of Theorem fldiv4lem1div2uz2
Step | Hyp | Ref
| Expression |
1 | | eluzelz 12875 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
2 | | zre 12605 |
. . 3
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
3 | | id 22 |
. . . 4
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
4 | | 4re 12339 |
. . . . 5
⊢ 4 ∈
ℝ |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℝ → 4 ∈
ℝ) |
6 | | 4ne0 12363 |
. . . . 5
⊢ 4 ≠
0 |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℝ → 4 ≠
0) |
8 | 3, 5, 7 | redivcld 12084 |
. . 3
⊢ (𝑁 ∈ ℝ → (𝑁 / 4) ∈
ℝ) |
9 | | flle 13810 |
. . 3
⊢ ((𝑁 / 4) ∈ ℝ →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) |
10 | 1, 2, 8, 9 | 4syl 19 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ (𝑁 / 4)) |
11 | | 1red 11253 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℝ) |
12 | | eluzelre 12876 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
13 | | rehalfcl 12481 |
. . . . 5
⊢ (𝑁 ∈ ℝ → (𝑁 / 2) ∈
ℝ) |
14 | 1, 2, 13 | 3syl 18 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ∈ ℝ) |
15 | | 2rp 13024 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℝ+) |
17 | | eluzle 12878 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
18 | | divge1 13087 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 ≤ (𝑁 / 2)) |
19 | 16, 12, 17, 18 | syl3anc 1368 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (𝑁 / 2)) |
20 | | eluzelcn 12877 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
21 | | subhalfhalf 12489 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → (𝑁 − (𝑁 / 2)) = (𝑁 / 2)) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (𝑁 / 2)) = (𝑁 / 2)) |
23 | 19, 22 | breqtrrd 5171 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (𝑁 − (𝑁 / 2))) |
24 | 11, 12, 14, 23 | lesubd 11856 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ≤ (𝑁 − 1)) |
25 | | 2t2e4 12419 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
26 | 25 | eqcomi 2735 |
. . . . . . . 8
⊢ 4 = (2
· 2) |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 = (2 · 2)) |
28 | 27 | oveq2d 7429 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = (𝑁 / (2 · 2))) |
29 | | 2cnne0 12465 |
. . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ∈ ℂ ∧ 2 ≠
0)) |
31 | | divdiv1 11967 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) |
32 | 20, 30, 30, 31 | syl3anc 1368 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) |
33 | 28, 32 | eqtr4d 2769 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = ((𝑁 / 2) / 2)) |
34 | 33 | breq1d 5153 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) |
35 | | peano2rem 11565 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
36 | 12, 35 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℝ) |
37 | 14, 36, 16 | lediv1d 13107 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) ≤ (𝑁 − 1) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) |
38 | 34, 37 | bitr4d 281 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ (𝑁 / 2) ≤ (𝑁 − 1))) |
39 | 24, 38 | mpbird 256 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) ≤ ((𝑁 − 1) / 2)) |
40 | 8 | flcld 13809 |
. . . . 5
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℤ) |
41 | 40 | zred 12709 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℝ) |
42 | 35 | rehalfcld 12502 |
. . . 4
⊢ (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈
ℝ) |
43 | 41, 8, 42 | 3jca 1125 |
. . 3
⊢ (𝑁 ∈ ℝ →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ ((𝑁
− 1) / 2) ∈ ℝ)) |
44 | | letr 11346 |
. . 3
⊢
(((⌊‘(𝑁
/ 4)) ∈ ℝ ∧ (𝑁 / 4) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈ ℝ)
→ (((⌊‘(𝑁
/ 4)) ≤ (𝑁 / 4) ∧
(𝑁 / 4) ≤ ((𝑁 − 1) / 2)) →
(⌊‘(𝑁 / 4))
≤ ((𝑁 − 1) /
2))) |
45 | 1, 2, 43, 44 | 4syl 19 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((⌊‘(𝑁 / 4)) ≤ (𝑁 / 4) ∧ (𝑁 / 4) ≤ ((𝑁 − 1) / 2)) →
(⌊‘(𝑁 / 4))
≤ ((𝑁 − 1) /
2))) |
46 | 10, 39, 45 | mp2and 697 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2)) |