Proof of Theorem dignn0flhalflem2
Step | Hyp | Ref
| Expression |
1 | | zre 11258 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
2 | 1 | rehalfcld 11156 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 / 2) ∈
ℝ) |
3 | 2 | flcld 12461 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ →
(⌊‘(𝐴 / 2))
∈ ℤ) |
4 | 3 | zred 11358 |
. . . . . 6
⊢ (𝐴 ∈ ℤ →
(⌊‘(𝐴 / 2))
∈ ℝ) |
5 | 4 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ∈ ℝ) |
6 | | 2re 10967 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
8 | | id 22 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
9 | 7, 8 | reexpcld 12887 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℝ) |
10 | 9 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℝ) |
11 | | 2cnd 10970 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℂ) |
12 | | 2ne0 10990 |
. . . . . . 7
⊢ 2 ≠
0 |
13 | 12 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ≠ 0) |
14 | | nn0z 11277 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
15 | 14 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℤ) |
16 | 11, 13, 15 | expne0d 12876 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ≠ 0) |
17 | 5, 10, 16 | redivcld 10732 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ∈ ℝ) |
18 | 17 | flcld 12461 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ) |
19 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝐴 ∈ ℝ) |
20 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℝ) |
21 | | simp3 1056 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
22 | | 1nn0 11185 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 1 ∈ ℕ0) |
24 | 21, 23 | nn0addcld 11232 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝑁 + 1) ∈
ℕ0) |
25 | 20, 24 | reexpcld 12887 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) ∈ ℝ) |
26 | 15 | peano2zd 11361 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝑁 + 1) ∈ ℤ) |
27 | 11, 13, 26 | expne0d 12876 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) ≠ 0) |
28 | 19, 25, 27 | redivcld 10732 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2↑(𝑁 + 1))) ∈ ℝ) |
29 | 28 | flcld 12461 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) ∈ ℤ) |
30 | | nn0p1nn 11209 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
31 | | dignn0flhalflem1 42207 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ (𝑁 + 1) ∈
ℕ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) <
(⌊‘((𝐴 −
1) / (2↑(𝑁 +
1))))) |
32 | 30, 31 | syl3an3 1353 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) <
(⌊‘((𝐴 −
1) / (2↑(𝑁 +
1))))) |
33 | | 1zzd 11285 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 1 ∈ ℤ) |
34 | | flsubz 42106 |
. . . . . 6
⊢ (((𝐴 / (2↑(𝑁 + 1))) ∈ ℝ ∧ 1 ∈
ℤ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1)) |
35 | 28, 33, 34 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1)) |
36 | 35 | eqcomd 2616 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) = (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1))) |
37 | | nnz 11276 |
. . . . . . . . . . 11
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ ((𝐴 − 1) / 2)
∈ ℤ) |
38 | | zob 14921 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (((𝐴 + 1) / 2) ∈ ℤ ↔
((𝐴 − 1) / 2) ∈
ℤ)) |
39 | 37, 38 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → (((𝐴 − 1) / 2) ∈ ℕ
→ ((𝐴 + 1) / 2) ∈
ℤ)) |
40 | 39 | imp 444 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ)
→ ((𝐴 + 1) / 2) ∈
ℤ) |
41 | | zofldiv2 42119 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 + 1) / 2) ∈ ℤ)
→ (⌊‘(𝐴 /
2)) = ((𝐴 − 1) /
2)) |
42 | 40, 41 | syldan 486 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ)
→ (⌊‘(𝐴 /
2)) = ((𝐴 − 1) /
2)) |
43 | 42 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) = ((𝐴 − 1) / 2)) |
44 | 43 | oveq1d 6564 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) = (((𝐴 − 1) / 2) / (2↑𝑁))) |
45 | 44 | fveq2d 6107 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁)))) |
46 | | zcn 11259 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
47 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 1 ∈
ℂ) |
48 | 46, 47 | subcld 10271 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℂ) |
49 | | 2rp 11713 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ 2 ∈ ℝ+) |
51 | 50 | rpcnne0d 11757 |
. . . . . . . 8
⊢ (((𝐴 − 1) / 2) ∈ ℕ
→ (2 ∈ ℂ ∧ 2 ≠ 0)) |
52 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ+) |
53 | 52, 14 | rpexpcld 12894 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℝ+) |
54 | 53 | rpcnne0d 11757 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((2↑𝑁) ∈
ℂ ∧ (2↑𝑁)
≠ 0)) |
55 | | divdiv1 10615 |
. . . . . . . 8
⊢ (((𝐴 − 1) ∈ ℂ ∧
(2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁)))) |
56 | 48, 51, 54, 55 | syl3an 1360 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁)))) |
57 | 10 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℂ) |
58 | 11, 57 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2)) |
59 | 11, 21 | expp1d 12871 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) |
60 | 58, 59 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1))) |
61 | 60 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 − 1) / (2 · (2↑𝑁))) = ((𝐴 − 1) / (2↑(𝑁 + 1)))) |
62 | 56, 61 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2↑(𝑁 + 1)))) |
63 | 62 | fveq2d 6107 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1))))) |
64 | 45, 63 | eqtrd 2644 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1))))) |
65 | 32, 36, 64 | 3brtr4d 4615 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) |
66 | 19 | rehalfcld 11156 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / 2) ∈ ℝ) |
67 | 66, 10, 16 | redivcld 10732 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) ∈ ℝ) |
68 | | reflcl 12459 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
(⌊‘(𝐴 / 2))
∈ ℝ) |
69 | 66, 68 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ∈ ℝ) |
70 | 49 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → 2 ∈ ℝ+) |
71 | 70, 15 | rpexpcld 12894 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈
ℝ+) |
72 | | flle 12462 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
(⌊‘(𝐴 / 2))
≤ (𝐴 /
2)) |
73 | 66, 72 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / 2)) ≤ (𝐴 / 2)) |
74 | 69, 66, 71, 73 | lediv1dd 11806 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ≤ ((𝐴 / 2) / (2↑𝑁))) |
75 | | flwordi 12475 |
. . . . 5
⊢
((((⌊‘(𝐴
/ 2)) / (2↑𝑁)) ∈
ℝ ∧ ((𝐴 / 2) /
(2↑𝑁)) ∈ ℝ
∧ ((⌊‘(𝐴 /
2)) / (2↑𝑁)) ≤
((𝐴 / 2) / (2↑𝑁))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁)))) |
76 | 17, 67, 74, 75 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁)))) |
77 | | divdiv1 10615 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁)))) |
78 | 46, 51, 54, 77 | syl3an 1360 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁)))) |
79 | 53 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (2↑𝑁) ∈
ℂ) |
80 | 79 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑𝑁) ∈ ℂ) |
81 | 11, 80 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2)) |
82 | 11, 13, 15 | expp1zd 12879 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) |
83 | 81, 82 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1))) |
84 | 83 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2 · (2↑𝑁))) = (𝐴 / (2↑(𝑁 + 1)))) |
85 | 78, 84 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2↑(𝑁 + 1)))) |
86 | 85 | eqcomd 2616 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (𝐴 / (2↑(𝑁 + 1))) = ((𝐴 / 2) / (2↑𝑁))) |
87 | 86 | fveq2d 6107 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((𝐴 / 2) / (2↑𝑁)))) |
88 | 76, 87 | breqtrrd 4611 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1))))) |
89 | | zgtp1leeq 42105 |
. . . 4
⊢
(((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧
(⌊‘(𝐴 /
(2↑(𝑁 + 1)))) ∈
ℤ) → ((((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1))))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1)))))) |
90 | 89 | imp 444 |
. . 3
⊢
((((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧
(⌊‘(𝐴 /
(2↑(𝑁 + 1)))) ∈
ℤ) ∧ (((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) <
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1)))))) →
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1))))) |
91 | 18, 29, 65, 88, 90 | syl22anc 1319 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1))))) |
92 | 91 | eqcomd 2616 |
1
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ
∧ 𝑁 ∈
ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) =
(⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) |