df-seqz - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seqz 6483

Description: Define a recursive sequence builder operation that starts at an arbitrary integer index. See seqz1 6497 and seqzp1 6498 for its initial and successor values. Theorems seq0seqz 6492 and seq1seqz 6491 derive the 0-based

and the 1-based

as special cases.

**Assertion**
Ref	Expression
df-seqz

Distinct variable group:

**Detailed syntax breakdown of Definition df-seqz**
Step	Hyp	Ref	Expression
1		cseqz 6481	. 2
2		vh	. . . . 5
3	2	cv 954	. . . 4
4		vx	. . . . . . . . 9
5	4	cv 954	. . . . . . . 8
6		c2nd 4075	. . . . . . . 8
7	5, 6	cfv 3179	. . . . . . 7
8		vg	. . . . . . . . 9
9	8	cv 954	. . . . . . . 8
10		c1 5222	. . . . . . . . 9
11		c1st 4074	. . . . . . . . . 10
12	5, 11	cfv 3179	. . . . . . . . 9
13		cmin 5279	. . . . . . . . 9
14	10, 12, 13	co 3960	. . . . . . . 8
15		cshi 6295	. . . . . . . 8
16	9, 14, 15	co 3960	. . . . . . 7
17		cseq1 6262	. . . . . . 7
18	7, 16, 17	co 3960	. . . . . 6
19	12, 10, 13	co 3960	. . . . . 6
20	18, 19, 15	co 3960	. . . . 5
21		vk	. . . . . . . 8
22	21	cv 954	. . . . . . 7
23		cle 5282	. . . . . . 7
24	12, 22, 23	wbr 2616	. . . . . 6
25		cz 5285	. . . . . 6
26	24, 21, 25	crab 1647	. . . . 5
27	20, 26	cres 3169	. . . 4
28	3, 27	wceq 955	. . 3
29	28, 4, 8, 2	copab2 3961	. 2
30	1, 29	wceq 955	1

Colors of variables: wff set class

This definition is referenced by: seqzfval 6487