Definition df-fib

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfib	⊢ Fibci
1		cc0	⊢ 0
2		c1	⊢ 1
3	1 2	cs2	⊢ ⟨“ 0 1 ”⟩
4		csseq	⊢ seqstr
5		vw	⊢ 𝑤
6		cn0	⊢ ℕ0
7	6	cword	⊢ Word ℕ0
8		chash	⊢ ♯
9	8	ccnv	⊢ ◡ ♯
10		cuz	⊢ ℤ≥
11		c2	⊢ 2
12	11 10	cfv	⊢ ( ℤ≥ ‘ 2 )
13	9 12	cima	⊢ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) )
14	7 13	cin	⊢ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) )
15	5	cv	⊢ 𝑤
16	15 8	cfv	⊢ ( ♯ ‘ 𝑤 )
17		cmin	⊢ −
18	16 11 17	co	⊢ ( ( ♯ ‘ 𝑤 ) − 2 )
19	18 15	cfv	⊢ ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) )
20		caddc	⊢ +
21	16 2 17	co	⊢ ( ( ♯ ‘ 𝑤 ) − 1 )
22	21 15	cfv	⊢ ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) )
23	19 22 20	co	⊢ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) )
24	5 14 23	cmpt	⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) )
25	3 24 4	co	⊢ ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
26	0 25	wceq	⊢ Fibci = ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )