nn0sumshdiglem1

Description: Lemma 1 for nn0sumshdig (induction step). (Contributed by AV, 7-Jun-2020)

		Ref	Expression
	Assertion	nn0sumshdiglem1	$⊢ y \in ℕ \to (\forall a \in ℕ_{0} (#_{b(a)=y\toa = \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k}\to\forall a \in ℕ_{0} (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$⊢ a = x \to (#_{b(a)=y\leftrightarrow#_{b} (x) = y})$
2		id	$⊢ a = x \to a = x$
3		oveq2	$⊢ a = x \to k digit (2) a = k digit (2) x$
4	3	oveq1d	$⊢ a = x \to (k digit (2) a) 2^{k} = (k digit (2) x) 2^{k}$
5	4	sumeq2sdv	$⊢ a = x \to \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k} = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}$
6	2 5	eqeq12d	$⊢ a = x \to (a = \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k} \leftrightarrow x = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k})$
7	1 6	imbi12d	$⊢ a = x \to ((#_{b(a)=y\toa = \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k}\leftrightarrow(#_{b} (x) = y \to x = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k})}))$
8	7	cbvralvw	$⊢ \forall a \in ℕ_{0} (#_{b(a)=y\toa = \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k}\leftrightarrow\forall x \in ℕ_{0} (#_{b} (x) = y \to x = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k})})$
9		elnn0	$⊢ a \in ℕ_{0} \leftrightarrow (a \in ℕ \lor a = 0)$
10		nn0sumshdiglemA	$⊢ ((a \in ℕ \land \frac{a}{2} \in ℕ) \land y \in ℕ) \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$
11	10	expimpd	$⊢ (a \in ℕ \land \frac{a}{2} \in ℕ) \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
12		nn0sumshdiglemB	$⊢ ((a \in ℕ \land \frac{a - 1}{2} \in ℕ_{0}) \land y \in ℕ) \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$
13	12	expimpd	$⊢ (a \in ℕ \land \frac{a - 1}{2} \in ℕ_{0}) \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
14		nneom	$⊢ a \in ℕ \to (\frac{a}{2} \in ℕ \lor \frac{a - 1}{2} \in ℕ_{0})$
15	11 13 14	mpjaodan	$⊢ a \in ℕ \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
16		eqcom	$⊢ 1 = y + 1 \leftrightarrow y + 1 = 1$
17	16	a1i	$⊢ y \in ℕ \to (1 = y + 1 \leftrightarrow y + 1 = 1)$
18		nncn	$⊢ y \in ℕ \to y \in ℂ$
19		1cnd	$⊢ y \in ℕ \to 1 \in ℂ$
20	18 19 19	addlsub	$⊢ y \in ℕ \to (y + 1 = 1 \leftrightarrow y = 1 - 1)$
21		1m1e0	$⊢ 1 - 1 = 0$
22	21	a1i	$⊢ y \in ℕ \to 1 - 1 = 0$
23	22	eqeq2d	$⊢ y \in ℕ \to (y = 1 - 1 \leftrightarrow y = 0)$
24	17 20 23	3bitrd	$⊢ y \in ℕ \to (1 = y + 1 \leftrightarrow y = 0)$
25		oveq1	$⊢ y = 0 \to y + 1 = 0 + 1$
26	25	oveq2d	$⊢ y = 0 \to (0 ..^y + 1) = (0 ..^0 + 1)$
27		0p1e1	$⊢ 0 + 1 = 1$
28	27	oveq2i	$⊢ (0 ..^0 + 1) = (0 ..^1)$
29		fzo01	$⊢ (0 ..^1) = \{0\}$
30	28 29	eqtri	$⊢ (0 ..^0 + 1) = \{0\}$
31	26 30	eqtrdi	$⊢ y = 0 \to (0 ..^y + 1) = \{0\}$
32	31	sumeq1d	$⊢ y = 0 \to \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k} = \sum_{k \in \{0\}} (k digit (2) 0) 2^{k}$
33		0cn	$⊢ 0 \in ℂ$
34		oveq1	$⊢ k = 0 \to k digit (2) 0 = 0 digit (2) 0$
35		2nn	$⊢ 2 \in ℕ$
36		0z	$⊢ 0 \in ℤ$
37		dig0	$⊢ (2 \in ℕ \land 0 \in ℤ) \to 0 digit (2) 0 = 0$
38	35 36 37	mp2an	$⊢ 0 digit (2) 0 = 0$
39	34 38	eqtrdi	$⊢ k = 0 \to k digit (2) 0 = 0$
40		oveq2	$⊢ k = 0 \to 2^{k} = 2^{0}$
41		2cn	$⊢ 2 \in ℂ$
42		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
43	41 42	ax-mp	$⊢ 2^{0} = 1$
44	40 43	eqtrdi	$⊢ k = 0 \to 2^{k} = 1$
45	39 44	oveq12d	$⊢ k = 0 \to (k digit (2) 0) 2^{k} = 0 \cdot 1$
46		1re	$⊢ 1 \in ℝ$
47		mul02lem2	$⊢ 1 \in ℝ \to 0 \cdot 1 = 0$
48	46 47	ax-mp	$⊢ 0 \cdot 1 = 0$
49	45 48	eqtrdi	$⊢ k = 0 \to (k digit (2) 0) 2^{k} = 0$
50	49	sumsn	$⊢ (0 \in ℂ \land 0 \in ℂ) \to \sum_{k \in \{0\}} (k digit (2) 0) 2^{k} = 0$
51	33 33 50	mp2an	$⊢ \sum_{k \in \{0\}} (k digit (2) 0) 2^{k} = 0$
52	32 51	eqtr2di	$⊢ y = 0 \to 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k}$
53	24 52	syl6bi	$⊢ y \in ℕ \to (1 = y + 1 \to 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k})$
54	53	adantl	$⊢ (a = 0 \land y \in ℕ) \to (1 = y + 1 \to 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k})$
55		fveq2	$⊢ a = 0 \to #_{b(a)=#_{b} (0)}$
56		blen0	$⊢ #_{b(0)=1}$
57	55 56	eqtrdi	$⊢ a = 0 \to #_{b(a)=1}$
58	57	eqeq1d	$⊢ a = 0 \to (#_{b(a)=y + 1\leftrightarrow1 = y + 1})$
59		id	$⊢ a = 0 \to a = 0$
60		oveq2	$⊢ a = 0 \to k digit (2) a = k digit (2) 0$
61	60	oveq1d	$⊢ a = 0 \to (k digit (2) a) 2^{k} = (k digit (2) 0) 2^{k}$
62	61	sumeq2sdv	$⊢ a = 0 \to \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k} = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k}$
63	59 62	eqeq12d	$⊢ a = 0 \to (a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k} \leftrightarrow 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k})$
64	58 63	imbi12d	$⊢ a = 0 \to ((#_{b(a)=y + 1\toa = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}\leftrightarrow(1 = y + 1 \to 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k})}))$
65	64	adantr	$⊢ (a = 0 \land y \in ℕ) \to ((#_{b(a)=y + 1\toa = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}\leftrightarrow(1 = y + 1 \to 0 = \sum_{k \in (0 ..^y + 1)} (k digit (2) 0) 2^{k})}))$
66	54 65	mpbird	$⊢ (a = 0 \land y \in ℕ) \to (#_{b(a)=y + 1\toa = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}})$
67	66	a1d	$⊢ (a = 0 \land y \in ℕ) \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$
68	67	expimpd	$⊢ a = 0 \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
69	15 68	jaoi	$⊢ (a \in ℕ \lor a = 0) \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
70	9 69	sylbi	$⊢ a \in ℕ_{0} \to ((y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
71	70	com12	$⊢ (y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(a \in ℕ_{0} \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))}))$
72	71	ralrimiv	$⊢ (y \in ℕ \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to\forall a \in ℕ_{0} (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$
73	72	ex	$⊢ y \in ℕ \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to\forall a \in ℕ_{0} (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$
74	8 73	biimtrid	$⊢ y \in ℕ \to (\forall a \in ℕ_{0} (#_{b(a)=y\toa = \sum_{k \in (0 ..^y)} (k digit (2) a) 2^{k}\to\forall a \in ℕ_{0} (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$

Metamath Proof Explorer

Theorem nn0sumshdiglem1

Proof