Step | Hyp | Ref
| Expression |
1 | | nnnn0 12249 |
. . . 4
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 / 2) ∈
ℕ0) |
2 | | blennn0em1 45948 |
. . . 4
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈
ℕ0) → (#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1)) |
3 | 1, 2 | sylan2 593 |
. . 3
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
(#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1)) |
4 | | fveqeq2 6792 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 / 2) → ((#b‘𝑥) = 𝑦 ↔ (#b‘(𝑎 / 2)) = 𝑦)) |
5 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 / 2) → 𝑥 = (𝑎 / 2)) |
6 | | oveq2 7292 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)(𝑎 / 2))) |
7 | 6 | oveq1d 7299 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑎 / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
8 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑎 / 2) ∧ 𝑘 ∈ (0..^𝑦)) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
9 | 8 | sumeq2dv 15424 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
10 | 5, 9 | eqeq12d 2755 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))) |
11 | 4, 10 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑎 / 2) → (((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))) |
12 | 11 | rspcva 3560 |
. . . . . . . . 9
⊢ (((𝑎 / 2) ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))) |
13 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
(#b‘𝑎) =
(𝑦 + 1)) |
14 | 13 | oveq1d 7299 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
((#b‘𝑎)
− 1) = ((𝑦 + 1)
− 1)) |
15 | | nncn 11990 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
16 | | pncan1 11408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦) |
18 | 14, 17 | sylan9eq 2799 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘𝑎)
− 1) = 𝑦) |
19 | 18 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) ↔
(#b‘(𝑎 /
2)) = 𝑦)) |
20 | | nnz 12351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ) |
22 | | fzval3 13465 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℤ →
(0...𝑦) = (0..^(𝑦 + 1))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0...𝑦) = (0..^(𝑦 + 1))) |
24 | 23 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^(𝑦 + 1)) = (0...𝑦)) |
25 | 24 | sumeq1d 15422 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
26 | | nnnn0 12249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
27 | | elnn0uz 12632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈
(ℤ≥‘0)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘0)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
(ℤ≥‘0)) |
30 | | 2nn 12055 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ) |
32 | | elfzelz 13265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ) |
34 | | nnnn0 12249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ0) |
35 | | nn0rp0 13196 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
(0[,)+∞)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
(0[,)+∞)) |
37 | 36 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
38 | | digvalnn0 45956 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 𝑎
∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
39 | 31, 33, 37, 38 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
40 | 39 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
41 | | 2nn0 12259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ0 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 2 ∈
ℕ0) |
43 | | elfznn0 13358 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0) |
44 | 42, 43 | nn0expcld 13970 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈
ℕ0) |
45 | 44 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ) |
47 | 40, 46 | mulcld 11004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
48 | | oveq1 7291 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎)) |
49 | | oveq2 7292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
50 | 48, 49 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0))) |
51 | | 2cn 12057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℂ |
52 | | exp0 13795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 ∈
ℂ → (2↑0) = 1) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑0) = 1 |
54 | 53 | oveq2i 7295 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0(digit‘2)𝑎)
· (2↑0)) = ((0(digit‘2)𝑎) · 1) |
55 | 50, 54 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
56 | 29, 47, 55 | fsum1p 15474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
57 | | 0dig2nn0e 45969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ ℕ0
∧ (𝑎 / 2) ∈
ℕ0) → (0(digit‘2)𝑎) = 0) |
58 | 34, 1, 57 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
(0(digit‘2)𝑎) =
0) |
59 | 58 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = (0 · 1)) |
60 | | 1re 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℝ |
61 | | mul02lem2 11161 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℝ → (0 · 1) = 0) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0
· 1) = 0 |
63 | 59, 62 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = 0) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
((0(digit‘2)𝑎)
· 1) = 0) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = 0) |
66 | | 1z 12359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℤ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℤ) |
68 | | 0p1e1 12104 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
69 | 68, 66 | eqeltri 2836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 + 1)
∈ ℤ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + 1) ∈
ℤ) |
71 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ) |
72 | | elfzelz 13265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ) |
74 | 36 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
75 | 71, 73, 74, 38 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
76 | 75 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
77 | | 2cnd 12060 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈
ℂ) |
78 | | elfznn 13294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ) |
79 | 78 | nnnn0d 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0) |
80 | 68 | oveq1i 7294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0 +
1)...𝑦) = (1...𝑦) |
81 | 79, 80 | eleq2s 2858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0) |
82 | 77, 81 | expcld 13873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈
ℂ) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ) |
84 | 76, 83 | mulcld 11004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
85 | | oveq1 7291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎)) |
86 | | oveq2 7292 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1))) |
87 | 85, 86 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
88 | 67, 70, 21, 84, 87 | fsumshftm 15502 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
89 | 65, 88 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((0(digit‘2)𝑎)
· 1) + Σ𝑘
∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
90 | 1 | ad4antr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈
ℕ0) |
91 | 34 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ ℕ0) |
92 | | elfzonn0 13441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℕ0) |
94 | | dignn0ehalf 45974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 / 2) ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑖
∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2))) |
95 | 90, 91, 93, 94 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2))) |
96 | | 2cnd 12060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℂ) |
97 | 96, 92 | expp1d 13874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2)) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2)) |
99 | 95, 98 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2))) |
100 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℕ) |
101 | | elfzoelz 13396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ) |
103 | | nn0rp0 13196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 / 2) ∈ ℕ0
→ (𝑎 / 2) ∈
(0[,)+∞)) |
104 | 1, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 / 2) ∈
(0[,)+∞)) |
105 | 104 | ad4antr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ (0[,)+∞)) |
106 | | digvalnn0 45956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2
∈ ℕ ∧ 𝑖
∈ ℤ ∧ (𝑎 /
2) ∈ (0[,)+∞)) → (𝑖(digit‘2)(𝑎 / 2)) ∈
ℕ0) |
107 | 100, 102,
105, 106 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈
ℕ0) |
108 | 107 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ) |
109 | | 2re 12056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℝ |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℝ) |
111 | 110, 92 | reexpcld 13890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℝ) |
112 | 111 | recnd 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ) |
114 | | 2cnd 12060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ) |
115 | | mulass 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧
(2↑𝑖) ∈ ℂ
∧ 2 ∈ ℂ) → (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2))) |
116 | 115 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧
(2↑𝑖) ∈ ℂ
∧ 2 ∈ ℂ) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
117 | 108, 113,
114, 116 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
118 | 99, 117 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
119 | 118 | sumeq2dv 15424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
120 | | 0cn 10976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℂ |
121 | | pncan1 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (0 ∈
ℂ → ((0 + 1) − 1) = 0) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((0 + 1)
− 1) = 0 |
123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ → ((0 + 1)
− 1) = 0) |
124 | 123 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0...(𝑦 −
1))) |
125 | | fzoval 13397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ →
(0..^𝑦) = (0...(𝑦 − 1))) |
126 | 125 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℤ →
(0...(𝑦 − 1)) =
(0..^𝑦)) |
127 | 20, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ →
(0...(𝑦 − 1)) =
(0..^𝑦)) |
128 | 124, 127 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0..^𝑦)) |
129 | 128 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0 + 1) −
1)...(𝑦 − 1)) =
(0..^𝑦)) |
130 | 129 | sumeq1d 15422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
131 | 130 | oveq2d 7300 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
132 | | fzofi 13703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0..^𝑦) ∈
Fin |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^𝑦) ∈ Fin) |
134 | 101 | peano2zd 12438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℤ) |
135 | 134 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ ℤ) |
136 | 36 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ (0[,)+∞)) |
137 | | digvalnn0 45956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((2
∈ ℕ ∧ (𝑖 +
1) ∈ ℤ ∧ 𝑎
∈ (0[,)+∞)) → ((𝑖 + 1)(digit‘2)𝑎) ∈
ℕ0) |
138 | 100, 135,
136, 137 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈
ℕ0) |
139 | 138 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℂ) |
140 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈
ℕ0) |
141 | | peano2nn0 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
142 | 92, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈
ℕ0) |
143 | 140, 142 | nn0expcld 13970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈
ℕ0) |
144 | 143 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℂ) |
145 | 144 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) ∈ ℂ) |
146 | 139, 145 | mulcld 11004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ) |
147 | 133, 146 | fsumcl 15454 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ) |
148 | 147 | addid2d 11185 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
149 | 131, 148 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
150 | | 2cnd 12060 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
151 | 140, 92 | nn0expcld 13970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈
ℕ0) |
152 | 151 | nn0cnd 12304 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ) |
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ) |
154 | 108, 153 | mulcld 11004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) ∈ ℂ) |
155 | 133, 150,
154 | fsummulc1 15506 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
156 | 119, 149,
155 | 3eqtr4d 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
157 | 89, 156 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((0(digit‘2)𝑎)
· 1) + Σ𝑘
∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
158 | 25, 56, 157 | 3eqtrd 2783 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
159 | 158 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
160 | | oveq1 7291 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (𝑘(digit‘2)(𝑎 / 2)) = (𝑖(digit‘2)(𝑎 / 2))) |
161 | | oveq2 7292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖)) |
162 | 160, 161 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
163 | 162 | cbvsumv 15417 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑘 ∈
(0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
165 | 164 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))) |
166 | 165 | biimpac 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
167 | 166 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) = (𝑎 / 2)) |
168 | 167 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
(Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑎 / 2) · 2)) |
169 | | nncn 11990 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
170 | | 2cnd 12060 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 2 ∈
ℂ) |
171 | | 2ne0 12086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 2 ≠
0) |
173 | 169, 170,
172 | divcan1d 11761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ ℕ → ((𝑎 / 2) · 2) = 𝑎) |
174 | 173 | ad3antlr 728 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) · 2) = 𝑎) |
175 | 174 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → ((𝑎 / 2) · 2) = 𝑎) |
176 | 159, 168,
175 | 3eqtrrd 2784 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
177 | 176 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
178 | 177 | imim2i 16 |
. . . . . . . . . . . . . . 15
⊢
(((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = 𝑦 → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
179 | 178 | com13 88 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = 𝑦 →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
180 | 19, 179 | sylbid 239 |
. . . . . . . . . . . . 13
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
181 | 180 | com23 86 |
. . . . . . . . . . . 12
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → 𝑎 =
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
182 | 181 | exp31 420 |
. . . . . . . . . . 11
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((#b‘𝑎) =
(𝑦 + 1) → (𝑦 ∈ ℕ →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → 𝑎 =
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
183 | 182 | com25 99 |
. . . . . . . . . 10
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
184 | 183 | com14 96 |
. . . . . . . . 9
⊢
(((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
185 | 12, 184 | syl 17 |
. . . . . . . 8
⊢ (((𝑎 / 2) ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
186 | 185 | ex 413 |
. . . . . . 7
⊢ ((𝑎 / 2) ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
187 | 186 | com25 99 |
. . . . . 6
⊢ ((𝑎 / 2) ∈ ℕ0
→ (((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) → ((#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
188 | 187 | expdcom 415 |
. . . . 5
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 ∈ ℕ →
((𝑎 / 2) ∈
ℕ0 → ((#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))) |
189 | 1, 188 | mpid 44 |
. . . 4
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 ∈ ℕ →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
190 | 189 | impcom 408 |
. . 3
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
191 | 3, 190 | mpd 15 |
. 2
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
(𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
192 | 191 | imp 407 |
1
⊢ (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧
𝑦 ∈ ℕ) →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |