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 45033

Description: Lemma for nn0sumshdig 45037 (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 11892	. . . 4 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ ℕ₀)
2		blennn0em1 45005	. . . 4 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ₀) → (#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1))
3	1, 2	sylan2 595	. . 3 ⊢ ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → (#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1))
4		fveqeq2 6654	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑎 / 2) → ((#_b‘𝑥) = 𝑦 ↔ (#_b‘(𝑎 / 2)) = 𝑦))
5		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑎 / 2) → 𝑥 = (𝑎 / 2))
6		oveq2 7143	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑎 / 2) → (𝑘(digit‘2)𝑥) = (𝑘(digit‘2)(𝑎 / 2)))
7	6	oveq1d 7150	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑎 / 2) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
8	7	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝑎 / 2) ∧ 𝑘 ∈ (0..^𝑦)) → ((𝑘(digit‘2)𝑥) · (2↑𝑘)) = ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
9	8	sumeq2dv 15052	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑎 / 2) → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))
10	5, 9	eqeq12d 2814	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑎 / 2) → (𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
11	4, 10	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑥 = (𝑎 / 2) → (((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) ↔ ((#_b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)))))
12	11	rspcva 3569	. . . . . . . . 9 ⊢ (((𝑎 / 2) ∈ ℕ₀ ∧ ∀𝑥 ∈ ℕ₀ ((#_b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#_b‘(𝑎 / 2)) = 𝑦 → (𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘))))
13		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → (#_b‘𝑎) = (𝑦 + 1))
14	13	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → ((#_b‘𝑎) − 1) = ((𝑦 + 1) − 1))
15		nncn 11633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
16		pncan1 11053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦)
17	15, 16	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) − 1) = 𝑦)
18	14, 17	sylan9eq 2853	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#_b‘𝑎) − 1) = 𝑦)
19	18	eqeq2d 2809	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((#_b‘(𝑎 / 2)) = ((#_b‘𝑎) − 1) ↔ (#_b‘(𝑎 / 2)) = 𝑦))
20		nnz 11992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
21	20	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
22		fzval3 13101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℤ → (0...𝑦) = (0..^(𝑦 + 1)))
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0...𝑦) = (0..^(𝑦 + 1)))
24	23	eqcomd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^(𝑦 + 1)) = (0...𝑦))
25	24	sumeq1d 15050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)))
26		nnnn0 11892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
27		elnn0uz 12271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ (ℤ_≥‘0))
28	26, 27	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘0))
29	28	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘0))
30		2nn 11698	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 2 ∈ ℕ)
32		elfzelz 12902	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℤ)
33	32	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑘 ∈ ℤ)
34		nnnn0 11892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ₀)
35		nn0rp0 12833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ℕ₀ → 𝑎 ∈ (0[,)+∞))
36	34, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ (0[,)+∞))
37	36	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → 𝑎 ∈ (0[,)+∞))
38		digvalnn0 45013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
39	31, 33, 37, 38	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
40	39	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
41		2nn0 11902	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℕ₀
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 2 ∈ ℕ₀)
43		elfznn0 12995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑦) → 𝑘 ∈ ℕ₀)
44	42, 43	nn0expcld 13603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℕ₀)
45	44	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (0...𝑦) → (2↑𝑘) ∈ ℂ)
46	45	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → (2↑𝑘) ∈ ℂ)
47	40, 46	mulcld 10650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
48		oveq1 7142	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → (𝑘(digit‘2)𝑎) = (0(digit‘2)𝑎))
49		oveq2 7143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
50	48, 49	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · (2↑0)))
51		2cn 11700	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℂ
52		exp0 13429	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 ∈ ℂ → (2↑0) = 1)
53	51, 52	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2↑0) = 1
54	53	oveq2i 7146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0(digit‘2)𝑎) · (2↑0)) = ((0(digit‘2)𝑎) · 1)
55	50, 54	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((0(digit‘2)𝑎) · 1))
56	29, 47, 55	fsum1p 15100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
57		0dig2nn0e 45026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ ℕ₀ ∧ (𝑎 / 2) ∈ ℕ₀) → (0(digit‘2)𝑎) = 0)
58	34, 1, 57	syl2anr 599	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → (0(digit‘2)𝑎) = 0)
59	58	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = (0 · 1))
60		1re 10630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
61		mul02lem2 10806	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 · 1) = 0)
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 · 1) = 0
63	59, 62	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
64	63	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) → ((0(digit‘2)𝑎) · 1) = 0)
65	64	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((0(digit‘2)𝑎) · 1) = 0)
66		1z 12000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℤ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℤ)
68		0p1e1 11747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
69	68, 66	eqeltri 2886	. . . . . . . . . . . . . . . . . . . . . . . 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 12902	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℤ)
73	72	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑘 ∈ ℤ)
74	36	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → 𝑎 ∈ (0[,)+∞))
75	71, 73, 74, 38	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℕ₀)
76	75	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (𝑘(digit‘2)𝑎) ∈ ℂ)
77		2cnd 11703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 2 ∈ ℂ)
78		elfznn 12931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ)
79	78	nnnn0d 11943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...𝑦) → 𝑘 ∈ ℕ₀)
80	68	oveq1i 7145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 + 1)...𝑦) = (1...𝑦)
81	79, 80	eleq2s 2908	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → 𝑘 ∈ ℕ₀)
82	77, 81	expcld 13506	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ((0 + 1)...𝑦) → (2↑𝑘) ∈ ℂ)
83	82	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → (2↑𝑘) ∈ ℂ)
84	76, 83	mulcld 10650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑘 ∈ ((0 + 1)...𝑦)) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) ∈ ℂ)
85		oveq1 7142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝑖 + 1) → (𝑘(digit‘2)𝑎) = ((𝑖 + 1)(digit‘2)𝑎))
86		oveq2 7143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝑖 + 1) → (2↑𝑘) = (2↑(𝑖 + 1)))
87	85, 86	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑖 + 1) → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
88	67, 70, 21, 84, 87	fsumshftm 15128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
89	65, 88	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . 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 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ ℕ₀)
91	34	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ ℕ₀)
92		elfzonn0 13077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℕ₀)
93	92	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℕ₀)
94		dignn0ehalf 45031	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 / 2) ∈ ℕ₀ ∧ 𝑎 ∈ ℕ₀ ∧ 𝑖 ∈ ℕ₀) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
95	90, 91, 93, 94	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) = (𝑖(digit‘2)(𝑎 / 2)))
96		2cnd 11703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℂ)
97	96, 92	expp1d 13507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
98	97	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) = ((2↑𝑖) · 2))
99	95, 98	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . . . . 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 13033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ ℤ)
102	101	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ ℤ)
103		nn0rp0 12833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 / 2) ∈ ℕ₀ → (𝑎 / 2) ∈ (0[,)+∞))
104	1, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 / 2) ∈ ℕ → (𝑎 / 2) ∈ (0[,)+∞))
105	104	ad4antr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑎 / 2) ∈ (0[,)+∞))
106		digvalnn0 45013	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2 ∈ ℕ ∧ 𝑖 ∈ ℤ ∧ (𝑎 / 2) ∈ (0[,)+∞)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ₀)
107	100, 102, 105, 106	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℕ₀)
108	107	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ)
109		2re 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
110	109	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℝ)
111	110, 92	reexpcld 13523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℝ)
112	111	recnd 10658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
113	112	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
114		2cnd 11703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 2 ∈ ℂ)
115		mulass 10614	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)))
116	115	eqcomd 2804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑖(digit‘2)(𝑎 / 2)) ∈ ℂ ∧ (2↑𝑖) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
117	108, 113, 114, 116	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · ((2↑𝑖) · 2)) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
118	99, 117	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = (((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
119	118	sumeq2dv 15052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
120		0cn 10622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 ∈ ℂ
121		pncan1 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0...(𝑦 − 1)))
125		fzoval 13034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ ℤ → (0..^𝑦) = (0...(𝑦 − 1)))
126	125	eqcomd 2804	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ ℤ → (0...(𝑦 − 1)) = (0..^𝑦))
127	20, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → (0...(𝑦 − 1)) = (0..^𝑦))
128	124, 127	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
129	128	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0 + 1) − 1)...(𝑦 − 1)) = (0..^𝑦))
130	129	sumeq1d 15050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
131	130	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))))
132		fzofi 13337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0..^𝑦) ∈ Fin
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0..^𝑦) ∈ Fin)
134	101	peano2zd 12078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℤ)
135	134	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ ℤ)
136	36	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑎 ∈ (0[,)+∞))
137		digvalnn0 45013	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑎 ∈ (0[,)+∞)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ₀)
138	100, 135, 136, 137	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℕ₀)
139	138	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖 + 1)(digit‘2)𝑎) ∈ ℂ)
140	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → 2 ∈ ℕ₀)
141		peano2nn0 11925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
142	92, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ ℕ₀)
143	140, 142	nn0expcld 13603	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℕ₀)
144	143	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑(𝑖 + 1)) ∈ ℂ)
145	144	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑(𝑖 + 1)) ∈ ℂ)
146	139, 145	mulcld 10650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
147	133, 146	fsumcl 15082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))) ∈ ℂ)
148	147	addid2d 10830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
149	131, 148	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = Σ𝑖 ∈ (0..^𝑦)(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1))))
150		2cnd 11703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
151	140, 92	nn0expcld 13603	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℕ₀)
152	151	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ (0..^𝑦) → (2↑𝑖) ∈ ℂ)
153	152	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → (2↑𝑖) ∈ ℂ)
154	108, 153	mulcld 10650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) ∈ ℂ)
155	133, 150, 154	fsummulc1 15132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = Σ𝑖 ∈ (0..^𝑦)(((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
156	119, 149, 155	3eqtr4d 2843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (0 + Σ𝑖 ∈ (((0 + 1) − 1)...(𝑦 − 1))(((𝑖 + 1)(digit‘2)𝑎) · (2↑(𝑖 + 1)))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
157	89, 156	eqtrd 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → (((0(digit‘2)𝑎) · 1) + Σ𝑘 ∈ ((0 + 1)...𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
158	25, 56, 157	3eqtrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
159	158	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2))
160		oveq1 7142	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘(digit‘2)(𝑎 / 2)) = (𝑖(digit‘2)(𝑎 / 2)))
161		oveq2 7143	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (2↑𝑘) = (2↑𝑖))
162	160, 161	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) = ((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
163	162	cbvsumv 15045	. . . . . . . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ↔ (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖))))
166	165	biimpac 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (𝑎 / 2) = Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)))
167	166	eqcomd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) = (𝑎 / 2))
168	167	oveq1d 7150	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → (Σ𝑖 ∈ (0..^𝑦)((𝑖(digit‘2)(𝑎 / 2)) · (2↑𝑖)) · 2) = ((𝑎 / 2) · 2))
169		nncn 11633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
170		2cnd 11703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℂ)
171		2ne0 11729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → 2 ≠ 0)
173	169, 170, 172	divcan1d 11406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ ℕ → ((𝑎 / 2) · 2) = 𝑎)
174	173	ad3antlr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ) → ((𝑎 / 2) · 2) = 𝑎)
175	174	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → ((𝑎 / 2) · 2) = 𝑎)
176	159, 168, 175	3eqtrrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 / 2) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)(𝑎 / 2)) · (2↑𝑘)) ∧ ((((𝑎 / 2) ∈ ℕ ∧ 𝑎 ∈ ℕ) ∧ (#_b‘𝑎) = (𝑦 + 1)) ∧ 𝑦 ∈ ℕ)) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))
177	176	ex 416	. . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . 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 423	. . . . . . . . . . 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 416	. . . . . . 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 418	. . . . 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 411	. . 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 410	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 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ‘cfv 6324 (class class class)co 7135 Fincfn 8492 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 +∞cpnf 10661 − cmin 10859 / cdiv 11286 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 [,)cico 12728 ...cfz 12885 ..^cfzo 13028 ↑cexp 13425 Σcsu 15034 #_bcblen 44983 digitcdig 45009

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-fi 8859 df-sup 8890 df-inf 8891 df-oi 8958 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-ioc 12731 df-ico 12732 df-icc 12733 df-fz 12886 df-fzo 13029 df-fl 13157 df-mod 13233 df-seq 13365 df-exp 13426 df-fac 13630 df-bc 13659 df-hash 13687 df-shft 14418 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-limsup 14820 df-clim 14837 df-rlim 14838 df-sum 15035 df-ef 15413 df-sin 15415 df-cos 15416 df-pi 15418 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-fbas 20088 df-fg 20089 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-cls 21626 df-nei 21703 df-lp 21741 df-perf 21742 df-cn 21832 df-cnp 21833 df-haus 21920 df-tx 22167 df-hmeo 22360 df-fil 22451 df-fm 22543 df-flim 22544 df-flf 22545 df-xms 22927 df-ms 22928 df-tms 22929 df-cncf 23483 df-limc 24469 df-dv 24470 df-log 25148 df-logb 25351 df-blen 44984 df-dig 45010

This theorem is referenced by: nn0sumshdiglem1 45035

W3C validator