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 e. NN
4 fibp1 
 |-  ( 5 e. NN -> ( Fibci ` ( 5 + 1 ) ) = ( ( Fibci ` ( 5 - 1 ) ) + ( Fibci ` 5 ) ) )
5 3 4 ax-mp 
 |-  ( Fibci ` ( 5 + 1 ) ) = ( ( Fibci ` ( 5 - 1 ) ) + ( Fibci ` 5 ) )
6 5cn 
 |-  5 e. CC
7 ax-1cn 
 |-  1 e. CC
8 4cn 
 |-  4 e. CC
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 e. CC
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