Proof of Theorem dignn0flhalflem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zre 12617 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) | 
| 2 | 1 | rehalfcld 12513 | . . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 / 2) ∈
ℝ) | 
| 3 | 2 | flcld 13838 | . . . . . . 7
⊢ (𝐴 ∈ ℤ →
(⌊‘(𝐴 / 2))
∈ ℤ) | 
| 4 | 3 | zred 12722 | . . . . . 6
⊢ (𝐴 ∈ ℤ →
(⌊‘(𝐴 / 2))
∈ ℝ) | 
| 5 | 4 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ∈ ℝ) | 
| 6 |  | 2re 12340 | . . . . . . . 8
⊢ 2 ∈
ℝ | 
| 7 | 6 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) | 
| 8 |  | id 22 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) | 
| 9 | 7, 8 | reexpcld 14203 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℝ) | 
| 10 | 9 | 3ad2ant3 1136 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℝ) | 
| 11 |  | 2cnd 12344 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℂ) | 
| 12 |  | 2ne0 12370 | . . . . . . 7
⊢ 2 ≠
0 | 
| 13 | 12 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ≠ 0) | 
| 14 |  | nn0z 12638 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 15 | 14 | 3ad2ant3 1136 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℤ) | 
| 16 | 11, 13, 15 | expne0d 14192 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ≠ 0) | 
| 17 | 5, 10, 16 | redivcld 12095 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ∈ ℝ) | 
| 18 | 17 | flcld 13838 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ) | 
| 19 | 1 | 3ad2ant1 1134 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝐴 ∈ ℝ) | 
| 20 | 6 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℝ) | 
| 21 |  | simp3 1139 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) | 
| 22 |  | 1nn0 12542 | . . . . . . . 8
⊢ 1 ∈
ℕ0 | 
| 23 | 22 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 1 ∈ ℕ0) | 
| 24 | 21, 23 | nn0addcld 12591 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝑁 + 1) ∈
ℕ0) | 
| 25 | 20, 24 | reexpcld 14203 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) ∈ ℝ) | 
| 26 | 15 | peano2zd 12725 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝑁 + 1) ∈ ℤ) | 
| 27 | 11, 13, 26 | expne0d 14192 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) ≠ 0) | 
| 28 | 19, 25, 27 | redivcld 12095 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2↑(𝑁 + 1))) ∈ ℝ) | 
| 29 | 28 | flcld 13838 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) ∈ ℤ) | 
| 30 |  | nn0p1nn 12565 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) | 
| 31 |  | dignn0flhalflem1 48536 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ (𝑁 + 1) ∈
ℕ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) <
(⌊‘((𝐴 −
1) / (2↑(𝑁 +
1))))) | 
| 32 | 30, 31 | syl3an3 1166 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) <
(⌊‘((𝐴 −
1) / (2↑(𝑁 +
1))))) | 
| 33 |  | 1zzd 12648 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 1 ∈ ℤ) | 
| 34 |  | flsubz 48439 | . . . . . 6
⊢ (((𝐴 / (2↑(𝑁 + 1))) ∈ ℝ ∧ 1 ∈
ℤ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1)) | 
| 35 | 28, 33, 34 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1)) | 
| 36 | 35 | eqcomd 2743 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) = (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1))) | 
| 37 |  | nnz 12634 | . . . . . . . . . 10
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ ((𝐴 − 1) / 2)
∈ ℤ) | 
| 38 |  | zob 16396 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → (((𝐴 + 1) / 2) ∈ ℤ ↔
((𝐴 − 1) / 2) ∈
ℤ)) | 
| 39 | 37, 38 | imbitrrid 246 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (((𝐴 − 1) / 2) ∈ ℕ
→ ((𝐴 + 1) / 2) ∈
ℤ)) | 
| 40 | 39 | imp 406 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ)
→ ((𝐴 + 1) / 2) ∈
ℤ) | 
| 41 |  | zofldiv2 48452 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 + 1) / 2) ∈ ℤ)
→ (⌊‘(𝐴 /
2)) = ((𝐴 − 1) /
2)) | 
| 42 | 40, 41 | syldan 591 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ)
→ (⌊‘(𝐴 /
2)) = ((𝐴 − 1) /
2)) | 
| 43 | 42 | 3adant3 1133 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) = ((𝐴 − 1) / 2)) | 
| 44 | 43 | fvoveq1d 7453 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁)))) | 
| 45 |  | zcn 12618 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) | 
| 46 |  | 1cnd 11256 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 1 ∈
ℂ) | 
| 47 | 45, 46 | subcld 11620 | . . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℂ) | 
| 48 |  | 2rp 13039 | . . . . . . . . . 10
⊢ 2 ∈
ℝ+ | 
| 49 | 48 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ 2 ∈ ℝ+) | 
| 50 | 49 | rpcnne0d 13086 | . . . . . . . 8
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ (2 ∈ ℂ ∧ 2 ≠ 0)) | 
| 51 | 48 | a1i 11 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ+) | 
| 52 | 51, 14 | rpexpcld 14286 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℝ+) | 
| 53 | 52 | rpcnne0d 13086 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((2↑𝑁) ∈
ℂ ∧ (2↑𝑁)
≠ 0)) | 
| 54 |  | divdiv1 11978 | . . . . . . . 8
⊢ (((𝐴 − 1) ∈ ℂ ∧
(2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁)))) | 
| 55 | 47, 50, 53, 54 | syl3an 1161 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁)))) | 
| 56 | 10 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℂ) | 
| 57 | 11, 56 | mulcomd 11282 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2)) | 
| 58 | 11, 21 | expp1d 14187 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) | 
| 59 | 57, 58 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1))) | 
| 60 | 59 | oveq2d 7447 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 − 1) / (2 · (2↑𝑁))) = ((𝐴 − 1) / (2↑(𝑁 + 1)))) | 
| 61 | 55, 60 | eqtrd 2777 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2↑(𝑁 + 1)))) | 
| 62 | 61 | fveq2d 6910 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1))))) | 
| 63 | 44, 62 | eqtrd 2777 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1))))) | 
| 64 | 32, 36, 63 | 3brtr4d 5175 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) | 
| 65 | 19 | rehalfcld 12513 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / 2) ∈ ℝ) | 
| 66 | 65, 10, 16 | redivcld 12095 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) ∈ ℝ) | 
| 67 |  | reflcl 13836 | . . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
(⌊‘(𝐴 / 2))
∈ ℝ) | 
| 68 | 65, 67 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ∈ ℝ) | 
| 69 | 48 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℝ+) | 
| 70 | 69, 15 | rpexpcld 14286 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈
ℝ+) | 
| 71 |  | flle 13839 | . . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
(⌊‘(𝐴 / 2))
≤ (𝐴 /
2)) | 
| 72 | 65, 71 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ≤ (𝐴 / 2)) | 
| 73 | 68, 65, 70, 72 | lediv1dd 13135 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ≤ ((𝐴 / 2) / (2↑𝑁))) | 
| 74 |  | flwordi 13852 | . . . . 5
⊢
((((⌊‘(𝐴
/ 2)) / (2↑𝑁)) ∈
ℝ ∧ ((𝐴 / 2) /
(2↑𝑁)) ∈ ℝ
∧ ((⌊‘(𝐴 /
2)) / (2↑𝑁)) ≤
((𝐴 / 2) / (2↑𝑁))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁)))) | 
| 75 | 17, 66, 73, 74 | syl3anc 1373 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁)))) | 
| 76 |  | divdiv1 11978 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁)))) | 
| 77 | 45, 50, 53, 76 | syl3an 1161 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁)))) | 
| 78 | 52 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℂ) | 
| 79 | 78 | 3ad2ant3 1136 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℂ) | 
| 80 | 11, 79 | mulcomd 11282 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2)) | 
| 81 | 11, 13, 15 | expp1zd 14195 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) | 
| 82 | 80, 81 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1))) | 
| 83 | 82 | oveq2d 7447 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2 · (2↑𝑁))) = (𝐴 / (2↑(𝑁 + 1)))) | 
| 84 | 77, 83 | eqtrd 2777 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2↑(𝑁 + 1)))) | 
| 85 | 84 | eqcomd 2743 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2↑(𝑁 + 1))) = ((𝐴 / 2) / (2↑𝑁))) | 
| 86 | 85 | fveq2d 6910 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((𝐴 / 2) / (2↑𝑁)))) | 
| 87 | 75, 86 | breqtrrd 5171 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1))))) | 
| 88 |  | zgtp1leeq 48438 | . . . 4
⊢
(((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧
(⌊‘(𝐴 /
(2↑(𝑁 + 1)))) ∈
ℤ) → ((((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1))))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1)))))) | 
| 89 | 88 | imp 406 | . . 3
⊢
((((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧
(⌊‘(𝐴 /
(2↑(𝑁 + 1)))) ∈
ℤ) ∧ (((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1)))))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1))))) | 
| 90 | 18, 29, 64, 87, 89 | syl22anc 839 | . 2
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1))))) | 
| 91 | 90 | eqcomd 2743 | 1
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) =
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) |