Proof of Theorem fldiv4lem1div2uz2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eluzelz 12888 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) | 
| 2 |  | zre 12617 | . . 3
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 3 |  | id 22 | . . . 4
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) | 
| 4 |  | 4re 12350 | . . . . 5
⊢ 4 ∈
ℝ | 
| 5 | 4 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℝ → 4 ∈
ℝ) | 
| 6 |  | 4ne0 12374 | . . . . 5
⊢ 4 ≠
0 | 
| 7 | 6 | a1i 11 | . . . 4
⊢ (𝑁 ∈ ℝ → 4 ≠
0) | 
| 8 | 3, 5, 7 | redivcld 12095 | . . 3
⊢ (𝑁 ∈ ℝ → (𝑁 / 4) ∈
ℝ) | 
| 9 |  | flle 13839 | . . 3
⊢ ((𝑁 / 4) ∈ ℝ →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) | 
| 10 | 1, 2, 8, 9 | 4syl 19 | . 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ (𝑁 / 4)) | 
| 11 |  | 1red 11262 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℝ) | 
| 12 |  | eluzelre 12889 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) | 
| 13 |  | rehalfcl 12492 | . . . . 5
⊢ (𝑁 ∈ ℝ → (𝑁 / 2) ∈
ℝ) | 
| 14 | 1, 2, 13 | 3syl 18 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ∈ ℝ) | 
| 15 |  | 2rp 13039 | . . . . . . 7
⊢ 2 ∈
ℝ+ | 
| 16 | 15 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℝ+) | 
| 17 |  | eluzle 12891 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) | 
| 18 |  | divge1 13103 | . . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁) → 1 ≤ (𝑁 / 2)) | 
| 19 | 16, 12, 17, 18 | syl3anc 1373 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ (𝑁 / 2)) | 
| 20 |  | eluzelcn 12890 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) | 
| 21 |  | subhalfhalf 12500 | . . . . . 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 11867 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 2) ≤ (𝑁 − 1)) | 
| 25 |  | 2t2e4 12430 | . . . . . . . . 9
⊢ (2
· 2) = 4 | 
| 26 | 25 | eqcomi 2746 | . . . . . . . 8
⊢ 4 = (2
· 2) | 
| 27 | 26 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 = (2 · 2)) | 
| 28 | 27 | oveq2d 7447 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = (𝑁 / (2 · 2))) | 
| 29 |  | 2cnne0 12476 | . . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 30 | 29 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 ∈ ℂ ∧ 2 ≠
0)) | 
| 31 |  | divdiv1 11978 | . . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) | 
| 32 | 20, 30, 30, 31 | syl3anc 1373 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) / 2) = (𝑁 / (2 · 2))) | 
| 33 | 28, 32 | eqtr4d 2780 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) = ((𝑁 / 2) / 2)) | 
| 34 | 33 | breq1d 5153 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) | 
| 35 |  | peano2rem 11576 | . . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) | 
| 36 | 12, 35 | syl 17 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℝ) | 
| 37 | 14, 36, 16 | lediv1d 13123 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 2) ≤ (𝑁 − 1) ↔ ((𝑁 / 2) / 2) ≤ ((𝑁 − 1) / 2))) | 
| 38 | 34, 37 | bitr4d 282 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 / 4) ≤ ((𝑁 − 1) / 2) ↔ (𝑁 / 2) ≤ (𝑁 − 1))) | 
| 39 | 24, 38 | mpbird 257 | . 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 / 4) ≤ ((𝑁 − 1) / 2)) | 
| 40 | 8 | flcld 13838 | . . . . 5
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℤ) | 
| 41 | 40 | zred 12722 | . . . 4
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℝ) | 
| 42 | 35 | rehalfcld 12513 | . . . 4
⊢ (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈
ℝ) | 
| 43 | 41, 8, 42 | 3jca 1129 | . . 3
⊢ (𝑁 ∈ ℝ →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ ((𝑁
− 1) / 2) ∈ ℝ)) | 
| 44 |  | letr 11355 | . . 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 699 | 1
⊢ (𝑁 ∈
(ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2)) |