Theorem itcovalt2lem1

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

	Ref	Expression
Hypothesis	itcovalt2.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+C\right)$$
Assertion	itcovalt2lem1	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)$$

Proof

Step	Hyp	Ref	Expression
1		itcovalt2.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+C\right)$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3		ovexd	$$⊢n\in {\mathbb{N}}_0\to 2n+C\in \mathrm{V}$$
4	3	rgen	$$⊢\forall n\in {\mathbb{N}}_{0}2n+C\in \mathrm{V}$$
5	2 4	pm3.2i	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \forall n\in {\mathbb{N}}_{0}2n+C\in \mathrm{V}\right)$$
6	1	itcoval0mpt	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \forall n\in {\mathbb{N}}_{0}2n+C\in \mathrm{V}\right)\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n\right)$$
7	5 6	mp1i	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼n\right)$$
8		simpr	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
9	8	nn0cnd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n\in ℂ$$
10		simpl	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to C\in {\mathbb{N}}_0$$
11	10	nn0cnd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to C\in ℂ$$
12		2nn0	$$⊢2\in {\mathbb{N}}_0$$
13	12	numexp0	$$⊢2^0=1$$
14	13	a1i	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to 2^0=1$$
15	14	oveq2d	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)2^0=\left(n+C\right)\cdot 1$$
16	8 10	nn0addcld	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+C\in {\mathbb{N}}_0$$
17	16	nn0cnd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+C\in ℂ$$
18	17	mulridd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)\cdot 1=n+C$$
19	15 18	eqtrd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)2^0=n+C$$
20	9 11 19	mvrraddd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)2^0-C=n$$
21	20	eqcomd	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n=\left(n+C\right)2^0-C$$
22	21	mpteq2dva	$$⊢C\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼n\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)$$
23	7 22	eqtrd	$$⊢C\in {\mathbb{N}}_0\to \mathrm{IterComp}\left(F\right)\left(0\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^0-C\right)$$