df-seq1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seq1 6673

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 6682 and seq1p1 6683. 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 7302), then by eusn 2507 and unisn 2583 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 om2uz0i 6658, originally proved by Raph Levien for use with df-exp 6764 and later generalized for arbitrary recursive sequences. The related definitions df-seq0 6729 and df-seqz 6728 build recursive sequences on and general upper integer sets respectively. Definition df-sum 7183 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 6672	. 2
2		vh	. . . . 5
3	2	cv 991	. . . 4
4		vx	. . . . . . . 8
5	4	cv 991	. . . . . . 7
6		cn 5450	. . . . . . 7
7	5, 6	wcel 994	. . . . . 6
8		vy	. . . . . . . 8
9	8	cv 991	. . . . . . 7
10		vw	. . . . . . . . . . . . . 14
11	10	cv 991	. . . . . . . . . . . . 13
12		vz	. . . . . . . . . . . . . . . . 17
13	12	cv 991	. . . . . . . . . . . . . . . 16
14		c1st 4138	. . . . . . . . . . . . . . . 16
15	13, 14	cfv 3263	. . . . . . . . . . . . . . 15
16		c1 5389	. . . . . . . . . . . . . . 15
17		caddc 5391	. . . . . . . . . . . . . . 15
18	15, 16, 17	co 4021	. . . . . . . . . . . . . 14
19		c2nd 4139	. . . . . . . . . . . . . . . 16
20	13, 19	cfv 3263	. . . . . . . . . . . . . . 15
21		vg	. . . . . . . . . . . . . . . . 17
22	21	cv 991	. . . . . . . . . . . . . . . 16
23	18, 22	cfv 3263	. . . . . . . . . . . . . . 15
24		vf	. . . . . . . . . . . . . . . 16
25	24	cv 991	. . . . . . . . . . . . . . 15
26	20, 23, 25	co 4021	. . . . . . . . . . . . . 14
27	18, 26	cop 2469	. . . . . . . . . . . . 13
28	11, 27	wceq 992	. . . . . . . . . . . 12
29	28, 12, 10	copab 2740	. . . . . . . . . . 11
30	16, 22	cfv 3263	. . . . . . . . . . . 12
31	16, 30	cop 2469	. . . . . . . . . . 11
32	29, 31	crdg 4232	. . . . . . . . . 10
33	13, 16, 17	co 4021	. . . . . . . . . . . . . . 15
34	11, 33	wceq 992	. . . . . . . . . . . . . 14
35	34, 12, 10	copab 2740	. . . . . . . . . . . . 13
36	35, 16	crdg 4232	. . . . . . . . . . . 12
37		com 3218	. . . . . . . . . . . 12
38	36, 37	cres 3253	. . . . . . . . . . 11
39	38	ccnv 3250	. . . . . . . . . 10
40	32, 39	ccom 3255	. . . . . . . . 9
41	5, 40	cfv 3263	. . . . . . . 8
42	41, 19	cfv 3263	. . . . . . 7
43	9, 42	wceq 992	. . . . . 6
44	7, 43	wa 221	. . . . 5 $/\$
45	44, 4, 8	copab 2740	. . . 4 $/\$
46	3, 45	wceq 992	. . 3 $/\$
47	46, 24, 21, 2	copab2 4022	. 2 $/\$
48	1, 47	wceq 992	1 $/\$

Colors of variables: wff set class

This definition is referenced by: seq1val 6677