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 
|- ( Fibci ` 2 ) = 1

Proof

Step Hyp Ref Expression
1 1p1e2 
 |-  ( 1 + 1 ) = 2
2 1 fveq2i 
 |-  ( Fibci ` ( 1 + 1 ) ) = ( Fibci ` 2 )
3 1nn 
 |-  1 e. NN
4 fibp1 
 |-  ( 1 e. NN -> ( Fibci ` ( 1 + 1 ) ) = ( ( Fibci ` ( 1 - 1 ) ) + ( Fibci ` 1 ) ) )
5 3 4 ax-mp 
 |-  ( Fibci ` ( 1 + 1 ) ) = ( ( Fibci ` ( 1 - 1 ) ) + ( Fibci ` 1 ) )
6 1m1e0 
 |-  ( 1 - 1 ) = 0
7 6 fveq2i 
 |-  ( Fibci ` ( 1 - 1 ) ) = ( Fibci ` 0 )
8 fib0 
 |-  ( Fibci ` 0 ) = 0
9 7 8 eqtri 
 |-  ( Fibci ` ( 1 - 1 ) ) = 0
10 fib1 
 |-  ( Fibci ` 1 ) = 1
11 9 10 oveq12i 
 |-  ( ( Fibci ` ( 1 - 1 ) ) + ( Fibci ` 1 ) ) = ( 0 + 1 )
12 0p1e1 
 |-  ( 0 + 1 ) = 1
13 5 11 12 3eqtri 
 |-  ( Fibci ` ( 1 + 1 ) ) = 1
14 2 13 eqtr3i 
 |-  ( Fibci ` 2 ) = 1