df-seqz - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seqz 7776

Description: Define a recursive sequence builder operation that starts at an arbitrary integer index. See seqz1 7790 and seqzp1 7791 for its initial and successor values. Theorems seq0seqz 7785 and seq1seqz 7784 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 7774	. 2
2		vh	. . . . 5
3	2	cv 1297	. . . 4
4		vx	. . . . . . . . 9
5	4	cv 1297	. . . . . . . 8
6		c2nd 5019	. . . . . . . 8
7	5, 6	cfv 3998	. . . . . . 7
8		vg	. . . . . . . . 9
9	8	cv 1297	. . . . . . . 8
10		c1 6387	. . . . . . . . 9
11		c1st 5018	. . . . . . . . . 10
12	5, 11	cfv 3998	. . . . . . . . 9
13		cmin 6445	. . . . . . . . 9
14	10, 12, 13	co 4884	. . . . . . . 8
15		cshi 7753	. . . . . . . 8
16	9, 14, 15	co 4884	. . . . . . 7
17		cseq1 7720	. . . . . . 7
18	7, 16, 17	co 4884	. . . . . 6
19	12, 10, 13	co 4884	. . . . . 6
20	18, 19, 15	co 4884	. . . . 5
21		vk	. . . . . . . 8
22	21	cv 1297	. . . . . . 7
23		cle 6448	. . . . . . 7
24	12, 22, 23	wbr 3338	. . . . . 6
25		cz 6451	. . . . . 6
26	24, 21, 25	crab 2108	. . . . 5
27	20, 26	cres 3988	. . . 4
28	3, 27	wceq 1298	. . 3
29	28, 4, 8, 2	copab2 4885	. 2
30	1, 29	wceq 1298	1

Colors of variables: wff set class

This definition is referenced by: seqzfval 7780