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 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
2	1	fveq1i	⊢ ( Fibci ‘ 1 ) = ( ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 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 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 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		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 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) ‘ 1 ) = ( ⟨“ 0 1 ”⟩ ‘ 1 ) )
22	21	mptru	⊢ ( ( ⟨“ 0 1 ”⟩ seqstr ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 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