Theorem fib4

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

	Ref	Expression
Assertion	fib4	$$⊢\mathrm{Fibci}\left(4\right)=3$$

Proof

Step	Hyp	Ref	Expression
1		3p1e4	$$⊢3+1=4$$
2	1	fveq2i	$$⊢\mathrm{Fibci}\left(3+1\right)=\mathrm{Fibci}\left(4\right)$$
3		3nn	$$⊢3\in \mathbb{N}$$
4		fibp1	$$⊢3\in \mathbb{N}\to \mathrm{Fibci}\left(3+1\right)=\mathrm{Fibci}\left(3-1\right)+\mathrm{Fibci}\left(3\right)$$
5	3 4	ax-mp	$$⊢\mathrm{Fibci}\left(3+1\right)=\mathrm{Fibci}\left(3-1\right)+\mathrm{Fibci}\left(3\right)$$
6		3m1e2	$$⊢3-1=2$$
7	6	fveq2i	$$⊢\mathrm{Fibci}\left(3-1\right)=\mathrm{Fibci}\left(2\right)$$
8		fib2	$$⊢\mathrm{Fibci}\left(2\right)=1$$
9	7 8	eqtri	$$⊢\mathrm{Fibci}\left(3-1\right)=1$$
10		fib3	$$⊢\mathrm{Fibci}\left(3\right)=2$$
11	9 10	oveq12i	$$⊢\mathrm{Fibci}\left(3-1\right)+\mathrm{Fibci}\left(3\right)=1+2$$
12		1p2e3	$$⊢1+2=3$$
13	5 11 12	3eqtri	$$⊢\mathrm{Fibci}\left(3+1\right)=3$$
14	2 13	eqtr3i	$$⊢\mathrm{Fibci}\left(4\right)=3$$