Metamath Proof Explorer


Theorem itcovalpclem2

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

Ref Expression
Hypothesis itcovalpc.f F = n 0 n + C
Assertion itcovalpclem2 Could not format assertion : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 itcovalpc.f F = n 0 n + C
2 nn0ex 0 V
3 2 mptex n 0 n + C V
4 1 3 eqeltri F V
5 simpl y 0 C 0 y 0
6 simpr Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) with typecode |-
7 itcovalsucov Could not format ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) : No typesetting found for |- ( ( F e. _V /\ y e. NN0 /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) 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. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) ) with typecode |-
9 simpr y 0 C 0 n 0 n 0
10 simplr y 0 C 0 n 0 C 0
11 5 adantr y 0 C 0 n 0 y 0
12 10 11 nn0mulcld y 0 C 0 n 0 C y 0
13 9 12 nn0addcld y 0 C 0 n 0 n + C y 0
14 eqidd y 0 C 0 n 0 n + C y = n 0 n + C y
15 oveq1 n = m n + C = m + C
16 15 cbvmptv n 0 n + C = m 0 m + C
17 1 16 eqtri F = m 0 m + C
18 17 a1i y 0 C 0 F = m 0 m + C
19 oveq1 m = n + C y m + C = n + C y + C
20 13 14 18 19 fmptco y 0 C 0 F n 0 n + C y = n 0 n + C y + C
21 9 nn0cnd y 0 C 0 n 0 n
22 12 nn0cnd y 0 C 0 n 0 C y
23 10 nn0cnd y 0 C 0 n 0 C
24 21 22 23 addassd y 0 C 0 n 0 n + C y + C = n + C y + C
25 nn0cn C 0 C
26 25 mulid1d C 0 C 1 = C
27 26 adantl y 0 C 0 C 1 = C
28 27 eqcomd y 0 C 0 C = C 1
29 28 oveq2d y 0 C 0 C y + C = C y + C 1
30 simpr y 0 C 0 C 0
31 30 nn0cnd y 0 C 0 C
32 5 nn0cnd y 0 C 0 y
33 1cnd y 0 C 0 1
34 31 32 33 adddid y 0 C 0 C y + 1 = C y + C 1
35 29 34 eqtr4d y 0 C 0 C y + C = C y + 1
36 35 oveq2d y 0 C 0 n + C y + C = n + C y + 1
37 36 adantr y 0 C 0 n 0 n + C y + C = n + C y + 1
38 24 37 eqtrd y 0 C 0 n 0 n + C y + C = n + C y + 1
39 38 mpteq2dva y 0 C 0 n 0 n + C y + C = n 0 n + C y + 1
40 20 39 eqtrd y 0 C 0 F n 0 n + C y = n 0 n + C y + 1
41 40 adantr Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( F o. ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) with typecode |-
42 8 41 eqtrd Could not format ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) : No typesetting found for |- ( ( ( y e. NN0 /\ C e. NN0 ) /\ ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) with typecode |-
43 42 ex Could not format ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) : No typesetting found for |- ( ( y e. NN0 /\ C e. NN0 ) -> ( ( ( IterComp ` F ) ` y ) = ( n e. NN0 |-> ( n + ( C x. y ) ) ) -> ( ( IterComp ` F ) ` ( y + 1 ) ) = ( n e. NN0 |-> ( n + ( C x. ( y + 1 ) ) ) ) ) ) with typecode |-