Metamath Proof Explorer

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 ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 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 
 |-  w
6 cn0 
 |-  NN0
7 6 cword 
 |-  Word NN0
8 chash 
 |-  #
9 8 ccnv 
 |-  `' #
10 cuz 
 |-  ZZ>=
11 c2 
 |-  2
12 11 10 cfv 
 |-  ( ZZ>= ` 2 )
13 9 12 cima 
 |-  ( `' # " ( ZZ>= ` 2 ) )
14 7 13 cin 
 |-  ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) )
15 5 cv 
 |-  w
16 15 8 cfv 
 |-  ( # ` w )
17 cmin 
 |-  -
18 16 11 17 co 
 |-  ( ( # ` w ) - 2 )
19 18 15 cfv 
 |-  ( w ` ( ( # ` w ) - 2 ) )
20 caddc 
 |-  +
21 16 2 17 co 
 |-  ( ( # ` w ) - 1 )
22 21 15 cfv 
 |-  ( w ` ( ( # ` w ) - 1 ) )
23 19 22 20 co 
 |-  ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) )
24 5 14 23 cmpt 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) )
25 3 24 4 co 
 |-  ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
26 0 25 wceq 
 |-  Fibci = ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )