Metamath Proof Explorer

Theorem fib0

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

Ref Expression
Assertion fib0 ⊢ Fibci ⁡ 0 = 0

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 ⁡ 0 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 0
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 lbfzo0 ⊢ 0 ∈ 0 ..^ 2 ↔ 2 ∈ ℕ
15 13 14 mpbir ⊢ 0 ∈ 0 ..^ 2
16 s2len ⊢ ⟨“ 0 1 ”⟩ = 2
17 16 oveq2i ⊢ 0 ..^ ⟨“ 0 1 ”⟩ = 0 ..^ 2
18 15 17 eleqtrri ⊢ 0 ∈ 0 ..^ ⟨“ 0 1 ”⟩
19 18 a1i ⊢ ⊤ → 0 ∈ 0 ..^ ⟨“ 0 1 ”⟩
20 4 9 10 12 19 sseqfv1 ⊢ ⊤ → ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 0 = ⟨“ 0 1 ”⟩ ⁡ 0
21 20 mptru ⊢ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ 0 = ⟨“ 0 1 ”⟩ ⁡ 0
22 s2fv0 ⊢ 0 ∈ ℕ 0 → ⟨“ 0 1 ”⟩ ⁡ 0 = 0
23 5 22 ax-mp ⊢ ⟨“ 0 1 ”⟩ ⁡ 0 = 0
24 2 21 23 3eqtri ⊢ Fibci ⁡ 0 = 0