Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpartlems.r |
|- R = { f | ( `' f " NN ) e. Fin } |
2 |
|
eulerpartlems.s |
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) ) |
3 |
2
|
a1i |
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) ) ) |
4 |
|
simplr |
|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> f = A ) |
5 |
4
|
fveq1d |
|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> ( f ` k ) = ( A ` k ) ) |
6 |
5
|
oveq1d |
|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> ( ( f ` k ) x. k ) = ( ( A ` k ) x. k ) ) |
7 |
6
|
sumeq2dv |
|- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) -> sum_ k e. NN ( ( f ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) ) |
8 |
|
id |
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> A e. ( ( NN0 ^m NN ) i^i R ) ) |
9 |
|
sumex |
|- sum_ k e. NN ( ( A ` k ) x. k ) e. _V |
10 |
9
|
a1i |
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. NN ( ( A ` k ) x. k ) e. _V ) |
11 |
3 7 8 10
|
fvmptd |
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) ) |