Description: Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | fib2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1p1e2 | |
|
2 | 1 | fveq2i | |
3 | 1nn | |
|
4 | fibp1 | |
|
5 | 3 4 | ax-mp | |
6 | 1m1e0 | |
|
7 | 6 | fveq2i | |
8 | fib0 | |
|
9 | 7 8 | eqtri | |
10 | fib1 | |
|
11 | 9 10 | oveq12i | |
12 | 0p1e1 | |
|
13 | 5 11 12 | 3eqtri | |
14 | 2 13 | eqtr3i | |