df-seq1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seq1 6253

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 6262 and seq1p1 6263. 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 7044), then by eusn 2442 and unisn 2512 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 6240, originally proved by Raph Levien for use with df-exp 6509 and later generalized for arbitrary recursive sequences. The related definitions df-seq0 6474 and df-seqz 6473 build recursive sequences on and general upper integer sets respectively. Definition df-sum 6926 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 6252	. 2
2		vh	. . . . 5
3	2	cv 953	. . . 4
4		vx	. . . . . . . 8
5	4	cv 953	. . . . . . 7
6		cn 5276	. . . . . . 7
7	5, 6	wcel 956	. . . . . 6
8		vy	. . . . . . . 8
9	8	cv 953	. . . . . . 7
10		vw	. . . . . . . . . . . . . 14
11	10	cv 953	. . . . . . . . . . . . 13
12		vz	. . . . . . . . . . . . . . . . 17
13	12	cv 953	. . . . . . . . . . . . . . . 16
14		c1st 4067	. . . . . . . . . . . . . . . 16
15	13, 14	cfv 3177	. . . . . . . . . . . . . . 15
16		c1 5215	. . . . . . . . . . . . . . 15
17		caddc 5217	. . . . . . . . . . . . . . 15
18	15, 16, 17	co 3954	. . . . . . . . . . . . . 14
19		c2nd 4068	. . . . . . . . . . . . . . . 16
20	13, 19	cfv 3177	. . . . . . . . . . . . . . 15
21		vg	. . . . . . . . . . . . . . . . 17
22	21	cv 953	. . . . . . . . . . . . . . . 16
23	18, 22	cfv 3177	. . . . . . . . . . . . . . 15
24		vf	. . . . . . . . . . . . . . . 16
25	24	cv 953	. . . . . . . . . . . . . . 15
26	20, 23, 25	co 3954	. . . . . . . . . . . . . 14
27	18, 26	cop 2407	. . . . . . . . . . . . 13
28	11, 27	wceq 954	. . . . . . . . . . . 12
29	28, 12, 10	copab 2661	. . . . . . . . . . 11
30	16, 22	cfv 3177	. . . . . . . . . . . 12
31	16, 30	cop 2407	. . . . . . . . . . 11
32	29, 31	crdg 3922	. . . . . . . . . 10
33	13, 16, 17	co 3954	. . . . . . . . . . . . . . 15
34	11, 33	wceq 954	. . . . . . . . . . . . . 14
35	34, 12, 10	copab 2661	. . . . . . . . . . . . 13
36	35, 16	crdg 3922	. . . . . . . . . . . 12
37		com 3126	. . . . . . . . . . . 12
38	36, 37	cres 3167	. . . . . . . . . . 11
39	38	ccnv 3164	. . . . . . . . . 10
40	32, 39	ccom 3169	. . . . . . . . 9
41	5, 40	cfv 3177	. . . . . . . 8
42	41, 19	cfv 3177	. . . . . . 7
43	9, 42	wceq 954	. . . . . 6
44	7, 43	wa 223	. . . . 5 $/\$
45	44, 4, 8	copab 2661	. . . 4 $/\$
46	3, 45	wceq 954	. . 3 $/\$
47	46, 24, 21, 2	copab2 3955	. 2 $/\$
48	1, 47	wceq 954	1 $/\$

Colors of variables: wff set class

This definition is referenced by: seq1val 6257