Metamath Proof Explorer

Theorem fib4

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

Ref Expression
Assertion fib4 
|- ( Fibci ` 4 ) = 3

Proof

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