df-seq1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seq1 6308

Description: Define a general-purpose operation that builds an recursive sequence (i.e. a function on the natural numbers

) whose value at an index is a function of its previous value and the value of an input sequence at that index. This definition is complicated, but fortunately it is not intended to be used directly. Instead, the only purpose of this definition is to provide us with an object that has the properties expressed by seq11 6317 and seq1p1 6318. Typically, those are the main theorems that would be used in practice.

The first operand is the operation that is applied to the previous value and the value of the input sequence (second operand). For example, for the operation , an input sequence with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. means "the sum of F(n) from n = 1 to infinity is 2." Since limits are unique (climuni 7099), then by eusn 2446 and unisn 2517 the "sum of F(n) from n = 1 to infinity" can be expressed as (provided the sequence converges) and evaluates to 2 in this example.

Internally, we define a recursive function whose values are ordered pairs starting at . The first member of the ordered pair is a counter used to select the appropriate value of the input sequence . The first constructs this function on , and the converse of the second maps to .

This definition has its roots in a series of theorems starting at om2uz0 6295, originally proved by Raph Levien for use with df-exp 6569 and later generalized for arbitrary recursive sequences. The related definitions df-seq0 6534 and df-seqz 6533 build recursive sequences on and general upper integer sets respectively. Definition df-sum 6980 extracts the summation values from partial (finite) and complete (infinite) series.

**Assertion**
Ref	Expression
df-seq1	$/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-seq1**
Step	Hyp	Ref	Expression
1		cseq1 6307	. 2
2		vh	. . . . 5
3	2	cv 955	. . . 4
4		vx	. . . . . . . 8
5	4	cv 955	. . . . . . 7
6		cn 5296	. . . . . . 7
7	5, 6	wcel 958	. . . . . 6
8		vy	. . . . . . . 8
9	8	cv 955	. . . . . . 7
10		vw	. . . . . . . . . . . . . 14
11	10	cv 955	. . . . . . . . . . . . 13
12		vz	. . . . . . . . . . . . . . . . 17
13	12	cv 955	. . . . . . . . . . . . . . . 16
14		c1st 4077	. . . . . . . . . . . . . . . 16
15	13, 14	cfv 3182	. . . . . . . . . . . . . . 15
16		c1 5235	. . . . . . . . . . . . . . 15
17		caddc 5237	. . . . . . . . . . . . . . 15
18	15, 16, 17	co 3963	. . . . . . . . . . . . . 14
19		c2nd 4078	. . . . . . . . . . . . . . . 16
20	13, 19	cfv 3182	. . . . . . . . . . . . . . 15
21		vg	. . . . . . . . . . . . . . . . 17
22	21	cv 955	. . . . . . . . . . . . . . . 16
23	18, 22	cfv 3182	. . . . . . . . . . . . . . 15
24		vf	. . . . . . . . . . . . . . . 16
25	24	cv 955	. . . . . . . . . . . . . . 15
26	20, 23, 25	co 3963	. . . . . . . . . . . . . 14
27	18, 26	cop 2411	. . . . . . . . . . . . 13
28	11, 27	wceq 956	. . . . . . . . . . . 12
29	28, 12, 10	copab 2666	. . . . . . . . . . 11
30	16, 22	cfv 3182	. . . . . . . . . . . 12
31	16, 30	cop 2411	. . . . . . . . . . 11
32	29, 31	crdg 3931	. . . . . . . . . 10
33	13, 16, 17	co 3963	. . . . . . . . . . . . . . 15
34	11, 33	wceq 956	. . . . . . . . . . . . . 14
35	34, 12, 10	copab 2666	. . . . . . . . . . . . 13
36	35, 16	crdg 3931	. . . . . . . . . . . 12
37		com 3131	. . . . . . . . . . . 12
38	36, 37	cres 3172	. . . . . . . . . . 11
39	38	ccnv 3169	. . . . . . . . . 10
40	32, 39	ccom 3174	. . . . . . . . 9
41	5, 40	cfv 3182	. . . . . . . 8
42	41, 19	cfv 3182	. . . . . . 7
43	9, 42	wceq 956	. . . . . 6
44	7, 43	wa 223	. . . . 5 $/\$
45	44, 4, 8	copab 2666	. . . 4 $/\$
46	3, 45	wceq 956	. . 3 $/\$
47	46, 24, 21, 2	copab2 3964	. 2 $/\$
48	1, 47	wceq 956	1 $/\$

Colors of variables: wff set class

This definition is referenced by: seq1val 6312