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 |