Theorem itcovalt2lem2

Description: Lemma 2 for itcovalt2 : induction step. (Contributed by AV, 7-May-2024)

	Ref	Expression
Hypothesis	itcovalt2.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼2n+C\right)$$
Assertion	itcovalt2lem2	Could not format assertion : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - 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	2	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼2n+C\right)\in \mathrm{V}$$
4	1 3	eqeltri	$$⊢F\in \mathrm{V}$$
5		simpl	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to y\in {\mathbb{N}}_0$$
6		simpr	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) with typecode |-
7		itcovalsucov	Could not format ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) : No typesetting found for |- ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) with typecode |-
8	4 5 6 7	mp3an2ani	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) ) with typecode |-
9		2nn	$$⊢2\in \mathbb{N}$$
10	9	a1i	$$⊢y\in {\mathbb{N}}_0\to 2\in \mathbb{N}$$
11		id	$$⊢y\in {\mathbb{N}}_0\to y\in {\mathbb{N}}_0$$
12	10 11	nnexpcld	$$⊢y\in {\mathbb{N}}_0\to 2^y\in \mathbb{N}$$
13		itcovalt2lem2lem1	$$⊢\left(\left(2^y\in \mathbb{N}\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)2^y-C\in {\mathbb{N}}_0$$
14	12 13	sylanl1	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to \left(n+C\right)2^y-C\in {\mathbb{N}}_0$$
15		eqidd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)$$
16		oveq2	$$⊢n=m\to 2n=2m$$
17	16	oveq1d	$$⊢n=m\to 2n+C=2m+C$$
18	17	cbvmptv	$$⊢\left(n\in {\mathbb{N}}_0⟼2n+C\right)=\left(m\in {\mathbb{N}}_0⟼2m+C\right)$$
19	1 18	eqtri	$$⊢F=\left(m\in {\mathbb{N}}_0⟼2m+C\right)$$
20	19	a1i	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F=\left(m\in {\mathbb{N}}_0⟼2m+C\right)$$
21		oveq2	$$⊢m=\left(n+C\right)2^y-C\to 2m=2\left(\left(n+C\right)2^y-C\right)$$
22	21	oveq1d	$$⊢m=\left(n+C\right)2^y-C\to 2m+C=2\left(\left(n+C\right)2^y-C\right)+C$$
23	14 15 20 22	fmptco	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F\circ \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)=\left(n\in {\mathbb{N}}_0⟼2\left(\left(n+C\right)2^y-C\right)+C\right)$$
24		itcovalt2lem2lem2	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge n\in {\mathbb{N}}_0\right)\to 2\left(\left(n+C\right)2^y-C\right)+C=\left(n+C\right)2^{y+1}-C$$
25	24	mpteq2dva	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼2\left(\left(n+C\right)2^y-C\right)+C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)$$
26	23 25	eqtrd	$$⊢\left(y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to F\circ \left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^y-C\right)=\left(n\in {\mathbb{N}}_0⟼\left(n+C\right)2^{y+1}-C\right)$$
27	26	adantr	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( F o. ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) with typecode |-
28	8 27	eqtrd	Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) with typecode |-
29	28	ex	Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ y ) ) - C ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( ( ( n + C ) x. ( 2 ^ ( y + 1 ) ) ) - C ) ) ) ) with typecode |-