Metamath Proof Explorer

Theorem fib3

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

Ref Expression
Assertion fib3 
|- ( Fibci ` 3 ) = 2

Proof

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