| Step | Hyp | Ref
| Expression |
| 1 | | eqeq2 2749 |
. . . 4
⊢ (𝑥 = 1 →
((#b‘𝑎) =
𝑥 ↔
(#b‘𝑎) =
1)) |
| 2 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1)) |
| 3 | | fzo01 13786 |
. . . . . . 7
⊢ (0..^1) =
{0} |
| 4 | 2, 3 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 = 1 → (0..^𝑥) = {0}) |
| 5 | 4 | sumeq1d 15736 |
. . . . 5
⊢ (𝑥 = 1 → Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 6 | 5 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = 1 → (𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
| 7 | 1, 6 | imbi12d 344 |
. . 3
⊢ (𝑥 = 1 →
(((#b‘𝑎) =
𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ((#b‘𝑎) = 1 → 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 8 | 7 | ralbidv 3178 |
. 2
⊢ (𝑥 = 1 → (∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ∀𝑎 ∈ ℕ0
((#b‘𝑎) =
1 → 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 9 | | eqeq2 2749 |
. . . 4
⊢ (𝑥 = 𝑦 → ((#b‘𝑎) = 𝑥 ↔ (#b‘𝑎) = 𝑦)) |
| 10 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦)) |
| 11 | 10 | sumeq1d 15736 |
. . . . 5
⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 12 | 11 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
| 13 | 9, 12 | imbi12d 344 |
. . 3
⊢ (𝑥 = 𝑦 → (((#b‘𝑎) = 𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 14 | 13 | ralbidv 3178 |
. 2
⊢ (𝑥 = 𝑦 → (∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 15 | | eqeq2 2749 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((#b‘𝑎) = 𝑥 ↔ (#b‘𝑎) = (𝑦 + 1))) |
| 16 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1))) |
| 17 | 16 | sumeq1d 15736 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 18 | 17 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
| 19 | 15, 18 | imbi12d 344 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (((#b‘𝑎) = 𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 20 | 19 | ralbidv 3178 |
. 2
⊢ (𝑥 = (𝑦 + 1) → (∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ∀𝑎 ∈ ℕ0
((#b‘𝑎) =
(𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 21 | | eqeq2 2749 |
. . . 4
⊢ (𝑥 = 𝐿 → ((#b‘𝑎) = 𝑥 ↔ (#b‘𝑎) = 𝐿)) |
| 22 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝐿 → (0..^𝑥) = (0..^𝐿)) |
| 23 | 22 | sumeq1d 15736 |
. . . . 5
⊢ (𝑥 = 𝐿 → Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 24 | 23 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = 𝐿 → (𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
| 25 | 21, 24 | imbi12d 344 |
. . 3
⊢ (𝑥 = 𝐿 → (((#b‘𝑎) = 𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 26 | 25 | ralbidv 3178 |
. 2
⊢ (𝑥 = 𝐿 → (∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝑥 → 𝑎 = Σ𝑘 ∈ (0..^𝑥)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ∀𝑎 ∈ ℕ0
((#b‘𝑎) =
𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 27 | | 0cnd 11254 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ0
→ 0 ∈ ℂ) |
| 28 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ0
→ 2 ∈ ℕ) |
| 30 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ0
→ 0 ∈ ℤ) |
| 31 | | nn0rp0 13495 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
(0[,)+∞)) |
| 32 | | digvalnn0 48520 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 0 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) →
(0(digit‘2)𝑎) ∈
ℕ0) |
| 33 | 29, 30, 31, 32 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ0
→ (0(digit‘2)𝑎)
∈ ℕ0) |
| 34 | 33 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ0
→ (0(digit‘2)𝑎)
∈ ℂ) |
| 35 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ0
→ 1 ∈ ℂ) |
| 36 | 34, 35 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ0
→ ((0(digit‘2)𝑎)
· 1) ∈ ℂ) |
| 37 | 27, 36 | jca 511 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ0
→ (0 ∈ ℂ ∧ ((0(digit‘2)𝑎) · 1) ∈
ℂ)) |
| 38 | 37 | adantr 480 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → (0 ∈ ℂ ∧
((0(digit‘2)𝑎)
· 1) ∈ ℂ)) |
| 39 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎)) |
| 40 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
| 41 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 42 | | exp0 14106 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ → (2↑0) = 1) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . . . . 9
⊢
(2↑0) = 1 |
| 44 | 40, 43 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑘 = 0 → (2↑𝑘) = 1) |
| 45 | 39, 44 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
| 46 | 45 | sumsn 15782 |
. . . . . 6
⊢ ((0
∈ ℂ ∧ ((0(digit‘2)𝑎) · 1) ∈ ℂ) →
Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
| 47 | 38, 46 | syl 17 |
. . . . 5
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1)) |
| 48 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → (0(digit‘2)𝑎) ∈
ℂ) |
| 49 | 48 | mulridd 11278 |
. . . . 5
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → ((0(digit‘2)𝑎) · 1) =
(0(digit‘2)𝑎)) |
| 50 | | blen1b 48509 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ0
→ ((#b‘𝑎) = 1 ↔ (𝑎 = 0 ∨ 𝑎 = 1))) |
| 51 | 50 | biimpa 476 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → (𝑎 = 0 ∨ 𝑎 = 1)) |
| 52 | | vex 3484 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
| 53 | 52 | elpr 4650 |
. . . . . . 7
⊢ (𝑎 ∈ {0, 1} ↔ (𝑎 = 0 ∨ 𝑎 = 1)) |
| 54 | 51, 53 | sylibr 234 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → 𝑎 ∈ {0, 1}) |
| 55 | | 0dig2pr01 48531 |
. . . . . 6
⊢ (𝑎 ∈ {0, 1} →
(0(digit‘2)𝑎) = 𝑎) |
| 56 | 54, 55 | syl 17 |
. . . . 5
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → (0(digit‘2)𝑎) = 𝑎) |
| 57 | 47, 49, 56 | 3eqtrrd 2782 |
. . . 4
⊢ ((𝑎 ∈ ℕ0
∧ (#b‘𝑎) = 1) → 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 58 | 57 | ex 412 |
. . 3
⊢ (𝑎 ∈ ℕ0
→ ((#b‘𝑎) = 1 → 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |
| 59 | 58 | rgen 3063 |
. 2
⊢
∀𝑎 ∈
ℕ0 ((#b‘𝑎) = 1 → 𝑎 = Σ𝑘 ∈ {0} ((𝑘(digit‘2)𝑎) · (2↑𝑘))) |
| 60 | | nn0sumshdiglem1 48542 |
. 2
⊢ (𝑦 ∈ ℕ →
(∀𝑎 ∈
ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0
((#b‘𝑎) =
(𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) |
| 61 | 8, 14, 20, 26, 59, 60 | nnind 12284 |
1
⊢ (𝐿 ∈ ℕ →
∀𝑎 ∈
ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) |