Step | Hyp | Ref
| Expression |
1 | | elnn1uz2 11641 |
. . 3
⊢ (𝑎 ∈ ℕ ↔ (𝑎 = 1 ∨ 𝑎 ∈
(ℤ≥‘2))) |
2 | | 1t1e1 11052 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
3 | 2 | eqcomi 2619 |
. . . . . . . 8
⊢ 1 = (1
· 1) |
4 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) → 𝑎 = 1) |
5 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ ((𝑦 + 1) =
(#b‘𝑎)
→ (0..^(𝑦 + 1)) =
(0..^(#b‘𝑎))) |
6 | 5 | eqcoms 2618 |
. . . . . . . . . . 11
⊢
((#b‘𝑎) = (𝑦 + 1) → (0..^(𝑦 + 1)) = (0..^(#b‘𝑎))) |
7 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 1 →
(#b‘𝑎) =
(#b‘1)) |
8 | | blen1 42176 |
. . . . . . . . . . . . . 14
⊢
(#b‘1) = 1 |
9 | 7, 8 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 →
(#b‘𝑎) =
1) |
10 | 9 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 →
(0..^(#b‘𝑎)) = (0..^1)) |
11 | | fzo01 12417 |
. . . . . . . . . . . 12
⊢ (0..^1) =
{0} |
12 | 10, 11 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 →
(0..^(#b‘𝑎)) = {0}) |
13 | 6, 12 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) → (0..^(𝑦 + 1)) = {0}) |
14 | 13 | sumeq1d 14279 |
. . . . . . . . 9
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) →
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
15 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 1 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)1)) |
16 | 15 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑎 = 1 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)1) · (2↑𝑘))) |
17 | 16 | sumeq2sdv 14282 |
. . . . . . . . . . 11
⊢ (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘))) |
18 | | c0ex 9913 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
19 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
20 | 19, 19 | mulcli 9924 |
. . . . . . . . . . . 12
⊢ (1
· 1) ∈ ℂ |
21 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (𝑘(digit‘2)1) =
(0(digit‘2)1)) |
22 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
23 | 22 | prid2 4242 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
{0, 1} |
24 | | 0dig2pr01 42202 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
{0, 1} → (0(digit‘2)1) = 1) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(0(digit‘2)1) = 1 |
26 | 21, 25 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → (𝑘(digit‘2)1) = 1) |
27 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
28 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
29 | | exp0 12726 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℂ → (2↑0) = 1) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(2↑0) = 1 |
31 | 27, 30 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → (2↑𝑘) = 1) |
32 | 26, 31 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 ·
1)) |
33 | 32 | sumsn 14319 |
. . . . . . . . . . . 12
⊢ ((0
∈ V ∧ (1 · 1) ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)1) · (2↑𝑘)) = (1 ·
1)) |
34 | 18, 20, 33 | mp2an 704 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈ {0}
((𝑘(digit‘2)1)
· (2↑𝑘)) = (1
· 1) |
35 | 17, 34 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1)) |
36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) →
Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 ·
1)) |
37 | 14, 36 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) →
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 · 1)) |
38 | 3, 4, 37 | 3eqtr4a 2670 |
. . . . . . 7
⊢ ((𝑎 = 1 ∧
(#b‘𝑎) =
(𝑦 + 1)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
39 | 38 | ex 449 |
. . . . . 6
⊢ (𝑎 = 1 →
((#b‘𝑎) =
(𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
40 | 39 | a1d 25 |
. . . . 5
⊢ (𝑎 = 1 → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
41 | 40 | 2a1d 26 |
. . . 4
⊢ (𝑎 = 1 → (((𝑎 − 1) / 2) ∈
ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
42 | | eluzge2nn0 11603 |
. . . . . . . . 9
⊢ (𝑎 ∈
(ℤ≥‘2) → 𝑎 ∈ ℕ0) |
43 | | nn0ob 14938 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ0
→ (((𝑎 + 1) / 2)
∈ ℕ0 ↔ ((𝑎 − 1) / 2) ∈
ℕ0)) |
44 | 43 | bicomd 212 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ0
→ (((𝑎 − 1) / 2)
∈ ℕ0 ↔ ((𝑎 + 1) / 2) ∈
ℕ0)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 − 1) / 2) ∈ ℕ0
↔ ((𝑎 + 1) / 2) ∈
ℕ0)) |
46 | | blennngt2o2 42184 |
. . . . . . . . 9
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 + 1) / 2) ∈ ℕ0) →
(#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1)) |
47 | 46 | ex 449 |
. . . . . . . 8
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 →
(#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1))) |
48 | 45, 47 | sylbid 229 |
. . . . . . 7
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 − 1) / 2) ∈ ℕ0
→ (#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) +
1))) |
49 | 48 | imp 444 |
. . . . . 6
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ (#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) +
1)) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝑎 − 1) / 2) →
(#b‘𝑥) =
(#b‘((𝑎
− 1) / 2))) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑎 − 1) / 2) →
((#b‘𝑥) =
𝑦 ↔
(#b‘((𝑎
− 1) / 2)) = 𝑦)) |
52 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝑎 − 1) / 2) → 𝑥 = ((𝑎 − 1) / 2)) |
53 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ((𝑎 − 1) / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)((𝑎 − 1) / 2))) |
54 | 53 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝑎 − 1) / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) |
55 | 54 | sumeq2sdv 14282 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝑎 − 1) / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) |
56 | 52, 55 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑎 − 1) / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))) |
57 | 51, 56 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑎 − 1) / 2) →
(((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))))) |
58 | 57 | rspcva 3280 |
. . . . . . . . . . 11
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)))) |
59 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢
((#b‘𝑎) = (𝑦 + 1) → ((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) ↔ (𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) +
1))) |
60 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
61 | 60 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℂ) |
62 | | blennn0elnn 42169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈
ℕ) |
63 | 62 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → (#b‘((𝑎 − 1) / 2)) ∈
ℂ) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (#b‘((𝑎 − 1) / 2)) ∈
ℂ) |
65 | 64 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
(#b‘((𝑎
− 1) / 2)) ∈ ℂ) |
66 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈
ℂ) |
67 | 61, 65, 66 | addcan2d 10119 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) ↔
𝑦 =
(#b‘((𝑎
− 1) / 2)))) |
68 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (#b‘((𝑎 − 1) / 2)) ↔
(#b‘((𝑎
− 1) / 2)) = 𝑦) |
69 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
70 | 69 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈ ℤ) |
71 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ →
(0...𝑦) = (0..^(𝑦 + 1))) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (0...𝑦) = (0..^(𝑦 + 1))) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (0..^(𝑦 + 1)) = (0...𝑦)) |
74 | 73 | sumeq1d 14279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
75 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
76 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈
(ℤ≥‘0)) |
77 | 75, 76 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘0)) |
78 | 77 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈
(ℤ≥‘0)) |
79 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
ℕ |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑘 ∈ (0...𝑦)) → 2 ∈
ℕ) |
81 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ) |
83 | | nn0rp0 12150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
(0[,)+∞)) |
84 | 42, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 ∈
(ℤ≥‘2) → 𝑎 ∈ (0[,)+∞)) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → 𝑎 ∈ (0[,)+∞)) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
87 | | digvalnn0 42191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 𝑎
∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
88 | 80, 82, 86, 87 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
89 | 88 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈
ℕ0)) |
90 | 89 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ (0...𝑦) → (𝑘(digit‘2)𝑎) ∈
ℕ0)) |
91 | 90 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
92 | 91 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
93 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ∈
ℕ0 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ (0...𝑦) → 2 ∈
ℕ0) |
95 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0) |
96 | 94, 95 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈
ℕ0) |
97 | 96 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ) |
98 | 97 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ) |
99 | 92, 98 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
100 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎)) |
101 | 100, 27 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0))) |
102 | 30 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0(digit‘2)𝑎)
· (2↑0)) = ((0(digit‘2)𝑎) · 1) |
103 | 101, 102 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
104 | 78, 99, 103 | fsum1p 14326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
105 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → 𝑎 ∈ ℕ0) |
106 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 + 1) / 2) ∈ ℕ0 ↔
((𝑎 − 1) / 2) ∈
ℕ0)) |
107 | 106 | biimparc 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → ((𝑎 + 1) / 2) ∈
ℕ0) |
108 | | 0dig2nn0o 42205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑎 ∈ ℕ0
∧ ((𝑎 + 1) / 2) ∈
ℕ0) → (0(digit‘2)𝑎) = 1) |
109 | 105, 107,
108 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (0(digit‘2)𝑎) = 1) |
110 | 109 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
(0(digit‘2)𝑎) =
1) |
111 | 110 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
((0(digit‘2)𝑎)
· 1) = (1 · 1)) |
112 | 111, 2 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
((0(digit‘2)𝑎)
· 1) = 1) |
113 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℤ |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 1 ∈
ℤ) |
115 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (0 + 1) =
1 |
116 | 115, 113 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (0 + 1)
∈ ℤ |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (0 + 1) ∈
ℤ) |
118 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ) |
119 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ) |
120 | 119 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ) |
121 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ ℕ0) |
122 | 121, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
123 | 118, 120,
122, 87 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
124 | 123 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 ∈
(ℤ≥‘2) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈
ℕ0)) |
125 | 124 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈
ℕ0)) |
126 | 125 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑘 ∈ ((0 + 1)...𝑦) → (𝑘(digit‘2)𝑎) ∈
ℕ0)) |
127 | 126 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
128 | 127 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
129 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈
ℂ) |
130 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ) |
131 | 130 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0) |
132 | 115 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((0 +
1)...𝑦) = (1...𝑦) |
133 | 131, 132 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0) |
134 | 129, 133 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈
ℂ) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ) |
136 | 128, 135 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
137 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎)) |
138 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1))) |
139 | 137, 138 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
140 | 114, 117,
70, 136, 139 | fsumshftm 14355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
141 | 112, 140 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
(((0(digit‘2)𝑎)
· 1) + Σ𝑘
∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (1 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
142 | 74, 104, 141 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
143 | 142 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (1 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
144 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈
ℕ) |
145 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ) |
147 | | nn0rp0 12150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → ((𝑎 − 1) / 2) ∈
(0[,)+∞)) |
148 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → ((𝑎 − 1) / 2) ∈
(0[,)+∞)) |
149 | 148 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → ((𝑎 − 1) / 2) ∈
(0[,)+∞)) |
150 | | digvalnn0 42191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((2
∈ ℕ ∧ 𝑖
∈ ℤ ∧ ((𝑎
− 1) / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℕ0) |
151 | 144, 146,
149, 150 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℕ0) |
152 | 151 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℂ) |
153 | 152 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℂ)) |
154 | 153 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑖 ∈ (0..^𝑦) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℂ)) |
155 | 154 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)((𝑎 − 1) / 2)) ∈
ℂ) |
156 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈
ℕ0) |
157 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0) |
158 | 156, 157 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈
ℕ0) |
159 | 158 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ) |
160 | 159 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ) |
161 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ) |
162 | 155, 160,
161 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) ·
((2↑𝑖) ·
2))) |
163 | 162 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)((𝑎 − 1) / 2)) ·
(2↑𝑖)) ·
2)) |
164 | 163 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2)) |
165 | 164 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2)) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2)) |
166 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 ∈
ℂ |
167 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (0 ∈
ℂ → ((0 + 1) − 1) = 0) |
168 | 166, 167 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((0 + 1)
− 1) = 0 |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℕ → ((0 + 1)
− 1) = 0) |
170 | 169 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0...(𝑦 −
1))) |
171 | | fzoval 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℤ →
(0..^𝑦) = (0...(𝑦 − 1))) |
172 | 69, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℕ →
(0..^𝑦) = (0...(𝑦 − 1))) |
173 | 170, 172 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0..^𝑦)) |
174 | 173 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (((0 + 1) −
1)...(𝑦 − 1)) =
(0..^𝑦)) |
175 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 ∈
(ℤ≥‘2)) |
176 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ (0...(𝑦 − 1)) → 𝑖 ∈ ℕ0) |
177 | 168 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((0 + 1)
− 1)...(𝑦 − 1))
= (0...(𝑦 −
1)) |
178 | 176, 177 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1)) →
𝑖 ∈
ℕ0) |
179 | | dignn0flhalf 42210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2)))) |
180 | 175, 178,
179 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(⌊‘(𝑎 / 2)))) |
181 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑎 ∈
(ℤ≥‘2) → 𝑎 ∈ ℤ) |
182 | 181 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ 𝑎 ∈
ℤ) |
183 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → ((𝑎 − 1) / 2) ∈
ℤ) |
184 | | zob 14921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∈ ℤ → (((𝑎 + 1) / 2) ∈ ℤ ↔
((𝑎 − 1) / 2) ∈
ℤ)) |
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 + 1) / 2) ∈ ℤ ↔ ((𝑎 − 1) / 2) ∈
ℤ)) |
186 | 183, 185 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 − 1) / 2) ∈ ℕ0
→ ((𝑎 + 1) / 2) ∈
ℤ)) |
187 | 186 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ ((𝑎 + 1) / 2) ∈
ℤ) |
188 | 182, 187 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ (𝑎 ∈ ℤ
∧ ((𝑎 + 1) / 2) ∈
ℤ)) |
189 | 188 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ)) |
190 | 189 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ)) |
191 | 190 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈
ℤ)) |
192 | | zofldiv2 42119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑎 ∈ ℤ ∧ ((𝑎 + 1) / 2) ∈ ℤ)
→ (⌊‘(𝑎 /
2)) = ((𝑎 − 1) /
2)) |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) →
(⌊‘(𝑎 / 2)) =
((𝑎 − 1) /
2)) |
194 | 193 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (𝑖(digit‘2)(⌊‘(𝑎 / 2))) = (𝑖(digit‘2)((𝑎 − 1) / 2))) |
195 | 180, 194 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)((𝑎 − 1) / 2))) |
196 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1)) →
2 ∈ ℂ) |
197 | 196, 178 | expp1d 12871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1)) →
(2↑(𝑖 + 1)) =
((2↑𝑖) ·
2)) |
198 | 197 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) →
(2↑(𝑖 + 1)) =
((2↑𝑖) ·
2)) |
199 | 195, 198 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) ∧ 𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2))) |
200 | 174, 199 | sumeq12dv 14284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2))) |
201 | 200 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · ((2↑𝑖) · 2))) |
202 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 𝑖 → (𝑘(digit‘2)((𝑎 − 1) / 2)) = (𝑖(digit‘2)((𝑎 − 1) / 2))) |
203 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖)) |
204 | 202, 203 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 𝑖 → ((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))) |
205 | 204 | cbvsumv 14274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
Σ𝑘 ∈
(0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) |
206 | 205 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ↔ ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))) |
207 | 206 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))) |
208 | 207 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → ((𝑎 − 1) / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖))) |
209 | 208 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (((𝑎 − 1) / 2) · 2) =
(Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2)) |
210 | | fzofi 12635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(0..^𝑦) ∈
Fin |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (0..^𝑦) ∈ Fin) |
212 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → 2 ∈
ℂ) |
213 | 159 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈
ℂ) |
214 | 152, 213 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈
ℂ) |
215 | 214 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈
ℂ)) |
216 | 215 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑦 ∈ ℕ)
→ (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈
ℂ)) |
217 | 216 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (𝑖 ∈ (0..^𝑦) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈
ℂ)) |
218 | 217 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑎 − 1) /
2) = Σ𝑘 ∈
(0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) ∈
ℂ) |
219 | 211, 212,
218 | fsummulc1 14359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2)) |
220 | 209, 219 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (((𝑎 − 1) / 2) · 2) =
Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑖)) · 2)) |
221 | 165, 201,
220 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑎 − 1) / 2) ·
2)) |
222 | 221 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (1 + (((𝑎 − 1) / 2) ·
2))) |
223 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ∈
(ℤ≥‘2) → 𝑎 ∈ ℂ) |
224 | | peano2cnm 10226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ∈ ℂ → (𝑎 − 1) ∈
ℂ) |
225 | 223, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 ∈
(ℤ≥‘2) → (𝑎 − 1) ∈ ℂ) |
226 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
227 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 2 ≠
0 |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 ∈
(ℤ≥‘2) → 2 ≠ 0) |
229 | 225, 226,
228 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 ∈
(ℤ≥‘2) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0)) |
230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → ((𝑎 − 1) ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0)) |
231 | | divcan1 10573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 − 1) ∈ ℂ ∧
2 ∈ ℂ ∧ 2 ≠ 0) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1)) |
232 | 230, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (((𝑎 − 1) / 2) · 2) = (𝑎 − 1)) |
233 | 232 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = (1 + (𝑎 − 1))) |
234 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
235 | 234, 223 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 ∈
(ℤ≥‘2) → (1 ∈ ℂ ∧ 𝑎 ∈
ℂ)) |
236 | 235 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (1 ∈ ℂ ∧ 𝑎 ∈
ℂ)) |
237 | | pncan3 10168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℂ ∧ 𝑎
∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎) |
238 | 236, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (1 + (𝑎 − 1)) = 𝑎) |
239 | 233, 238 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) → (1 + (((𝑎 − 1) / 2) · 2)) = 𝑎) |
240 | 239 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑎 − 1) /
2) ∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑦 ∈ ℕ)
→ (1 + (((𝑎 − 1)
/ 2) · 2)) = 𝑎) |
241 | 240 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → (1 + (((𝑎 − 1) / 2) · 2)) =
𝑎) |
242 | 143, 222,
241 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) ∧
((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
243 | 242 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘)) →
(((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
244 | 243 | imim2i 16 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) →
((#b‘((𝑎
− 1) / 2)) = 𝑦 →
(((#b‘𝑎) =
(𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
245 | 244 | com13 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) →
((#b‘((𝑎
− 1) / 2)) = 𝑦 →
(((#b‘((𝑎
− 1) / 2)) = 𝑦 →
((𝑎 − 1) / 2) =
Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
246 | 68, 245 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → (𝑦 = (#b‘((𝑎 − 1) / 2)) →
(((#b‘((𝑎
− 1) / 2)) = 𝑦 →
((𝑎 − 1) / 2) =
Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
247 | 67, 246 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#b‘𝑎) = (𝑦 + 1) ∧ ((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ)) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(((#b‘((𝑎
− 1) / 2)) = 𝑦 →
((𝑎 − 1) / 2) =
Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
248 | 247 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
((#b‘𝑎) = (𝑦 + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(((#b‘((𝑎
− 1) / 2)) = 𝑦 →
((𝑎 − 1) / 2) =
Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
249 | 248 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢
((#b‘𝑎) = (𝑦 + 1) → ((𝑦 + 1) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(((((𝑎 − 1) / 2)
∈ ℕ0 ∧ 𝑎 ∈ (ℤ≥‘2))
∧ 𝑦 ∈ ℕ)
→ (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
250 | 59, 249 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢
((#b‘𝑎) = (𝑦 + 1) → ((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ) →
(((#b‘((𝑎
− 1) / 2)) = 𝑦 →
((𝑎 − 1) / 2) =
Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
251 | 250 | com23 84 |
. . . . . . . . . . . . . 14
⊢
((#b‘𝑎) = (𝑦 + 1) → (((((𝑎 − 1) / 2) ∈ ℕ0
∧ 𝑎 ∈
(ℤ≥‘2)) ∧ 𝑦 ∈ ℕ) →
((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) → (((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
252 | 251 | com14 94 |
. . . . . . . . . . . . 13
⊢
(((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((((𝑎 − 1) / 2) ∈
ℕ0 ∧ 𝑎
∈ (ℤ≥‘2)) ∧ 𝑦 ∈ ℕ) →
((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
253 | 252 | exp4c 634 |
. . . . . . . . . . . 12
⊢
(((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0
→ (𝑎 ∈
(ℤ≥‘2) → (𝑦 ∈ ℕ →
((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
254 | 253 | com35 96 |
. . . . . . . . . . 11
⊢
(((#b‘((𝑎 − 1) / 2)) = 𝑦 → ((𝑎 − 1) / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)((𝑎 − 1) / 2)) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0
→ ((#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(𝑦 ∈ ℕ →
(𝑎 ∈
(ℤ≥‘2) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
255 | 58, 254 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑎 − 1) / 2) ∈
ℕ0 ∧ ∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → (((𝑎 − 1) / 2) ∈ ℕ0
→ ((#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(𝑦 ∈ ℕ →
(𝑎 ∈
(ℤ≥‘2) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
256 | 255 | ex 449 |
. . . . . . . . 9
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → (((𝑎 − 1) / 2) ∈ ℕ0
→ ((#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(𝑦 ∈ ℕ →
(𝑎 ∈
(ℤ≥‘2) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))) |
257 | 256 | pm2.43a 52 |
. . . . . . . 8
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) =
((#b‘((𝑎
− 1) / 2)) + 1) → (𝑦 ∈ ℕ → (𝑎 ∈ (ℤ≥‘2)
→ ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
258 | 257 | com25 97 |
. . . . . . 7
⊢ (((𝑎 − 1) / 2) ∈
ℕ0 → (𝑎 ∈ (ℤ≥‘2)
→ ((#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
259 | 258 | impcom 445 |
. . . . . 6
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ ((#b‘𝑎) = ((#b‘((𝑎 − 1) / 2)) + 1) →
(𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
260 | 49, 259 | mpd 15 |
. . . . 5
⊢ ((𝑎 ∈
(ℤ≥‘2) ∧ ((𝑎 − 1) / 2) ∈ ℕ0)
→ (𝑦 ∈ ℕ
→ (∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
261 | 260 | ex 449 |
. . . 4
⊢ (𝑎 ∈
(ℤ≥‘2) → (((𝑎 − 1) / 2) ∈ ℕ0
→ (𝑦 ∈ ℕ
→ (∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
262 | 41, 261 | jaoi 393 |
. . 3
⊢ ((𝑎 = 1 ∨ 𝑎 ∈ (ℤ≥‘2))
→ (((𝑎 − 1) / 2)
∈ ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
263 | 1, 262 | sylbi 206 |
. 2
⊢ (𝑎 ∈ ℕ → (((𝑎 − 1) / 2) ∈
ℕ0 → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
264 | 263 | imp31 447 |
1
⊢ (((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈
ℕ0) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |