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/db36ae74-48ab-6c3e-5b52-aecc0b59a7b7%40gmx.net.
$( <MM> <PROOF_ASST> THEOREM=for_Olivier_1 LOC_AFTER=?
10::1zzd |- ( x = 1 -> 1 e. ZZ )
20::0zd |- ( x = 1 -> 0 e. ZZ )
30::2z |- 2 e. ZZ
40:30:a1i |- ( x = 1 -> 2 e. ZZ )
50::2cnd |- ( ( x = 1 /\ k e. ( 0 ... 2 ) ) -> 2 e. CC )
60::elfzelz |- ( k e. ( 0 ... 2 ) -> k e. ZZ )
70:60:zcnd |- ( k e. ( 0 ... 2 ) -> k e. CC )
80:70:adantl |- ( ( x = 1 /\ k e. ( 0 ... 2 ) ) -> k e. CC )
90:50,80:mulcld |- ( ( x = 1 /\ k e. ( 0 ... 2 ) ) -> ( 2 x. k ) e. CC )
100::1cnd |- ( x = 1 -> 1 e. CC )
110::id |- ( x = 1 -> x = 1 )
120:110,100:eqeltrd |- ( x = 1 -> x e. CC )
130:120:adantr |- ( ( x = 1 /\ k e. ( 0 ... 2 ) ) -> x e. CC )
140:90,130:addcld |- ( ( x = 1 /\ k e. ( 0 ... 2 ) ) -> ( ( 2 x. k ) + x ) e.
CC )
150::oveq2 |- ( k = ( j - 1 ) -> ( 2 x. k ) = ( 2 x. ( j - 1 ) ) )
160:150:oveq1d |- ( k = ( j - 1 ) -> ( ( 2 x. k ) + x ) = ( ( 2 x. ( j - 1
) ) + x ) )
170:10,20,40,140,160:fsumshft
|- ( x = 1 -> sum_ k e. ( 0 ... 2 ) ( ( 2 x. k ) + x ) =
sum_ j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) ( ( 2 x. ( j - 1 ) ) + x ) )
180::0p1e1 |- ( 0 + 1 ) = 1
190::2p1e3 |- ( 2 + 1 ) = 3
200:180,190:oveq12i |- ( ( 0 + 1 ) ... ( 2 + 1 ) ) = ( 1 ... 3 )
210:200:a1i |- ( x = 1 -> ( ( 0 + 1 ) ... ( 2 + 1 ) ) = ( 1 ... 3 ) )
220::elfzelz |- ( j e. ( ( 0 + 1 ) ... ( 2 + 1 ) ) -> j e. ZZ )
230::2cnd |- ( j e. ZZ -> 2 e. CC )
240::zcn |- ( j e. ZZ -> j e. CC )
250:230,240:muls1d |- ( j e. ZZ -> ( 2 x. ( j - 1 ) ) = ( ( 2 x. j ) - 2 ) )
260:250:oveq1d |- ( j e. ZZ -> ( ( 2 x. ( j - 1 ) ) + 1 ) = ( ( ( 2 x. j )
- 2 ) + 1 ) )
270::oveq2 |- ( x = 1 -> ( ( 2 x. ( j - 1 ) ) + x ) = ( ( 2 x. ( j - 1
) ) + 1 ) )
280:110,110:oveq12d |- ( x = 1 -> ( x x. x ) = ( 1 x. 1 ) )
290:280:oveq2d |- ( x = 1 -> ( ( 2 x. j ) - ( x x. x ) ) = ( ( 2 x. j ) -
( 1 x. 1 ) ) )
300:270,290:eqeq12d |- ( x = 1 -> ( ( ( 2 x. ( j - 1 ) ) + x ) = ( ( 2 x. j ) -
( x x. x ) ) <-> ( ( 2 x. ( j - 1 ) ) + 1 ) = ( ( 2 x. j ) - ( 1 x. 1 ) ) ) )
310:300:adantr |- ( ( x = 1 /\ j e. ZZ ) -> ( ( ( 2 x. ( j - 1 ) ) + x ) =
( ( 2 x. j ) - ( x x. x ) ) <-> ( ( 2 x. ( j - 1 ) ) + 1 ) = ( ( 2 x. j ) - ( 1
x. 1 ) ) ) )
320::1t1e1 |- ( 1 x. 1 ) = 1
330:320:a1i |- ( j e. ZZ -> ( 1 x. 1 ) = 1 )
340:330:oveq2d |- ( j e. ZZ -> ( ( 2 x. j ) - ( 1 x. 1 ) ) = ( ( 2 x. j )
- 1 ) )
350:230,240:mulcld |- ( j e. ZZ -> ( 2 x. j ) e. CC )
360::1cnd |- ( j e. ZZ -> 1 e. CC )
370:350,230,360:subadd23d
|- ( j e. ZZ -> ( ( ( 2 x. j ) - 2 ) + 1 ) = ( ( 2 x. j ) +
( 1 - 2 ) ) )
380::ax-1cn |- 1 e. CC
390::2cn |- 2 e. CC
400:390,380:negsubdi2i |- -u ( 2 - 1 ) = ( 1 - 2 )
410::2m1e1 |- ( 2 - 1 ) = 1
420:410:negeqi |- -u ( 2 - 1 ) = -u 1
430:400,420:eqtr3i |- ( 1 - 2 ) = -u 1
440:430:oveq2i |- ( ( 2 x. j ) + ( 1 - 2 ) ) = ( ( 2 x. j ) + -u 1 )
450:440:a1i |- ( j e. ZZ -> ( ( 2 x. j ) + ( 1 - 2 ) ) = ( ( 2 x. j ) +
-u 1 ) )
460:350,360:negsubd |- ( j e. ZZ -> ( ( 2 x. j ) + -u 1 ) = ( ( 2 x. j ) - 1 ) )
470:370,450,460:3eqtrd |- ( j e. ZZ -> ( ( ( 2 x. j ) - 2 ) + 1 ) = ( ( 2 x. j
) - 1 ) )
480:470,260,340:3eqtr4d |- ( j e. ZZ -> ( ( 2 x. ( j - 1 ) ) + 1 ) = ( ( 2 x. j
) - ( 1 x. 1 ) ) )
490:480:adantl |- ( ( x = 1 /\ j e. ZZ ) -> ( ( 2 x. ( j - 1 ) ) + 1 ) = (
( 2 x. j ) - ( 1 x. 1 ) ) )
500:490,310:mpbird |- ( ( x = 1 /\ j e. ZZ ) -> ( ( 2 x. ( j - 1 ) ) + x ) = (
( 2 x. j ) - ( x x. x ) ) )
510:220,500:sylan2 |- ( ( 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 ) ) )
$= ( cv c1 wceq cc0 c2 cfz co cmul caddc csu cmin c3 cz wcel a1i wa cc 1zzd 2z
0zd 2cnd elfzelz zcnd adantl mulcld 1cnd eqeltrd adantr addcld oveq2 oveq1d
fsumshft 0p1e1 2p1e3 oveq12i cneg zcn subadd23d 2cn ax-1cn negsubdi2i 2m1e1
id negeqi eqtr3i oveq2i negsubd 3eqtrd muls1d 1t1e1 3eqtr4d oveq12d eqeq12d
oveq2d wb mpbird sylan2 sumeq12dv eqtrd ) ADZEFZGHIJZHCDZKJZWCLJZCMGELJZHEL
JZIJZHBDZENJZKJZWCLJZBMEOIJZHWLKJZWCWCKJZNJZBMWDWHWOCBEGHWDUAWDUCHPQWDUBRWD
WFWEQZSZWGWCXAHWFXAUDWTWFTQWDWTWFWFGHUEUFUGUHWDWCTQWTWDWCETWDVFZWDUIUJUKULW
FWMFWGWNWCLWFWMHKUMUNUOWDWKWPWOWSBWKWPFWDWIEWJOIUPUQURRWLWKQWDWLPQZWOWSFZWL
WIWJUEWDXCSXDWNELJZWQEEKJZNJZFZXCXHWDXCWQHNJZELJZWQENJZXEXGXCXJWQEHNJZLJZWQ
EUSZLJZXKXCWQHEXCHWLXCUDZWLUTZUHZXPXCUIZVAXMXOFXCXLXNWQLHENJZUSXLXNHEVBVCVD
XTEVEVGVHVIRXCWQEXRXSVJVKXCWNXIELXCHWLXPXQVLUNXCXFEWQNXFEFXCVMRVQVNUGWDXDXH
VRXCWDWOXEWSXGWCEWNLUMWDWRXFWQNWDWCEWCEKXBXBVOVQVPUKVSVTWAWB $.
$d j k x
$)
