Theorem fib5

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

	Ref	Expression
Assertion	fib5	$$⊢\mathrm{Fibci}\left(5\right)=5$$

Proof

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