Thank you Thierry for the illustration. You can indeed do that. I'm guessing that the first step uses fsumshft without antecedent, that are later added with ps |- (ph -> ps )
It helps but I am not sure that it will solve my issue : I'm writing an ide/system where the user will be provided with ( ph -> ( j = ( k - K ) -> A = B ) ) where ph may be anything (it depends on what changes the user would have done in other parts of a statement) and so, the system would have to use first fsumshift, then add antecedents with ps |- (ph -> ps ) and then do the appropriate steps (without human intervention/help) that you did with mmj2 (I'm guessing) It might be possible and your illustration shows the way. I'll look into it. That would remove now, my need for a Mephistolus-friendly variant of fsumshift and also resolve the issues I would have in identical situations with other theorems. Thank you for the tip :) Le mercredi 30 octobre 2019 14:14:29 UTC+1, Thierry Arnoux a écrit : > > Hi Olivier, > > To illustrate Alexander's explanation with your example, I attach a proof > of your statement in set.mm: > > |- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x ) = sum_ j e. ( 1 ... > 3 ) ( ( 2 x. j ) - ( x x. x ) ) > > The main steps are following Alexander's model: > > 170::fsumshft |- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x > ) = sum_ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ( ( 2 x. ( j - 1 ) ) + x ) ) > 210:: |- ( x = 1 -> ( ( 0 + 1 ) ... ( 2 + 1 ) ) = ( 1 ... > 3 ) ) > 510:: |- ( ( x = 1 /\ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ) > -> ( ( 2 x. ( j - 1 ) ) + x ) = ( ( 2 x. j ) - ( x x. x ) ) ) > 520:210,510:sumeq12dv |- ( x = 1 -> sum_ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) > ( ( 2 x. ( j - 1 ) ) + x ) = sum_ j e. ( 1 ... 3 ) ( ( 2 x. j ) - ( x x. x > ) ) ) > qed:170,520:eqtrd |- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x > ) = sum_ j e. ( 1 ... 3 ) ( ( 2 x. j ) - ( x x. x ) ) ) > > BR, > _ > Thierry > -- 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/683ae61a-3887-4580-922c-39329402f07d%40googlegroups.com.
