Metamath Proof Explorer

Theorem fib1

Description: Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019)

Ref Expression
Assertion fib1 ⊢ Fibci ⁡ 1 = 1

Proof

Step Hyp Ref Expression
1 df-fib ⊢ Fibci = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
2 1 fveq1i ⊢ Fibci ⁡ 1 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 1
3 nn0ex ⊢ ℕ 0 ∈ V
4 3 a1i ⊢ ⊤ → ℕ 0 ∈ V
5 0nn0 ⊢ 0 ∈ ℕ 0
6 5 a1i ⊢ ⊤ → 0 ∈ ℕ 0
7 1nn0 ⊢ 1 ∈ ℕ 0
8 7 a1i ⊢ ⊤ → 1 ∈ ℕ 0
9 6 8 s2cld ⊢ ⊤ → ⟨“ 0 1 ”⟩ ∈ Word ℕ 0
10 eqid ⊢ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ = Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩
11 fiblem ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ⟶ ℕ 0
12 11 a1i ⊢ ⊤ → w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ⟶ ℕ 0
13 2nn ⊢ 2 ∈ ℕ
14 1lt2 ⊢ 1 < 2
15 elfzo0 ⊢ 1 ∈ 0 ..^ 2 ↔ 1 ∈ ℕ 0 ∧ 2 ∈ ℕ ∧ 1 < 2
16 7 13 14 15 mpbir3an ⊢ 1 ∈ 0 ..^ 2
17 s2len ⊢ ⟨“ 0 1 ”⟩ = 2
18 17 oveq2i ⊢ 0 ..^ ⟨“ 0 1 ”⟩ = 0 ..^ 2
19 16 18 eleqtrri ⊢ 1 ∈ 0 ..^ ⟨“ 0 1 ”⟩
20 19 a1i ⊢ ⊤ → 1 ∈ 0 ..^ ⟨“ 0 1 ”⟩
21 4 9 10 12 20 sseqfv1 ⊢ ⊤ → ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 1 = ⟨“ 0 1 ”⟩ ⁡ 1
22 21 mptru ⊢ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 1 = ⟨“ 0 1 ”⟩ ⁡ 1
23 s2fv1 ⊢ 1 ∈ ℕ 0 → ⟨“ 0 1 ”⟩ ⁡ 1 = 1
24 7 23 ax-mp ⊢ ⟨“ 0 1 ”⟩ ⁡ 1 = 1
25 2 22 24 3eqtri ⊢ Fibci ⁡ 1 = 1