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 |