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