Step |
Hyp |
Ref |
Expression |
1 |
|
climadd.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
climadd.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
climadd.4 |
|- ( ph -> F ~~> A ) |
4 |
|
climaddc1.5 |
|- ( ph -> C e. CC ) |
5 |
|
climaddc1.6 |
|- ( ph -> G e. W ) |
6 |
|
climaddc1.7 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
7 |
|
climsubc2.h |
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C - ( F ` k ) ) ) |
8 |
|
0z |
|- 0 e. ZZ |
9 |
|
uzssz |
|- ( ZZ>= ` 0 ) C_ ZZ |
10 |
|
zex |
|- ZZ e. _V |
11 |
9 10
|
climconst2 |
|- ( ( C e. CC /\ 0 e. ZZ ) -> ( ZZ X. { C } ) ~~> C ) |
12 |
4 8 11
|
sylancl |
|- ( ph -> ( ZZ X. { C } ) ~~> C ) |
13 |
|
eluzelz |
|- ( k e. ( ZZ>= ` M ) -> k e. ZZ ) |
14 |
13 1
|
eleq2s |
|- ( k e. Z -> k e. ZZ ) |
15 |
|
fvconst2g |
|- ( ( C e. CC /\ k e. ZZ ) -> ( ( ZZ X. { C } ) ` k ) = C ) |
16 |
4 14 15
|
syl2an |
|- ( ( ph /\ k e. Z ) -> ( ( ZZ X. { C } ) ` k ) = C ) |
17 |
4
|
adantr |
|- ( ( ph /\ k e. Z ) -> C e. CC ) |
18 |
16 17
|
eqeltrd |
|- ( ( ph /\ k e. Z ) -> ( ( ZZ X. { C } ) ` k ) e. CC ) |
19 |
16
|
oveq1d |
|- ( ( ph /\ k e. Z ) -> ( ( ( ZZ X. { C } ) ` k ) - ( F ` k ) ) = ( C - ( F ` k ) ) ) |
20 |
7 19
|
eqtr4d |
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( ( ZZ X. { C } ) ` k ) - ( F ` k ) ) ) |
21 |
1 2 12 5 3 18 6 20
|
climsub |
|- ( ph -> G ~~> ( C - A ) ) |