Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-seq 4661

Description: Define a general-purpose operation that builds an infinite 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 seq1 4670 and seqsuc 4671. 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 4884), then by eusn 1913 and unisn 1932 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, a recursive function is defined 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 .

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

Distinct variable group(s):

**Detailed syntax breakdown of Definition df-seq**
Step	Hyp	Ref	Expression
1		cseq 4660	. 2
2		vh	. . . . 5
3	2	cv 1089	. . . 4
4		vx	. . . . . . . 8
5	4	cv 1089	. . . . . . 7
6		cn 4093	. . . . . . 7
7	5, 6	wcel 1092	. . . . . 6
8		vy	. . . . . . . 8
9	8	cv 1089	. . . . . . 7
10		vw	. . . . . . . . . . . . . 14
11	10	cv 1089	. . . . . . . . . . . . 13
12		vz	. . . . . . . . . . . . . . . . 17
13	12	cv 1089	. . . . . . . . . . . . . . . 16
14		c1st 3085	. . . . . . . . . . . . . . . 16
15	13, 14	cfv 2422	. . . . . . . . . . . . . . 15
16		c1 4029	. . . . . . . . . . . . . . 15
17		caddc 4031	. . . . . . . . . . . . . . 15
18	15, 16, 17	co 3001	. . . . . . . . . . . . . 14
19		c2nd 3086	. . . . . . . . . . . . . . . 16
20	13, 19	cfv 2422	. . . . . . . . . . . . . . 15
21		vg	. . . . . . . . . . . . . . . . 17
22	21	cv 1089	. . . . . . . . . . . . . . . 16
23	18, 22	cfv 2422	. . . . . . . . . . . . . . 15
24		vf	. . . . . . . . . . . . . . . 16
25	24	cv 1089	. . . . . . . . . . . . . . 15
26	20, 23, 25	co 3001	. . . . . . . . . . . . . 14
27	18, 26	cop 1810	. . . . . . . . . . . . 13
28	11, 27	wceq 1091	. . . . . . . . . . . 12
29	28, 12, 10	copab 2055	. . . . . . . . . . 11
30	16, 22	cfv 2422	. . . . . . . . . . . 12
31	16, 30	cop 1810	. . . . . . . . . . 11
32	29, 31	crdg 2969	. . . . . . . . . 10
33	13, 16, 17	co 3001	. . . . . . . . . . . . . . 15
34	11, 33	wceq 1091	. . . . . . . . . . . . . 14
35	34, 12, 10	copab 2055	. . . . . . . . . . . . 13
36	35, 16	crdg 2969	. . . . . . . . . . . 12
37		com 2372	. . . . . . . . . . . 12
38	36, 37	cres 2412	. . . . . . . . . . 11
39	38	ccnv 2409	. . . . . . . . . 10
40	32, 39	ccom 2414	. . . . . . . . 9
41	5, 40	cfv 2422	. . . . . . . 8
42	41, 19	cfv 2422	. . . . . . 7
43	9, 42	wceq 1091	. . . . . 6
44	7, 43	wa 196	. . . . 5 $/\$
45	44, 4, 8	copab 2055	. . . 4 $/\$
46	3, 45	wceq 1091	. . 3 $/\$
47	46, 24, 21, 2	copab2 3002	. 2 $/\$
48	1, 47	wceq 1091	1 $/\$

Colors of variables: wff set class

This definition is referenced by: seqval 4665

metamath.org