Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fib Structured version   Visualization version   Unicode version
Definition df-fib 30459
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 = ( <" 0 1 ">seqstr ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
Detailed syntax breakdown of Definition df-fib
StepHypRef Expression
1 cfib 30458 . 2 class Fibci
2 cc0 9936 . . . 4 class 0
3 c1 9937 . . . 4 class 1
42, 3cs2 13586 . . 3 class <" 0 1 ">
5 vw . . . 4 setvar w
6 cn0 11292 . . . . . 6 class NN0
76cword 13291 . . . . 5 class Word NN0
8 chash 13117 . . . . . . 7 class #
98ccnv 5113 . . . . . 6 class `' #
10 c2 11070 . . . . . . 7 class 2
11 cuz 11687 . . . . . . 7 class ZZ>=
1210, 11cfv 5888 . . . . . 6 class ( ZZ>= ` 2 )
139, 12cima 5117 . . . . 5 class ( `' # " ( ZZ>= ` 2 ) )
147, 13cin 3573 . . . 4 class (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) )
155cv 1482 . . . . . . . 8 class w
1615, 8cfv 5888 . . . . . . 7 class ( # ` w )
17 cmin 10266 . . . . . . 7 class -
1816, 10, 17co 6650 . . . . . 6 class ( ( # ` w ) - 2 )
1918, 15cfv 5888 . . . . 5 class ( w ` ( ( # ` w ) - 2 ) )
2016, 3, 17co 6650 . . . . . 6 class ( ( # ` w ) - 1 )
2120, 15cfv 5888 . . . . 5 class ( w ` ( ( # ` w ) - 1 ) )
22 caddc 9939 . . . . 5 class +
2319, 21, 22co 6650 . . . 4 class ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) )
245, 14, 23cmpt 4729 . . 3 class ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) )
25 csseq 30445 . . 3 class seqstr
264, 24, 25co 6650 . 2 class ( <" 0 1 ">seqstr ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
271, 26wceq 1483 1 wff Fibci = ( <" 0 1 ">seqstr ( w e. (Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  fib0  30461  fib1  30462  fibp1  30463
  Copyright terms: Public domain W3C validator