nn0sumshdiglemA - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nn0sumshdiglemA		Structured version Visualization version GIF version

Theorem nn0sumshdiglemA 48608

Description: Lemma for nn0sumshdig 48612 (induction step, even multiplier). (Contributed by AV, 3-Jun-2020.)

**Assertion**
Ref	Expression
nn0sumshdiglemA	⊢ (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))

Distinct variable group: 𝑘,𝑎,𝑥,𝑦

Proof of Theorem nn0sumshdiglemA Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnnn0 12449	. . . 4 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ ℕ₀)
2		blennn0em1 48580	. . . 4 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ₀) → (#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1))
3	1, 2	sylan2 593	. . 3 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → (#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1))
4		fveqeq2 6867	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑎 / 2) → ((#_b‘𝑥) = 𝑦 ↔ (#_b‘(𝑎 / 2)) = 𝑦))
5		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑎 / 2) → 𝑥 = (𝑎 / 2))
6		oveq2 7395	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑎 / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)(𝑎 / 2)))
7	6	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑎 / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
8	7	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑎 / 2) ∧ 𝑘 ∈ (0..^𝑦)) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
9	8	sumeq2dv 15668	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑎 / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
10	5, 9	eqeq12d 2745	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑎 / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
11	4, 10	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = (𝑎 / 2) → (((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#_b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))))
12	11	rspcva 3586	. . . . . . . . 9 ⊢ (((𝑎 / 2) ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#_b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
13		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → (#_b‘𝑎) = (𝑦 + 1))
14	13	oveq1d 7402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → ((#_b‘𝑎) − 1) = ((𝑦 + 1) − 1))
15		nncn 12194	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
16		pncan1 11602	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦)
17	15, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦)
18	14, 17	sylan9eq 2784	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#_b‘𝑎) − 1) = 𝑦)
19	18	eqeq2d 2740	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) ↔ (#_b‘(𝑎 / 2)) = 𝑦))
20		nnz 12550	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
21	20	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
22		fzval3 13695	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0...𝑦) = (0..^(𝑦 + 1)))
24	23	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^(𝑦 + 1)) = (0...𝑦))
25	24	sumeq1d 15666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
26		nnnn0 12449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
27		elnn0uz 12838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ (ℤ_≥‘0))
28	26, 27	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘0))
29	28	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘0))
30		2nn 12259	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
32		elfzelz 13485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
33	32	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
34		nnnn0 12449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ₀)
35		nn0rp0 13416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ℕ₀ → 𝑎 ∈ (0[,)+∞))
36	34, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ (0[,)+∞))
37	36	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
38		digvalnn0 48588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
39	31, 33, 37, 38	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
40	39	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
41		2nn0 12459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℕ₀
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ₀)
43		elfznn0 13581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ₀)
44	42, 43	nn0expcld 14211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ₀)
45	44	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
46	45	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
47	40, 46	mulcld 11194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
48		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
49		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
50	48, 49	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
51		2cn 12261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
52		exp0 14030	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 ∈ ℂ → (2↑0) = 1)
53	51, 52	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑0) = 1
54	53	oveq2i 7398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
55	50, 54	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
56	29, 47, 55	fsum1p 15719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
57		0dig2nn0e 48601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ ℕ₀ ∧ (𝑎 / 2) ∈ ℕ₀) → (0(digit‘2)𝑎) = 0)
58	34, 1, 57	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → (0(digit‘2)𝑎) = 0)
59	58	oveq1d 7402	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = (0 · 1))
60		1re 11174	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
61		mul02lem2 11351	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 · 1) = 0)
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 · 1) = 0
63	59, 62	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → ((0(digit‘2)𝑎) · 1) = 0)
65	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
66		1z 12563	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℤ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℤ)
68		0p1e1 12303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
69	68, 66	eqeltri 2824	. . . . . . . . . . . . . . . . . . . . . . . 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 13485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
73	72	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
74	36	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
75	71, 73, 74, 38	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
76	75	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
77		2cnd 12264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
78		elfznn 13514	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
79	78	nnnn0d 12503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ₀)
80	68	oveq1i 7397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 + 1)...𝑦) = (1...𝑦)
81	79, 80	eleq2s 2846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ₀)
82	77, 81	expcld 14111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
83	82	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
84	76, 83	mulcld 11194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
85		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
86		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
87	85, 86	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
88	67, 70, 21, 84, 87	fsumshftm 15747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
89	65, 88	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ ℕ₀)
91	34	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ ℕ₀)
92		elfzonn0 13668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ₀)
93	92	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℕ₀)
94		dignn0ehalf 48606	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 / 2) ∈ ℕ₀ ∧ 𝑎 ∈ ℕ₀ ∧ 𝑖 ∈ ℕ₀) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
95	90, 91, 93, 94	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
96		2cnd 12264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℂ)
97	96, 92	expp1d 14112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
98	97	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
99	95, 98	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . 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 13620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
103		nn0rp0 13416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 / 2) ∈ ℕ₀ → (𝑎 / 2) ∈ (0[,)+∞))
104	1, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ (0[,)+∞))
105	104	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ (0[,)+∞))
106		digvalnn0 48588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ (𝑎 / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ₀)
107	100, 102, 105, 106	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ₀)
108	107	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ)
109		2re 12260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
110	109	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℝ)
111	110, 92	reexpcld 14128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℝ)
112	111	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
113	112	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
114		2cnd 12264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
115		mulass 11156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)))
116	115	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
117	108, 113, 114, 116	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
118	99, 117	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
119	118	sumeq2dv 15668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
120		0cn 11166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ ℂ
121		pncan1 11602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
125		fzoval 13621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
126	125	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ ℤ → (0...(𝑦 − 1)) = (0..^𝑦))
127	20, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → (0...(𝑦 − 1)) = (0..^𝑦))
128	124, 127	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
129	128	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
130	129	sumeq1d 15666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
131	130	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
132		fzofi 13939	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0..^𝑦) ∈ Fin
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^𝑦) ∈ Fin)
134	101	peano2zd 12641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℤ)
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ ℤ)
136	36	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ (0[,)+∞))
137		digvalnn0 48588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ₀)
138	100, 135, 136, 137	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ₀)
139	138	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℂ)
140	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ₀)
141		peano2nn0 12482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
142	92, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℕ₀)
143	140, 142	nn0expcld 14211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℕ₀)
144	143	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℂ)
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) ∈ ℂ)
146	139, 145	mulcld 11194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
147	133, 146	fsumcl 15699	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
148	147	addlidd 11375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
149	131, 148	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
150		2cnd 12264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
151	140, 92	nn0expcld 14211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ₀)
152	151	nn0cnd 12505	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
153	152	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
154	108, 153	mulcld 11194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) ∈ ℂ)
155	133, 150, 154	fsummulc1 15751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
156	119, 149, 155	3eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
157	89, 156	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
158	25, 56, 157	3eqtrd 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
159	158	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
160		oveq1 7394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘(digit‘2)(𝑎 / 2)) = (𝑖(digit‘2)(𝑎 / 2)))
161		oveq2 7395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
162	160, 161	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
163	162	cbvsumv 15662	. . . . . . . . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))))
166	165	biimpac 478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
167	166	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) = (𝑎 / 2))
168	167	oveq1d 7402	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑎 / 2) · 2))
169		nncn 12194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
170		2cnd 12264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℂ)
171		2ne0 12290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 2 ≠ 0)
173	169, 170, 172	divcan1d 11959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ ℕ → ((𝑎 / 2) · 2) = 𝑎)
174	173	ad3antlr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) · 2) = 𝑎)
175	174	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → ((𝑎 / 2) · 2) = 𝑎)
176	159, 168, 175	3eqtrrd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
177	176	ex 412	. . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . 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 419	. . . . . . . . . . 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) ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
186	185	ex 412	. . . . . . 7 ⊢ ((𝑎 / 2) ∈ ℕ₀ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
187	186	com25 99	. . . . . 6 ⊢ ((𝑎 / 2) ∈ ℕ₀ → (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
188	187	expdcom 414	. . . . 5 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 ∈ ℕ → ((𝑎 / 2) ∈ ℕ₀ → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))))
189	1, 188	mpid 44	. . . 4 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 ∈ ℕ → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))))
190	189	impcom 407	. . 3 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))))
191	3, 190	mpd 15	. 2 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))))
192	191	imp 406	1 ⊢ (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#_b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ‘cfv 6511 (class class class)co 7387 Fincfn 8918 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 +∞cpnf 11205 − cmin 11405 / cdiv 11835 ℕcn 12186 2c2 12241 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 [,)cico 13308 ...cfz 13468 ..^cfzo 13615 ↑cexp 14026 Σcsu 15652 #_bcblen 48558 digitcdig 48584

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15033 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-limsup 15437 df-clim 15454 df-rlim 15455 df-sum 15653 df-ef 16033 df-sin 16035 df-cos 16036 df-pi 16038 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-fbas 21261 df-fg 21262 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-lp 23023 df-perf 23024 df-cn 23114 df-cnp 23115 df-haus 23202 df-tx 23449 df-hmeo 23642 df-fil 23733 df-fm 23825 df-flim 23826 df-flf 23827 df-xms 24208 df-ms 24209 df-tms 24210 df-cncf 24771 df-limc 25767 df-dv 25768 df-log 26465 df-logb 26675 df-blen 48559 df-dig 48585

This theorem is referenced by: nn0sumshdiglem1 48610

W3C validator