Metamath Proof Explorer


Theorem fib2

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

Ref Expression
Assertion fib2 Fibci2=1

Proof

Step Hyp Ref Expression
1 1p1e2 1+1=2
2 1 fveq2i Fibci1+1=Fibci2
3 1nn 1
4 fibp1 1Fibci1+1=Fibci11+Fibci1
5 3 4 ax-mp Fibci1+1=Fibci11+Fibci1
6 1m1e0 11=0
7 6 fveq2i Fibci11=Fibci0
8 fib0 Fibci0=0
9 7 8 eqtri Fibci11=0
10 fib1 Fibci1=1
11 9 10 oveq12i Fibci11+Fibci1=0+1
12 0p1e1 0+1=1
13 5 11 12 3eqtri Fibci1+1=1
14 2 13 eqtr3i Fibci2=1