Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem seqzval2t 6485

Description: Value of the arbitrary-based recursive sequence builder operation.

Hypotheses

Ref	Expression
seq0val.1
seq0val.2

Assertion

Ref	Expression
seqzval2t

---

Proof of Theorem seqzval2t

Step	Hyp	Ref	Expression
1		zcnt 6087	. . . . 5
2		oprex 3968	. . . . . 6
3		oprex 3968	. . . . . . 7
4	3	shftvalt 6283	. . . . . 6
5	2, 4	mpan 693	. . . . 5
6	1, 5	syl 10	. . . 4
7	6	3ad2ant2 799	. . 3
8		zcnt 6087	. . . . . . . 8
9		negclt 5340	. . . . . . . . . 10
10		ax1cn 5241	. . . . . . . . . . 11
11		seq0val.2	. . . . . . . . . . . 12
12	11	2shft 6289	. . . . . . . . . . 11
13	10, 12	mpan2 694	. . . . . . . . . 10
14	9, 13	syl 10	. . . . . . . . 9
15		axaddcom 5247	. . . . . . . . . . . . 13
16	10, 15	mpan2 694	. . . . . . . . . . . 12
17	9, 16	syl 10	. . . . . . . . . . 11
18		negsubt 5354	. . . . . . . . . . . 12
19	10, 18	mpan 693	. . . . . . . . . . 11
20	17, 19	eqtrd 1499	. . . . . . . . . 10
21	20	opreq2d 3961	. . . . . . . . 9
22	14, 21	eqtrd 1499	. . . . . . . 8
23	8, 22	syl 10	. . . . . . 7
24	23	opreq2d 3961	. . . . . 6
25	24	fveq1d 3711	. . . . 5
26	25	3ad2ant1 798	. . . 4
27		subsubt 5434	. . . . . . . . . 10
28	10, 27	mp3an3 902	. . . . . . . . 9
29	28, 1, 8	syl2an 454	. . . . . . . 8
30	29	ancoms 436	. . . . . . 7
31	30	3adant3 797	. . . . . 6
32		znn0sub2t 6126	. . . . . . 7
33		nn0p1nnt 6122	. . . . . . 7
34	32, 33	syl 10	. . . . . 6
35	31, 34	eqeltrd 1540	. . . . 5
36		seq0val.1	. . . . . 6
37		oprex 3968	. . . . . 6
38	36, 37	seq1seq02t 6475	. . . . 5
39	35, 38	syl 10	. . . 4
40	26, 39	eqtr3d 1501	. . 3
41		subclt 5339	. . . . . . . . 9
42		subclt 5339	. . . . . . . . . 10
43	10, 42	mpan2 694	. . . . . . . . 9
44	41, 43	sylan2 451	. . . . . . . 8
45		oprex 3968	. . . . . . . . . 10
46	45	shftvalt 6283	. . . . . . . . 9
47	10, 46	mpan 693	. . . . . . . 8
48	44, 47	syl 10	. . . . . . 7
49		nnncant 5438	. . . . . . . . 9
50	10, 49	mp3an3 902	. . . . . . . 8
51	50	fveq2d 3713	. . . . . . 7
52	48, 51	eqtrd 1499	. . . . . 6
53	52	ancoms 436	. . . . 5
54	53, 8, 1	syl2an 454	. . . 4
55	54	3adant3 797	. . 3
56	7, 40, 55	3eqtrd 1503	. 2