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	Could not format assertion : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) with typecode |-

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	Could not format ( ( NN0 e. _V /\ A. n e. NN0 ( ( 2 x. n ) + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) : No typesetting found for |- ( ( NN0 e. _V /\ A. n e. NN0 ( ( 2 x. n ) + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) with typecode |-
7	5 6	mp1i	Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) with typecode |-
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	Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ 0 ) ) - C ) ) ) with typecode |-