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 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfib class Fibci
1 cc0 class 0
2 c1 class 1
3 1 2 cs2 class ⟨“ 0 1 ”⟩
4 csseq class seq str
5 vw setvar w
6 cn0 class ℕ 0
7 6 cword class Word ℕ 0
8 chash class .
9 8 ccnv class . -1
10 cuz class ℤ ≥
11 c2 class 2
12 11 10 cfv class ℤ ≥ 2
13 9 12 cima class . -1 ℤ ≥ 2
14 7 13 cin class Word ℕ 0 ∩ . -1 ℤ ≥ 2
15 5 cv setvar w
16 15 8 cfv class w
17 cmin class −
18 16 11 17 co class w − 2
19 18 15 cfv class w ⁡ w − 2
20 caddc class +
21 16 2 17 co class w − 1
22 21 15 cfv class w ⁡ w − 1
23 19 22 20 co class w ⁡ w − 2 + w ⁡ w − 1
24 5 14 23 cmpt class w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
25 3 24 4 co class ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
26 0 25 wceq wff Fibci = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1