Description: Function value at N + 1 with N replaced by 0 . Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fv0p1e1 | |- ( N = 0 -> ( F ` ( N + 1 ) ) = ( F ` 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq1 | |- ( N = 0 -> ( N + 1 ) = ( 0 + 1 ) ) |
|
| 2 | 0p1e1 | |- ( 0 + 1 ) = 1 |
|
| 3 | 1 2 | eqtrdi | |- ( N = 0 -> ( N + 1 ) = 1 ) |
| 4 | 3 | fveq2d | |- ( N = 0 -> ( F ` ( N + 1 ) ) = ( F ` 1 ) ) |