Theorem fib2

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

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

Proof

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