itcovalpclem2

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

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

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$⊢ F = (n \in ℕ_{0} ⟼ n + C)$
2		nn0ex	$⊢ ℕ_{0} \in V$
3	2	mptex	$⊢ (n \in ℕ_{0} ⟼ 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 y)) \to IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y)$
7		itcovalsucov	$⊢ (F \in V \land y \in ℕ_{0} \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y)) \to IterComp (F) (y + 1) = F \circ (n \in ℕ_{0} ⟼ n + C y)$
8	4 5 6 7	mp3an2ani	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y)) \to IterComp (F) (y + 1) = F \circ (n \in ℕ_{0} ⟼ n + C y)$
9		simpr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
10		simplr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to C \in ℕ_{0}$
11	5	adantr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to y \in ℕ_{0}$
12	10 11	nn0mulcld	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to C y \in ℕ_{0}$
13	9 12	nn0addcld	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n + C y \in ℕ_{0}$
14		eqidd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ n + C y) = (n \in ℕ_{0} ⟼ n + C y)$
15		oveq1	$⊢ n = m \to n + C = m + C$
16	15	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ n + C) = (m \in ℕ_{0} ⟼ m + C)$
17	1 16	eqtri	$⊢ F = (m \in ℕ_{0} ⟼ m + C)$
18	17	a1i	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F = (m \in ℕ_{0} ⟼ m + C)$
19		oveq1	$⊢ m = n + C y \to m + C = n + C y + C$
20	13 14 18 19	fmptco	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F \circ (n \in ℕ_{0} ⟼ n + C y) = (n \in ℕ_{0} ⟼ n + C y + C)$
21	9	nn0cnd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n \in ℂ$
22	12	nn0cnd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to C y \in ℂ$
23	10	nn0cnd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to C \in ℂ$
24	21 22 23	addassd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n + C y + C = n + C y + C$
25		nn0cn	$⊢ C \in ℕ_{0} \to C \in ℂ$
26	25	mulridd	$⊢ C \in ℕ_{0} \to C \cdot 1 = C$
27	26	adantl	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C \cdot 1 = C$
28	27	eqcomd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C = C \cdot 1$
29	28	oveq2d	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C y + C = C y + C \cdot 1$
30		simpr	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C \in ℕ_{0}$
31	30	nn0cnd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C \in ℂ$
32	5	nn0cnd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to y \in ℂ$
33		1cnd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to 1 \in ℂ$
34	31 32 33	adddid	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C (y + 1) = C y + C \cdot 1$
35	29 34	eqtr4d	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to C y + C = C (y + 1)$
36	35	oveq2d	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to n + C y + C = n + C (y + 1)$
37	36	adantr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n + C y + C = n + C (y + 1)$
38	24 37	eqtrd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land n \in ℕ_{0}) \to n + C y + C = n + C (y + 1)$
39	38	mpteq2dva	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ n + C y + C) = (n \in ℕ_{0} ⟼ n + C (y + 1))$
40	20 39	eqtrd	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to F \circ (n \in ℕ_{0} ⟼ n + C y) = (n \in ℕ_{0} ⟼ n + C (y + 1))$
41	40	adantr	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y)) \to F \circ (n \in ℕ_{0} ⟼ n + C y) = (n \in ℕ_{0} ⟼ n + C (y + 1))$
42	8 41	eqtrd	$⊢ ((y \in ℕ_{0} \land C \in ℕ_{0}) \land IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y)) \to IterComp (F) (y + 1) = (n \in ℕ_{0} ⟼ n + C (y + 1))$
43	42	ex	$⊢ (y \in ℕ_{0} \land C \in ℕ_{0}) \to (IterComp (F) (y) = (n \in ℕ_{0} ⟼ n + C y) \to IterComp (F) (y + 1) = (n \in ℕ_{0} ⟼ n + C (y + 1)))$

Metamath Proof Explorer

Theorem itcovalpclem2

Proof