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 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
2	1	fveq1i	⊢ ( Fibci ‘ 0 ) = ( ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 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 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) = ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) )
11		fiblem	⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) : ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) ⟶ ℕ0
12	11	a1i	⊢ ( ⊤ → ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) : ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 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 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ‘ 0 ) = ( ⟨“ 0 1 ”⟩ ‘ 0 ) )
21	20	mptru	⊢ ( ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 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