Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . 4
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 / 2) ∈
ℕ0) |
2 | | blennn0em1 42183 |
. . . 4
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈
ℕ0) → (#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1)) |
3 | 1, 2 | sylan2 490 |
. . 3
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
(#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1)) |
4 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 / 2) → (#b‘𝑥) = (#b‘(𝑎 / 2))) |
5 | 4 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 / 2) → ((#b‘𝑥) = 𝑦 ↔ (#b‘(𝑎 / 2)) = 𝑦)) |
6 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 / 2) → 𝑥 = (𝑎 / 2)) |
7 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)(𝑎 / 2))) |
8 | 7 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑎 / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑎 / 2) ∧ 𝑘 ∈ (0..^𝑦)) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
10 | 9 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) |
11 | 6, 10 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))) |
12 | 5, 11 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑎 / 2) → (((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))) |
13 | 12 | rspcva 3280 |
. . . . . . . . 9
⊢ (((𝑎 / 2) ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))) |
14 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
(#b‘𝑎) =
(𝑦 + 1)) |
15 | 14 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
((#b‘𝑎)
− 1) = ((𝑦 + 1)
− 1)) |
16 | | nncn 10905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
17 | | pncan1 10333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦) |
19 | 15, 18 | sylan9eq 2664 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘𝑎)
− 1) = 𝑦) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) ↔
(#b‘(𝑎 /
2)) = 𝑦)) |
21 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ) |
23 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℤ →
(0...𝑦) = (0..^(𝑦 + 1))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0...𝑦) = (0..^(𝑦 + 1))) |
25 | 24 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^(𝑦 + 1)) = (0...𝑦)) |
26 | 25 | sumeq1d 14279 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
27 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
28 | | elnn0uz 11601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈
(ℤ≥‘0)) |
29 | 27, 28 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘0)) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈
(ℤ≥‘0)) |
31 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ) |
33 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ) |
35 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ0) |
36 | | nn0rp0 12150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
(0[,)+∞)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
(0[,)+∞)) |
38 | 37 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
39 | | digvalnn0 42191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 𝑎
∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
40 | 32, 34, 38, 39 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
41 | 40 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
42 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ0 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 2 ∈
ℕ0) |
44 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ0) |
45 | 43, 44 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈
ℕ0) |
46 | 45 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ) |
48 | 41, 47 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
49 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎)) |
50 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
51 | 49, 50 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0))) |
52 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℂ |
53 | | exp0 12726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 ∈
ℂ → (2↑0) = 1) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2↑0) = 1 |
55 | 54 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0(digit‘2)𝑎)
· (2↑0)) = ((0(digit‘2)𝑎) · 1) |
56 | 51, 55 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
57 | 30, 48, 56 | fsum1p 14326 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
58 | | 0dig2nn0e 42204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ ℕ0
∧ (𝑎 / 2) ∈
ℕ0) → (0(digit‘2)𝑎) = 0) |
59 | 35, 1, 58 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
(0(digit‘2)𝑎) =
0) |
60 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = (0 · 1)) |
61 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℝ |
62 | | mul02lem2 10092 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℝ → (0 · 1) = 0) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0
· 1) = 0 |
64 | 60, 63 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = 0) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) →
((0(digit‘2)𝑎)
· 1) = 0) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((0(digit‘2)𝑎)
· 1) = 0) |
67 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℤ |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 1 ∈
ℤ) |
69 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
70 | 69, 67 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 + 1)
∈ ℤ |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + 1) ∈
ℤ) |
72 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 2 ∈ ℕ) |
73 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ) |
75 | 37 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞)) |
76 | 72, 74, 75, 39 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈
ℕ0) |
77 | 76 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ) |
78 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈
ℂ) |
79 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ) |
80 | 79 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ0) |
81 | 69 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0 +
1)...𝑦) = (1...𝑦) |
82 | 80, 81 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ0) |
83 | 78, 82 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈
ℂ) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ) |
85 | 77, 84 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ) |
86 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎)) |
87 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1))) |
88 | 86, 87 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
89 | 68, 71, 22, 85, 88 | fsumshftm 14355 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
90 | 66, 89 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((0(digit‘2)𝑎)
· 1) + Σ𝑘
∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
91 | 1 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈
ℕ0) |
92 | 35 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ ℕ0) |
93 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ0) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℕ0) |
95 | | dignn0ehalf 42209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 / 2) ∈ ℕ0
∧ 𝑎 ∈
ℕ0 ∧ 𝑖
∈ ℕ0) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2))) |
96 | 91, 92, 94, 95 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2))) |
97 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℂ) |
98 | 97, 93 | expp1d 12871 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2)) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2)) |
100 | 96, 99 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2))) |
101 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℕ) |
102 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ) |
104 | | nn0rp0 12150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 / 2) ∈ ℕ0
→ (𝑎 / 2) ∈
(0[,)+∞)) |
105 | 1, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 / 2) ∈
(0[,)+∞)) |
106 | 105 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ (0[,)+∞)) |
107 | | digvalnn0 42191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((2
∈ ℕ ∧ 𝑖
∈ ℤ ∧ (𝑎 /
2) ∈ (0[,)+∞)) → (𝑖(digit‘2)(𝑎 / 2)) ∈
ℕ0) |
108 | 101, 103,
106, 107 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈
ℕ0) |
109 | 108 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ) |
110 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℝ |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℝ) |
112 | 111, 93 | reexpcld 12887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℝ) |
113 | 112 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ) |
114 | 113 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ) |
115 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ) |
116 | | mulass 9903 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧
(2↑𝑖) ∈ ℂ
∧ 2 ∈ ℂ) → (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2))) |
117 | 116 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧
(2↑𝑖) ∈ ℂ
∧ 2 ∈ ℂ) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
118 | 109, 114,
115, 117 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
119 | 100, 118 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
120 | 119 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
121 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℂ |
122 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (0 ∈
ℂ → ((0 + 1) − 1) = 0) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((0 + 1)
− 1) = 0 |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℕ → ((0 + 1)
− 1) = 0) |
125 | 124 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0...(𝑦 −
1))) |
126 | | fzoval 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℤ →
(0..^𝑦) = (0...(𝑦 − 1))) |
127 | 126 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℤ →
(0...(𝑦 − 1)) =
(0..^𝑦)) |
128 | 21, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ →
(0...(𝑦 − 1)) =
(0..^𝑦)) |
129 | 125, 128 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → (((0 + 1)
− 1)...(𝑦 − 1))
= (0..^𝑦)) |
130 | 129 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0 + 1) −
1)...(𝑦 − 1)) =
(0..^𝑦)) |
131 | 130 | sumeq1d 14279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
132 | 131 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))) |
133 | | fzofi 12635 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0..^𝑦) ∈
Fin |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^𝑦) ∈ Fin) |
135 | 102 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℤ) |
136 | 135 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ ℤ) |
137 | 37 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ (0[,)+∞)) |
138 | | digvalnn0 42191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((2
∈ ℕ ∧ (𝑖 +
1) ∈ ℤ ∧ 𝑎
∈ (0[,)+∞)) → ((𝑖 + 1)(digit‘2)𝑎) ∈
ℕ0) |
139 | 101, 136,
137, 138 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈
ℕ0) |
140 | 139 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℂ) |
141 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈
ℕ0) |
142 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
143 | 93, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈
ℕ0) |
144 | 141, 143 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈
ℕ0) |
145 | 144 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℂ) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) ∈ ℂ) |
147 | 140, 146 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ) |
148 | 134, 147 | fsumcl 14311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ) |
149 | 148 | addid2d 10116 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
150 | 132, 149 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) |
151 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 2 ∈
ℂ) |
152 | 141, 93 | nn0expcld 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈
ℕ0) |
153 | 152 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ) |
154 | 153 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ) |
155 | 109, 154 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) ∈ ℂ) |
156 | 134, 151,
155 | fsummulc1 14359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
157 | 120, 150,
156 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) −
1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
158 | 90, 157 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((0(digit‘2)𝑎)
· 1) + Σ𝑘
∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
159 | 26, 57, 158 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
160 | 159 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2)) |
161 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (𝑘(digit‘2)(𝑎 / 2)) = (𝑖(digit‘2)(𝑎 / 2))) |
162 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖)) |
163 | 161, 162 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
164 | 163 | cbvsumv 14274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑘 ∈
(0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
166 | 165 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))) |
167 | 166 | biimpac 502 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))) |
168 | 167 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) = (𝑎 / 2)) |
169 | 168 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) →
(Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑎 / 2) · 2)) |
170 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
171 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 2 ∈
ℂ) |
172 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℕ → 2 ≠
0) |
174 | 170, 171,
173 | divcan1d 10681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ ℕ → ((𝑎 / 2) · 2) = 𝑎) |
175 | 174 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) · 2) = 𝑎) |
176 | 175 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → ((𝑎 / 2) · 2) = 𝑎) |
177 | 160, 169,
176 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
178 | 177 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
179 | 178 | imim2i 16 |
. . . . . . . . . . . . . . 15
⊢
(((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) = 𝑦 → (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧
(#b‘𝑎) =
(𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
180 | 179 | com13 86 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = 𝑦 →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
181 | 20, 180 | sylbid 229 |
. . . . . . . . . . . . 13
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
182 | 181 | com23 84 |
. . . . . . . . . . . 12
⊢
(((((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) ∧ (#b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → 𝑎 =
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
183 | 182 | exp31 628 |
. . . . . . . . . . 11
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((#b‘𝑎) =
(𝑦 + 1) → (𝑦 ∈ ℕ →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → 𝑎 =
Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
184 | 183 | com25 97 |
. . . . . . . . . 10
⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(((#b‘(𝑎 /
2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
185 | 184 | com14 94 |
. . . . . . . . 9
⊢
(((#b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
186 | 13, 185 | syl 17 |
. . . . . . . 8
⊢ (((𝑎 / 2) ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
187 | 186 | ex 449 |
. . . . . . 7
⊢ ((𝑎 / 2) ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘(𝑎 / 2)) =
((#b‘𝑎)
− 1) → (𝑦 ∈
ℕ → (((𝑎 / 2)
∈ ℕ ∧ 𝑎
∈ ℕ) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
188 | 187 | com25 97 |
. . . . . 6
⊢ ((𝑎 / 2) ∈ ℕ0
→ (((𝑎 / 2) ∈
ℕ ∧ 𝑎 ∈
ℕ) → ((#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
189 | 188 | expdcom 454 |
. . . . 5
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 ∈ ℕ →
((𝑎 / 2) ∈
ℕ0 → ((#b‘(𝑎 / 2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))) |
190 | 1, 189 | mpid 43 |
. . . 4
⊢ ((𝑎 / 2) ∈ ℕ →
(𝑎 ∈ ℕ →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))) |
191 | 190 | impcom 445 |
. . 3
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
((#b‘(𝑎 /
2)) = ((#b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0
((#b‘𝑥) =
𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))) |
192 | 3, 191 | mpd 15 |
. 2
⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) →
(𝑦 ∈ ℕ →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))) |
193 | 192 | imp 444 |
1
⊢ (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧
𝑦 ∈ ℕ) →
(∀𝑥 ∈
ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |