Olivier, maybe an approach for your problem could be to transform B into an expression C which looks like A (except that it has ( k - K ) instead of j) and then apply ~ fsumshft:
... 5 ? $? |- ( j = ( k - K ) -> A = C ) 6 1,2,3,4,5 fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) C ) 7 ? $? |- ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> C = B ) 8 7 sumeq2dv $p |- ( ph -> sum_ k e. ( ( M + K ) ... ( N + K ) ) C = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) 9 6,8 eqtrd $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) Example: Assume there is the following hypothesis for your theorem: ph -> A. k e. NN0 B = ( X + ( 2 - ( k - K ) ) ) To prove ( ph -> sum_ j e. ( M ... N ) ( X + ( 2 - j ) ) = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) you can choose C = ( X + ( 2 - ( k - K ) ) ). Then you can prove step 7 in the template above using the hypothesis, and afterwards you can prove step 5 easily, because it would become ( j = ( k - K ) -> ( X + ( 2 - j ) ) = ( X + ( 2 - ( k - K ) ) ) ). Maybe this helps, Alexander On Tuesday, October 29, 2019 at 11:03:50 PM UTC+1, Olivier Binda wrote: > > I have not grasped what I wanted (yet). But Thanks to your 3 answers, I > think that I understand a bit your point. > I will now have to ponder your answers a lot. There is a lot to think > about in here for me. I'll try to get it (real hard, because I really > really need this knowledge) > > Many thanks for your answers and for the kind help :) > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9d0977d3-9cb1-487a-82fa-7c271ecf0468%40googlegroups.com.
