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 F with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence ( + seqF) with values 1, 3/2, 7/4, 15/8,.., so that (( + seqF) ‘1) = 1, (( + seqF) ‘2) = 3/2, etc. In other words, ( + seqF) transforms a sequence F into an infinite series. ( + seqF) ⇝ 2 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 ∪{x∣( + seqF) ⇝ x} (provided the sequence converges) and evaluates to 2 in this example.

Internally, a recursive function is defined whose values are ordered pairs starting at ⟨1, (g ‘1)⟩. The first member of the ordered pair is a counter used to select the appropriate value of the input sequence g. The first rec constructs this function on ω, and the converse of the second rec maps ℕ to ω.

Assertion

Ref	Expression
df-seq	⊢ seq = {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}

Distinct variable group(s):   x,y,z,w,f,g,h

Detailed syntax breakdown of Definition df-seq

Step	Hyp	Ref	Expression
1		cseq 4660	. 2 class seq
2		vh	. . . . 5 set h
3	2	cv 1089	. . . 4 class h
4		vx	. . . . . . . 8 set x
5	4	cv 1089	. . . . . . 7 class x
6		cn 4093	. . . . . . 7 class ℕ
7	5, 6	wcel 1092	. . . . . 6 wff x ∈ ℕ
8		vy	. . . . . . . 8 set y
9	8	cv 1089	. . . . . . 7 class y
10		vw	. . . . . . . . . . . . . 14 set w
11	10	cv 1089	. . . . . . . . . . . . 13 class w
12		vz	. . . . . . . . . . . . . . . . 17 set z
13	12	cv 1089	. . . . . . . . . . . . . . . 16 class z
14		c1st 3085	. . . . . . . . . . . . . . . 16 class 1st
15	13, 14	cfv 2422	. . . . . . . . . . . . . . 15 class (1st ‘z)
16		c1 4029	. . . . . . . . . . . . . . 15 class 1
17		caddc 4031	. . . . . . . . . . . . . . 15 class +
18	15, 16, 17	co 3001	. . . . . . . . . . . . . 14 class ((1st ‘z) + 1)
19		c2nd 3086	. . . . . . . . . . . . . . . 16 class 2nd
20	13, 19	cfv 2422	. . . . . . . . . . . . . . 15 class (2nd ‘z)
21		vg	. . . . . . . . . . . . . . . . 17 set g
22	21	cv 1089	. . . . . . . . . . . . . . . 16 class g
23	18, 22	cfv 2422	. . . . . . . . . . . . . . 15 class (g ‘((1st ‘z) + 1))
24		vf	. . . . . . . . . . . . . . . 16 set f
25	24	cv 1089	. . . . . . . . . . . . . . 15 class f
26	20, 23, 25	co 3001	. . . . . . . . . . . . . 14 class ((2nd ‘z)f(g ‘((1st ‘z) + 1)))
27	18, 26	cop 1810	. . . . . . . . . . . . 13 class ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩
28	11, 27	wceq 1091	. . . . . . . . . . . 12 wff w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩
29	28, 12, 10	copab 2055	. . . . . . . . . . 11 class {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}
30	16, 22	cfv 2422	. . . . . . . . . . . 12 class (g ‘1)
31	16, 30	cop 1810	. . . . . . . . . . 11 class ⟨1, (g ‘1)⟩
32	29, 31	crdg 2969	. . . . . . . . . 10 class rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩)
33	13, 16, 17	co 3001	. . . . . . . . . . . . . . 15 class (z + 1)
34	11, 33	wceq 1091	. . . . . . . . . . . . . 14 wff w = (z + 1)
35	34, 12, 10	copab 2055	. . . . . . . . . . . . 13 class {⟨z, w⟩∣w = (z + 1)}
36	35, 16	crdg 2969	. . . . . . . . . . . 12 class rec({⟨z, w⟩∣w = (z + 1)}, 1)
37		com 2372	. . . . . . . . . . . 12 class ω
38	36, 37	cres 2412	. . . . . . . . . . 11 class (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
39	38	ccnv 2409	. . . . . . . . . 10 class ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
40	32, 39	ccom 2414	. . . . . . . . 9 class (rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω))
41	5, 40	cfv 2422	. . . . . . . 8 class ((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)
42	41, 19	cfv 2422	. . . . . . 7 class (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x))
43	9, 42	wceq 1091	. . . . . 6 wff y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x))
44	7, 43	wa 196	. . . . 5 wff (x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))
45	44, 4, 8	copab 2055	. . . 4 class {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}
46	3, 45	wceq 1091	. . 3 wff h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}
47	46, 24, 21, 2	copab2 3002	. 2 class {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}
48	1, 47	wceq 1091	1 wff seq = {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}

This definition is referenced by:  seqval 4665

metamath.org