Metamath Proof Explorer


Theorem fib6

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

Ref Expression
Assertion fib6 ( Fibci ‘ 6 ) = 8

Proof

Step Hyp Ref Expression
1 5p1e6 ( 5 + 1 ) = 6
2 1 fveq2i ( Fibci ‘ ( 5 + 1 ) ) = ( Fibci ‘ 6 )
3 5nn 5 ∈ ℕ
4 fibp1 ( 5 ∈ ℕ → ( Fibci ‘ ( 5 + 1 ) ) = ( ( Fibci ‘ ( 5 − 1 ) ) + ( Fibci ‘ 5 ) ) )
5 3 4 ax-mp ( Fibci ‘ ( 5 + 1 ) ) = ( ( Fibci ‘ ( 5 − 1 ) ) + ( Fibci ‘ 5 ) )
6 5cn 5 ∈ ℂ
7 ax-1cn 1 ∈ ℂ
8 4cn 4 ∈ ℂ
9 4p1e5 ( 4 + 1 ) = 5
10 8 7 9 addcomli ( 1 + 4 ) = 5
11 6 7 8 10 subaddrii ( 5 − 1 ) = 4
12 11 fveq2i ( Fibci ‘ ( 5 − 1 ) ) = ( Fibci ‘ 4 )
13 fib4 ( Fibci ‘ 4 ) = 3
14 12 13 eqtri ( Fibci ‘ ( 5 − 1 ) ) = 3
15 fib5 ( Fibci ‘ 5 ) = 5
16 14 15 oveq12i ( ( Fibci ‘ ( 5 − 1 ) ) + ( Fibci ‘ 5 ) ) = ( 3 + 5 )
17 3cn 3 ∈ ℂ
18 5p3e8 ( 5 + 3 ) = 8
19 6 17 18 addcomli ( 3 + 5 ) = 8
20 5 16 19 3eqtri ( Fibci ‘ ( 5 + 1 ) ) = 8
21 2 20 eqtr3i ( Fibci ‘ 6 ) = 8