Theorem fib6

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

	Ref	Expression
Assertion	fib6	⊢ ( Fibci ‘ 6 ) = 8

Proof

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