Theorem itcovalt2lem2lem2

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

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		2cnd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\in ℂ$$
2		simpr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
3		simpr	$$⊢\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C\in {\mathbb{N}}_0$$
4	3	adantr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to C\in {\mathbb{N}}_0$$
5	2 4	nn0addcld	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to N+C\in {\mathbb{N}}_0$$
6	5	nn0cnd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to N+C\in ℂ$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢Y\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
9		id	$$⊢Y\in {\mathbb{N}}_0\to Y\in {\mathbb{N}}_0$$
10	8 9	nn0expcld	$$⊢Y\in {\mathbb{N}}_0\to 2^Y\in {\mathbb{N}}_0$$
11	10	nn0cnd	$$⊢Y\in {\mathbb{N}}_0\to 2^Y\in ℂ$$
12	11	ad2antrr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2^Y\in ℂ$$
13	6 12	mulcld	$$⊢\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\in ℂ$$
14		nn0cn	$$⊢C\in {\mathbb{N}}_0\to C\in ℂ$$
15	14	ad2antlr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to C\in ℂ$$
16	1 13 15	subdid	$$⊢\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)=2\left(N+C\right)2^Y-2C$$
17	16	oveq1d	$$⊢\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=2\left(N+C\right)2^Y-2C+C$$
18	7	a1i	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\in {\mathbb{N}}_0$$
19	10	ad2antrr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2^Y\in {\mathbb{N}}_0$$
20	5 19	nn0mulcld	$$⊢\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\in {\mathbb{N}}_0$$
21	18 20	nn0mulcld	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y\in {\mathbb{N}}_0$$
22	21	nn0cnd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y\in ℂ$$
23	7	a1i	$$⊢\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to 2\in {\mathbb{N}}_0$$
24	23 3	nn0mulcld	$$⊢\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to 2C\in {\mathbb{N}}_0$$
25	24	adantr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2C\in {\mathbb{N}}_0$$
26	25	nn0cnd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2C\in ℂ$$
27	4	nn0cnd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to C\in ℂ$$
28	22 26 27	subsubd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y-\left(2C-C\right)=2\left(N+C\right)2^Y-2C+C$$
29	1 6 12	mul12d	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y=\left(N+C\right)22^Y$$
30		2cnd	$$⊢Y\in {\mathbb{N}}_0\to 2\in ℂ$$
31	30 11	mulcomd	$$⊢Y\in {\mathbb{N}}_0\to 22^Y=2^Y\cdot 2$$
32	30 9	expp1d	$$⊢Y\in {\mathbb{N}}_0\to 2^{Y+1}=2^Y\cdot 2$$
33	31 32	eqtr4d	$$⊢Y\in {\mathbb{N}}_0\to 22^Y=2^{Y+1}$$
34	33	ad2antrr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 22^Y=2^{Y+1}$$
35	34	oveq2d	$$⊢\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)22^Y=\left(N+C\right)2^{Y+1}$$
36	29 35	eqtrd	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y=\left(N+C\right)2^{Y+1}$$
37		2txmxeqx	$$⊢C\in ℂ\to 2C-C=C$$
38	14 37	syl	$$⊢C\in {\mathbb{N}}_0\to 2C-C=C$$
39	38	ad2antlr	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2C-C=C$$
40	36 39	oveq12d	$$⊢\left(\left(Y\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to 2\left(N+C\right)2^Y-\left(2C-C\right)=\left(N+C\right)2^{Y+1}-C$$
41	17 28 40	3eqtr2d	$$⊢\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$$