Definition df-fib 32264

Description: Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)

Assertion

Ref	Expression
df-fib	⊢ Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))

Detailed syntax breakdown of Definition df-fib

Step	Hyp	Ref	Expression
1		cfib 32263	. 2 class Fibci
2		cc0 10802	. . . 4 class 0
3		c1 10803	. . . 4 class 1
4	2, 3	cs2 14482	. . 3 class ⟨“01”⟩
5		vw	. . . 4 setvar 𝑤
6		cn0 12163	. . . . . 6 class ℕ0
7	6	cword 14145	. . . . 5 class Word ℕ0
8		chash 13972	. . . . . . 7 class ♯
9	8	ccnv 5579	. . . . . 6 class ◡♯
10		c2 11958	. . . . . . 7 class 2
11		cuz 12511	. . . . . . 7 class ℤ≥
12	10, 11	cfv 6418	. . . . . 6 class (ℤ≥‘2)
13	9, 12	cima 5583	. . . . 5 class (◡♯ “ (ℤ≥‘2))
14	7, 13	cin 3882	. . . 4 class (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2)))
15	5	cv 1538	. . . . . . . 8 class 𝑤
16	15, 8	cfv 6418	. . . . . . 7 class (♯‘𝑤)
17		cmin 11135	. . . . . . 7 class −
18	16, 10, 17	co 7255	. . . . . 6 class ((♯‘𝑤) − 2)
19	18, 15	cfv 6418	. . . . 5 class (𝑤‘((♯‘𝑤) − 2))
20	16, 3, 17	co 7255	. . . . . 6 class ((♯‘𝑤) − 1)
21	20, 15	cfv 6418	. . . . 5 class (𝑤‘((♯‘𝑤) − 1))
22		caddc 10805	. . . . 5 class +
23	19, 21, 22	co 7255	. . . 4 class ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))
24	5, 14, 23	cmpt 5153	. . 3 class (𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))
25		csseq 32250	. . 3 class seqstr
26	4, 24, 25	co 7255	. 2 class (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
27	1, 26	wceq 1539	1 wff Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))

This definition is referenced by:  fib0  32266  fib1  32267  fibp1  32268