Metamath Proof Explorer


Theorem fv0p1e1

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

Proof

Step Hyp Ref Expression
1 oveq1 N = 0 N + 1 = 0 + 1
2 0p1e1 0 + 1 = 1
3 1 2 syl6eq N = 0 N + 1 = 1
4 3 fveq2d N = 0 F N + 1 = F 1