Theorem itcovalpclem1

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

	Ref	Expression
Hypothesis	itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
Assertion	itcovalpclem1	Could not format assertion : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		itcovalpc.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼n+C\right)$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3		ovexd	$$⊢n\in {\mathbb{N}}_0\to n+C\in \mathrm{V}$$
4	3	rgen	$$⊢\forall n\in {\mathbb{N}}_{0}n+C\in \mathrm{V}$$
5	1	itcoval0mpt	Could not format ( ( NN0 e. _V /\ A. n e. NN0 ( n + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) : No typesetting found for |- ( ( NN0 e. _V /\ A. n e. NN0 ( n + C ) e. _V ) -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) ) with typecode |-
6	2 4 5	mp2an	Could not format ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) : No typesetting found for |- ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> n ) with typecode |-
7		nn0cn	$$⊢C\in {\mathbb{N}}_0\to C\in ℂ$$
8	7	mul01d	$$⊢C\in {\mathbb{N}}_0\to C\cdot 0=0$$
9	8	adantr	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to C\cdot 0=0$$
10	9	oveq2d	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+C\cdot 0=n+0$$
11		nn0cn	$$⊢n\in {\mathbb{N}}_0\to n\in ℂ$$
12	11	addridd	$$⊢n\in {\mathbb{N}}_0\to n+0=n$$
13	12	adantl	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n+0=n$$
14	10 13	eqtr2d	$$⊢\left(C\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\to n=n+C\cdot 0$$
15	14	mpteq2dva	$$⊢C\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼n\right)=\left(n\in {\mathbb{N}}_0⟼n+C\cdot 0\right)$$
16	6 15	eqtrid	Could not format ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) : No typesetting found for |- ( C e. NN0 -> ( ( IterComp ` F ) ` 0 ) = ( n e. NN0 |-> ( n + ( C x. 0 ) ) ) ) with typecode |-