Theorem fib6

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

	Ref	Expression
Assertion	fib6	$$⊢\mathrm{Fibci}\left(6\right)=8$$

Proof

Step	Hyp	Ref	Expression
1		5p1e6	$$⊢5+1=6$$
2	1	fveq2i	$$⊢\mathrm{Fibci}\left(5+1\right)=\mathrm{Fibci}\left(6\right)$$
3		5nn	$$⊢5\in \mathbb{N}$$
4		fibp1	$$⊢5\in \mathbb{N}\to \mathrm{Fibci}\left(5+1\right)=\mathrm{Fibci}\left(5-1\right)+\mathrm{Fibci}\left(5\right)$$
5	3 4	ax-mp	$$⊢\mathrm{Fibci}\left(5+1\right)=\mathrm{Fibci}\left(5-1\right)+\mathrm{Fibci}\left(5\right)$$
6		5cn	$$⊢5\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
8		4cn	$$⊢4\in ℂ$$
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	$$⊢\mathrm{Fibci}\left(5-1\right)=\mathrm{Fibci}\left(4\right)$$
13		fib4	$$⊢\mathrm{Fibci}\left(4\right)=3$$
14	12 13	eqtri	$$⊢\mathrm{Fibci}\left(5-1\right)=3$$
15		fib5	$$⊢\mathrm{Fibci}\left(5\right)=5$$
16	14 15	oveq12i	$$⊢\mathrm{Fibci}\left(5-1\right)+\mathrm{Fibci}\left(5\right)=3+5$$
17		3cn	$$⊢3\in ℂ$$
18		5p3e8	$$⊢5+3=8$$
19	6 17 18	addcomli	$$⊢3+5=8$$
20	5 16 19	3eqtri	$$⊢\mathrm{Fibci}\left(5+1\right)=8$$
21	2 20	eqtr3i	$$⊢\mathrm{Fibci}\left(6\right)=8$$