Theorem itcovalpclem1

Description: Lemma 1 for itcovalpc : induction basis. (Contributed by AV, 4-May-2024)

	Ref	Expression
Hypothesis	itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
Assertion	itcovalpclem1	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3		ovexd	$$⊢n\in {\mathbb{N}}_0\to n+C\in \mathrm{V}$$
4	3	rgen	$$⊢\forall n\in {\mathbb{N}}_{0}n+C\in \mathrm{V}$$
5	1	itcoval0mpt	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \forall n\in {\mathbb{N}}_{0}n+C\in \mathrm{V}\right)\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n\right)$$
6	2 4 5	mp2an	$$⊢\mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n\right)$$
7		nn0cn	$$⊢C\in {\mathbb{N}}_0\to C\in ℂ$$
8	7	mul01d	$$⊢C\in {\mathbb{N}}_0\to C\cdot 0=0$$
9	8	adantr	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to C\cdot 0=0$$
10	9	oveq2d	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+C\cdot 0=n+0$$
11		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
12	11	addridd	$$⊢n\in {\mathbb{N}}_0\to n+0=n$$
13	12	adantl	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+0=n$$
14	10 13	eqtr2d	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n=n+C\cdot 0$$
15	14	mpteq2dva	$$⊢C\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼n\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$
16	6 15	eqtrid	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$