Theorem fib2

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

	Ref	Expression
Assertion	fib2	⊢ ( Fibci ‘ 2 ) = 1

Proof

Step	Hyp	Ref	Expression
1		1p1e2	⊢ ( 1 + 1 ) = 2
2	1	fveq2i	⊢ ( Fibci ‘ ( 1 + 1 ) ) = ( Fibci ‘ 2 )
3		1nn	⊢ 1 ∈ ℕ
4		fibp1	⊢ ( 1 ∈ ℕ → ( Fibci ‘ ( 1 + 1 ) ) = ( ( Fibci ‘ ( 1 − 1 ) ) + ( Fibci ‘ 1 ) ) )
5	3 4	ax-mp	⊢ ( Fibci ‘ ( 1 + 1 ) ) = ( ( Fibci ‘ ( 1 − 1 ) ) + ( Fibci ‘ 1 ) )
6		1m1e0	⊢ ( 1 − 1 ) = 0
7	6	fveq2i	⊢ ( Fibci ‘ ( 1 − 1 ) ) = ( Fibci ‘ 0 )
8		fib0	⊢ ( Fibci ‘ 0 ) = 0
9	7 8	eqtri	⊢ ( Fibci ‘ ( 1 − 1 ) ) = 0
10		fib1	⊢ ( Fibci ‘ 1 ) = 1
11	9 10	oveq12i	⊢ ( ( Fibci ‘ ( 1 − 1 ) ) + ( Fibci ‘ 1 ) ) = ( 0 + 1 )
12		0p1e1	⊢ ( 0 + 1 ) = 1
13	5 11 12	3eqtri	⊢ ( Fibci ‘ ( 1 + 1 ) ) = 1
14	2 13	eqtr3i	⊢ ( Fibci ‘ 2 ) = 1