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\to F\left(N+1\right)=F\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢N=0\to N+1=0+1$$
2		0p1e1	$$⊢0+1=1$$
3	1 2	eqtrdi	$$⊢N=0\to N+1=1$$
4	3	fveq2d	$$⊢N=0\to F\left(N+1\right)=F\left(1\right)$$