Theorem fib4

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

	Ref	Expression
Assertion	fib4	⊢ ( Fibci ‘ 4 ) = 3

Proof

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