itcovalt2lem2

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

		Ref	Expression
	Hypothesis	itcovalt2.f	$⊢ F = (n \in ℕ_{0} ⟼ 2 n + C)$
	Assertion	itcovalt2lem2	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) \to IterComp (F) (y + 1) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C))$

Proof

Step	Hyp	Ref	Expression
1		itcovalt2.f	$⊢ F = (n \in ℕ_{0} ⟼ 2 n + C)$
2		nn0ex	$⊢ ℕ_{0} \in V$
3	2	mptex	$⊢ (n \in ℕ_{0} ⟼ 2 n + C) \in V$
4	1 3	eqeltri	$⊢ F \in V$
5		simpl	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to y \in ℕ_{0}$
6		simpr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)) \to IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)$
7		itcovalsucov	$⊢ (F \in V \land y \in ℕ_{0} \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)) \to IterComp (F) (y + 1) = F \circ (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)$
8	4 5 6 7	mp3an2ani	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)) \to IterComp (F) (y + 1) = F \circ (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)$
9		2nn	$⊢ 2 \in ℕ$
10	9	a1i	$⊢ y \in ℕ_{0} \to 2 \in ℕ$
11		id	$⊢ y \in ℕ_{0} \to y \in ℕ_{0}$
12	10 11	nnexpcld	$⊢ y \in ℕ_{0} \to 2^{y} \in ℕ$
13		itcovalt2lem2lem1	$⊢ ((2^{y} \in ℕ \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to (n + C) 2^{y} - C \in ℕ_{0}$
14	12 13	sylanl1	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to (n + C) 2^{y} - C \in ℕ_{0}$
15		eqidd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)$
16		oveq2	$⊢ n = m \to 2 n = 2 m$
17	16	oveq1d	$⊢ n = m \to 2 n + C = 2 m + C$
18	17	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ 2 n + C) = (m \in ℕ_{0} ⟼ 2 m + C)$
19	1 18	eqtri	$⊢ F = (m \in ℕ_{0} ⟼ 2 m + C)$
20	19	a1i	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F = (m \in ℕ_{0} ⟼ 2 m + C)$
21		oveq2	$⊢ m = (n + C) 2^{y} - C \to 2 m = 2 ((n + C) 2^{y} - C)$
22	21	oveq1d	$⊢ m = (n + C) 2^{y} - C \to 2 m + C = 2 ((n + C) 2^{y} - C) + C$
23	14 15 20 22	fmptco	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F \circ (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) = (n \in ℕ_{0} ⟼ 2 ((n + C) 2^{y} - C) + C)$
24		itcovalt2lem2lem2	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to 2 ((n + C) 2^{y} - C) + C = (n + C) 2^{y + 1} - C$
25	24	mpteq2dva	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ 2 ((n + C) 2^{y} - C) + C) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C)$
26	23 25	eqtrd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F \circ (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C)$
27	26	adantr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)) \to F \circ (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C)$
28	8 27	eqtrd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C)) \to IterComp (F) (y + 1) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C)$
29	28	ex	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (IterComp (F) (y) = (n \in ℕ_{0} ⟼ (n + C) 2^{y} - C) \to IterComp (F) (y + 1) = (n \in ℕ_{0} ⟼ (n + C) 2^{y + 1} - C))$

Metamath Proof Explorer

Theorem itcovalt2lem2

Proof