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 30799
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 30798 . 2 class Fibci
2 cc0 10138 . . . 4 class 0
3 c1 10139 . . . 4 class 1
42, 3cs2 13795 . . 3 class ⟨“01”⟩
5 vw . . . 4 setvar 𝑤
6 cn0 11494 . . . . . 6 class 0
76cword 13487 . . . . 5 class Word ℕ0
8 chash 13321 . . . . . . 7 class
98ccnv 5248 . . . . . 6 class
10 c2 11272 . . . . . . 7 class 2
11 cuz 11888 . . . . . . 7 class
1210, 11cfv 6031 . . . . . 6 class (ℤ‘2)
139, 12cima 5252 . . . . 5 class (♯ “ (ℤ‘2))
147, 13cin 3722 . . . 4 class (Word ℕ0 ∩ (♯ “ (ℤ‘2)))
155cv 1630 . . . . . . . 8 class 𝑤
1615, 8cfv 6031 . . . . . . 7 class (♯‘𝑤)
17 cmin 10468 . . . . . . 7 class
1816, 10, 17co 6793 . . . . . 6 class ((♯‘𝑤) − 2)
1918, 15cfv 6031 . . . . 5 class (𝑤‘((♯‘𝑤) − 2))
2016, 3, 17co 6793 . . . . . 6 class ((♯‘𝑤) − 1)
2120, 15cfv 6031 . . . . 5 class (𝑤‘((♯‘𝑤) − 1))
22 caddc 10141 . . . . 5 class +
2319, 21, 22co 6793 . . . 4 class ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))
245, 14, 23cmpt 4863 . . 3 class (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))
25 csseq 30785 . . 3 class seqstr
264, 24, 25co 6793 . 2 class (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
271, 26wceq 1631 1 wff Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
Colors of variables: wff setvar class
This definition is referenced by:  fib0  30801  fib1  30802  fibp1  30803
  Copyright terms: Public domain W3C validator