Theorem fib3

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

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

Proof

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