Theorem fib3

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

	Ref	Expression
Assertion	fib3	⊢ ( Fibci ‘ 3 ) = 2

Proof

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