Theorem fib5

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

	Ref	Expression
Assertion	fib5	⊢ ( Fibci ‘ 5 ) = 5

Proof

Step	Hyp	Ref	Expression
1		4p1e5	⊢ ( 4 + 1 ) = 5
2	1	fveq2i	⊢ ( Fibci ‘ ( 4 + 1 ) ) = ( Fibci ‘ 5 )
3		4nn	⊢ 4 ∈ ℕ
4		fibp1	⊢ ( 4 ∈ ℕ → ( Fibci ‘ ( 4 + 1 ) ) = ( ( Fibci ‘ ( 4 − 1 ) ) + ( Fibci ‘ 4 ) ) )
5	3 4	ax-mp	⊢ ( Fibci ‘ ( 4 + 1 ) ) = ( ( Fibci ‘ ( 4 − 1 ) ) + ( Fibci ‘ 4 ) )
6		4cn	⊢ 4 ∈ ℂ
7		ax-1cn	⊢ 1 ∈ ℂ
8		3cn	⊢ 3 ∈ ℂ
9		3p1e4	⊢ ( 3 + 1 ) = 4
10	8 7 9	addcomli	⊢ ( 1 + 3 ) = 4
11	6 7 8 10	subaddrii	⊢ ( 4 − 1 ) = 3
12	11	fveq2i	⊢ ( Fibci ‘ ( 4 − 1 ) ) = ( Fibci ‘ 3 )
13		fib3	⊢ ( Fibci ‘ 3 ) = 2
14	12 13	eqtri	⊢ ( Fibci ‘ ( 4 − 1 ) ) = 2
15		fib4	⊢ ( Fibci ‘ 4 ) = 3
16	14 15	oveq12i	⊢ ( ( Fibci ‘ ( 4 − 1 ) ) + ( Fibci ‘ 4 ) ) = ( 2 + 3 )
17		2cn	⊢ 2 ∈ ℂ
18		3p2e5	⊢ ( 3 + 2 ) = 5
19	8 17 18	addcomli	⊢ ( 2 + 3 ) = 5
20	5 16 19	3eqtri	⊢ ( Fibci ‘ ( 4 + 1 ) ) = 5
21	2 20	eqtr3i	⊢ ( Fibci ‘ 5 ) = 5