Metamath Proof Explorer

Theorem fib5

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

Ref Expression
Assertion fib5 
|- ( Fibci ` 5 ) = 5

Proof

Step Hyp Ref Expression
1 4p1e5 
 |-  ( 4 + 1 ) = 5
2 1 fveq2i 
 |-  ( Fibci ` ( 4 + 1 ) ) = ( Fibci ` 5 )
3 4nn 
 |-  4 e. NN
4 fibp1 
 |-  ( 4 e. NN -> ( Fibci ` ( 4 + 1 ) ) = ( ( Fibci ` ( 4 - 1 ) ) + ( Fibci ` 4 ) ) )
5 3 4 ax-mp 
 |-  ( Fibci ` ( 4 + 1 ) ) = ( ( Fibci ` ( 4 - 1 ) ) + ( Fibci ` 4 ) )
6 4cn 
 |-  4 e. CC
7 ax-1cn 
 |-  1 e. CC
8 3cn 
 |-  3 e. CC
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 8 7 9 addcomli 
 |-  ( 1 + 3 ) = 4
11 6 7 8 10 subaddrii 
 |-  ( 4 - 1 ) = 3
12 11 fveq2i 
 |-  ( Fibci ` ( 4 - 1 ) ) = ( Fibci ` 3 )
13 fib3 
 |-  ( Fibci ` 3 ) = 2
14 12 13 eqtri 
 |-  ( Fibci ` ( 4 - 1 ) ) = 2
15 fib4 
 |-  ( Fibci ` 4 ) = 3
16 14 15 oveq12i 
 |-  ( ( Fibci ` ( 4 - 1 ) ) + ( Fibci ` 4 ) ) = ( 2 + 3 )
17 2cn 
 |-  2 e. CC
18 3p2e5 
 |-  ( 3 + 2 ) = 5
19 8 17 18 addcomli 
 |-  ( 2 + 3 ) = 5
20 5 16 19 3eqtri 
 |-  ( Fibci ` ( 4 + 1 ) ) = 5
21 2 20 eqtr3i 
 |-  ( Fibci ` 5 ) = 5