Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fib Structured version   Visualization version   GIF version

Definition df-fib 29592
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
StepHypRef Expression
1 cfib 29591 . 2 class Fibci
2 cc0 9792 . . . 4 class 0
3 c1 9793 . . . 4 class 1
42, 3cs2 13383 . . 3 class ⟨“01”⟩
5 vw . . . 4 setvar 𝑤
6 cn0 11139 . . . . . 6 class 0
76cword 13092 . . . . 5 class Word ℕ0
8 chash 12934 . . . . . . 7 class #
98ccnv 5027 . . . . . 6 class #
10 c2 10917 . . . . . . 7 class 2
11 cuz 11519 . . . . . . 7 class
1210, 11cfv 5790 . . . . . 6 class (ℤ‘2)
139, 12cima 5031 . . . . 5 class (# “ (ℤ‘2))
147, 13cin 3538 . . . 4 class (Word ℕ0 ∩ (# “ (ℤ‘2)))
155cv 1473 . . . . . . . 8 class 𝑤
1615, 8cfv 5790 . . . . . . 7 class (#‘𝑤)
17 cmin 10117 . . . . . . 7 class
1816, 10, 17co 6527 . . . . . 6 class ((#‘𝑤) − 2)
1918, 15cfv 5790 . . . . 5 class (𝑤‘((#‘𝑤) − 2))
2016, 3, 17co 6527 . . . . . 6 class ((#‘𝑤) − 1)
2120, 15cfv 5790 . . . . 5 class (𝑤‘((#‘𝑤) − 1))
22 caddc 9795 . . . . 5 class +
2319, 21, 22co 6527 . . . 4 class ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))
245, 14, 23cmpt 4637 . . 3 class (𝑤 ∈ (Word ℕ0 ∩ (# “ (ℤ‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))
25 csseq 29578 . . 3 class seqstr
264, 24, 25co 6527 . 2 class (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (# “ (ℤ‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))
271, 26wceq 1474 1 wff Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (# “ (ℤ‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))
Colors of variables: wff setvar class
This definition is referenced by:  fib0  29594  fib1  29595  fibp1  29596
  Copyright terms: Public domain W3C validator