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 33396
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 33395 . 2 class Fibci
2 cc0 11110 . . . 4 class 0
3 c1 11111 . . . 4 class 1
42, 3cs2 14792 . . 3 class ⟨“01”⟩
5 vw . . . 4 setvar 𝑤
6 cn0 12472 . . . . . 6 class 0
76cword 14464 . . . . 5 class Word ℕ0
8 chash 14290 . . . . . . 7 class
98ccnv 5676 . . . . . 6 class
10 c2 12267 . . . . . . 7 class 2
11 cuz 12822 . . . . . . 7 class
1210, 11cfv 6544 . . . . . 6 class (ℤ‘2)
139, 12cima 5680 . . . . 5 class (♯ “ (ℤ‘2))
147, 13cin 3948 . . . 4 class (Word ℕ0 ∩ (♯ “ (ℤ‘2)))
155cv 1541 . . . . . . . 8 class 𝑤
1615, 8cfv 6544 . . . . . . 7 class (♯‘𝑤)
17 cmin 11444 . . . . . . 7 class
1816, 10, 17co 7409 . . . . . 6 class ((♯‘𝑤) − 2)
1918, 15cfv 6544 . . . . 5 class (𝑤‘((♯‘𝑤) − 2))
2016, 3, 17co 7409 . . . . . 6 class ((♯‘𝑤) − 1)
2120, 15cfv 6544 . . . . 5 class (𝑤‘((♯‘𝑤) − 1))
22 caddc 11113 . . . . 5 class +
2319, 21, 22co 7409 . . . 4 class ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))
245, 14, 23cmpt 5232 . . 3 class (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))
25 csseq 33382 . . 3 class seqstr
264, 24, 25co 7409 . 2 class (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
271, 26wceq 1542 1 wff Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
Colors of variables: wff setvar class
This definition is referenced by:  fib0  33398  fib1  33399  fibp1  33400
  Copyright terms: Public domain W3C validator