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 ∈ ℕ
4 fibp1 ( 3 ∈ ℕ → ( 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