Thank you for the detailed reply!
I definitely agree that uncompressed proofs are crucial. However, I still think syntax will remain a challenge for most LLMs, simply because Metamath is a low-resource language — it's underrepresented in training data compared to, for example, Python. So even if we provide clean proof traces, models might still fail to interpret them correctly unless they’ve seen enough Metamath-like structure during pretraining. However, I’ve been watching the reasoning abilities of state-of-the-art LLMs like ChatGPT, and I think we’re getting close to the point where models can “absorb” the Metamath rules on the fly, even without prior exposure - just by pattern recognition, structural reasoning, etc - how human behave. So maybe this will become less of an issue soon thanks to the models' growing "intelligence". I like the idea of training backward from the goal - I’ll try experimenting with that. Thanks again for your thoughts, very helpful! среда, 23 апреля 2025 г. в 22:18:47 UTC+7, David A. Wheeler: > > > > On Apr 22, 2025, at 1:07 PM, Pavel Kamenev <[email protected]> wrote: > > > > About a year and a half ago I dove into the Metamath system with the > goal of creation of LLM-based automatical theorem proover. I had trouble > with the fact that Metamath seemed to be under-represented in the training > sets of Chat-GPT and others, and so its syntax and proof semantics were > hard for the models to understand. I solved this by rewriting mmverify.py > to map Metamath’s floating and essential hypotheses, assertions, and proof > steps to executable Python classes. It seemed reasonable to me to share > these intermediate results and publish a short article, dataset and source > code. > > That's an interesting approach, thanks for sharing it! > > I've also been thinking about this, though from a different angle: > > 1. LLMs struggle with compressed proofs; it's important to provide > *uncompressed* proofs in training sets. > 2. In theory the LLM could simply output the proof steps, but I think they > need the intermediate results so they have more information to "work with" > to verify that they're going the right way. > 3. LLMs struggle to produce specific "final results". I speculate that > training going *backwards*, starting from the final goal, will produce a > better-working result. > 4. Instead of Python-looking, I think it'd be more effective to use > something like metamath set.mm; set scroll continuous; show proof > fsumdvdsmul /reverse and omit the step numbers. What I have in mind is > below. > > --- David A. Wheeler > > > === EXAMPLE === > > > > > 801 fsumdvdsmul=3eqtrd $p |- ( ph -> ( sum_ j e. X A x. sum_ k e. > Y B ) = sum_ i e. Z C ) > 800 3eqtrd.3=3eqtr4a $p |- ( ph -> sum_ j e. X sum_ k e. Y D = > sum_ i e. Z C ) > 799 3eqtr4a.3=eqtrid $p |- ( ph -> sum_ i e. Z C = sum_ z e. > ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) > 798 eqtrid.2=fsumf1o $p |- ( ph -> sum_ w e. Z [_ w / i ]_ > C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / > i ]_ > C ) > 797 fsumf1o.5=r19.21bi $p |- ( ( ph /\ w e. Z ) -> [_ w / > i ]_ C e. CC ) > 796 r19.21bi.1=mpbid $p |- ( ph -> A. w e. Z [_ w / i > ]_ C e. CC ) > 795 mpbid.maj=bitr3id $p |- ( ph -> ( A. z e. ( X X. > Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC <-> A. > w e. > Z [_ w / i ]_ C e. CC ) ) > 794 bitr3id.2=raleqdv $p |- ( ph -> ( A. w e. ( ( x > e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. > w e. > Z [_ w / i ]_ C e. CC ) ) > 793 raleqdv.1=eqtrid $p |- ( ph -> ( ( x e. CC , > y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) = Z ) > 792 eqtrid.2=3syl $p |- ( ph -> ran ( ( x > e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z ) > 791 3syl.3=forn $p |- ( ( ( x e. CC , y > e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z -> ran ( ( x > e. > CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z ) > 787 3syl.2=f1ofo $p |- ( ( ( x e. CC , y > e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z -> ( ( x > e. > CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z ) > 783 3syl.1=528 $p |- ( ph -> ( ( x e. > CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z ) > 770 eqtrid.1=df-ima $a |- ( ( x e. CC , y e. > CC |-> ( x x. y ) ) " ( X X. Y ) ) = ran ( ( x e. CC , y e. CC |-> ( x x. > y ) ) > |` ( X X. Y ) ) > 757 bitr3id.1=mp2an $p |- ( A. w e. ( ( x e. CC , > y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( > X X. > Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) > 756 mp2an.3=ralima $p |- ( ( ( x e. CC , y e. > CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( > A. w > e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. > CC > <-> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i > ]_ C > e. CC ) ) > 755 rexima.x=eleq1d $p |- ( w = ( ( x e. CC , > y e. CC |-> ( x x. y ) ) ` z ) -> ( [_ w / i ]_ C e. CC <-> [_ ( ( x e. CC > , y > e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) > 754 eleq1d.1=499 $p |- ( w = ( ( x e. CC > , y e. CC |-> ( x x. y ) ) ` z ) -> [_ w / i ]_ C = [_ ( ( x e. CC , y e. > CC > |-> ( x x. y ) ) ` z ) / i ]_ C ) > 740 mp2an.2=mp2an $p |- ( X X. Y ) C_ ( CC X. > CC ) > 739 mp2an.3=xpss12 $p |- ( ( X C_ CC /\ Y C_ > CC ) -> ( X X. Y ) C_ ( CC X. CC ) ) > 734 mp2an.2=332 $p |- Y C_ CC > 733 mp2an.1=317 $p |- X C_ CC > 725 mp2an.1=ax-mp $a |- ( x e. CC , y e. CC > |-> ( x x. y ) ) Fn ( CC X. CC ) > 724 maj=ffn $p |- ( ( x e. CC , y e. > CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC -> ( x e. CC , y e. CC |-> ( x > x. y ) > ) Fn ( CC X. CC ) ) > 720 min=mpomulf $p |- ( x e. CC , y e. CC > |-> ( x x. y ) ) : ( CC X. CC ) --> CC > 692 mpbid.min=syl $p |- ( ph -> A. z e. ( X X. Y > ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) > 691 syl.2=sylbi $p |- ( A. z e. ( X X. Y ) [_ > ( x. ` z ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC > |-> ( > x x. y ) ) ` z ) / i ]_ C e. CC ) > 690 sylbi.2=ralrimiv $p |- ( A. w e. ( X X. Y ) > [_ ( x. ` w ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. > CC |-> > ( x x. y ) ) ` z ) / i ]_ C e. CC ) > 689 ralrimiv.1=com12 $p |- ( A. w e. ( X X. Y > ) [_ ( x. ` w ) / i ]_ C e. CC -> ( z e. ( X X. Y ) -> [_ ( ( x e. CC , y > e. CC > |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) > 688 com12.1=rspcdv $p |- ( z e. ( X X. Y ) > -> ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> [_ ( ( x e. CC , y > e. > CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) > 687 rspcdv.2=bitr3d $p |- ( ( z e. ( X X. > Y ) /\ w = z ) -> ( [_ ( x. ` w ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. > CC > |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) > 686 bitr3d.2=adantr $p |- ( ( z e. ( X > X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y > e. > CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) > 685 adantr.1=eleq1d $p |- ( z e. ( X > X. Y ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> > ( x > x. y ) ) ` z ) / i ]_ C e. CC ) ) > 684 eleq1d.1=369 $p |- ( z e. ( > X X. Y ) -> [_ ( x. ` z ) / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y > ) ) > ` z ) / i ]_ C ) > 674 bitr3d.1=eleq1d $p |- ( ( z e. ( X > X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i > ]_ C > e. CC ) ) > 673 eleq1d.1=adantl $p |- ( ( z e. ( > X X. Y ) /\ w = z ) -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) > 672 adantl.1=eqcoms $p |- ( w = z > -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) > 671 eqcoms.1=633 $p |- ( z = w > -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) > 650 rspcdv.1=id $p |- ( z e. ( X X. Y > ) -> z e. ( X X. Y ) ) > 635 sylbi.1=cbvralvw $p |- ( A. z e. ( X X. Y ) > [_ ( x. ` z ) / i ]_ C e. CC <-> A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C > e. > CC ) > 634 cbvralvw.1=eleq1d $p |- ( z = w -> ( [_ ( > x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i ]_ C e. CC ) ) > 633 633:eleq1d.1=csbeq1d $p |- ( z = w -> [_ ( > x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) > 632 csbeq1d.1=fveq2 $p |- ( z = w -> ( x. > ` z ) = ( x. ` w ) ) > 599 syl.1=sylibr $p |- ( ph -> A. z e. ( X X. > Y ) [_ ( x. ` z ) / i ]_ C e. CC ) > 598 sylibr.2=ralxp $p |- ( A. z e. ( X X. Y ) > [_ ( x. ` z ) / i ]_ C e. CC <-> A. j e. X A. k e. Y D e. CC ) > 597 ralxp.1=eleq1d $p |- ( z = <. j , k >. > -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> D e. CC ) ) > 596 eleq1d.1=424 $p |- ( z = <. j , k >. > -> [_ ( x. ` z ) / i ]_ C = D ) > 584 sylibr.1=ralrimivva $p |- ( ph -> A. j e. X A. > k e. Y D e. CC ) > 583 ralrimivva.1=454 $p |- ( ( ph /\ ( j e. X > /\ k e. Y ) ) -> D e. CC ) > 540 fsumf1o.4=adantl $p |- ( ( ph /\ z e. ( X X. Y ) ) > -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x > e. CC > , y e. CC |-> ( x x. y ) ) ` z ) ) > 539 adantl.1=fvres $p |- ( z e. ( X X. Y ) -> ( ( ( > x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x e. CC , y > e. > CC |-> ( x x. y ) ) ` z ) ) > 528 528:fsumf1o.3=mpodvdsmulf1o $p |- ( ph -> ( ( x e. CC , y e. CC > |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z ) > 527 mpodvdsmulf1o.z=mpodvdsmulf1o.z $e |- Z = { x e. NN | x || ( M x. > N ) } > 526 mpodvdsmulf1o.y=mpodvdsmulf1o.y $e |- Y = { x e. NN | x || N } > 525 mpodvdsmulf1o.x=mpodvdsmulf1o.x $e |- X = { x e. NN | x || M } > 524 mpodvdsmulf1o.3=mpodvdsmulf1o.3 $e |- ( ph -> ( M gcd N ) = 1 ) > 523 mpodvdsmulf1o.2=mpodvdsmulf1o.2 $e |- ( ph -> N e. NN ) > 522 mpodvdsmulf1o.1=mpodvdsmulf1o.1 $e |- ( ph -> M e. NN ) > 513 fsumf1o.2=syl2anc $p |- ( ph -> ( X X. Y ) e. Fin ) > 512 syl2anc.3=xpfi $p |- ( ( X e. Fin /\ Y e. Fin ) > -> ( X X. Y ) e. Fin ) > 509 syl2anc.2=109 $p |- ( ph -> Y e. Fin ) > 508 syl2anc.1=70 $p |- ( ph -> X e. Fin ) > 499 499:fsumf1o.1=csbeq1 $p |- ( w = ( ( x e. CC , y e. CC > |-> ( x x. y ) ) ` z ) -> [_ w / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x > x. y > ) ) ` z ) / i ]_ C ) > 483 eqtrid.1=cbvsumi $p |- sum_ i e. Z C = sum_ w e. Z [_ > w / i ]_ C > 482 cbvsumi.3=csbeq1a $p |- ( i = w -> C = [_ w / i ]_ C > ) > 478 cbvsumi.2=nfcsb1v $p |- F/_ i [_ w / i ]_ C > 474 cbvsumi.1=nfcv $p |- F/_ w C > 455 3eqtr4a.2=fsumxp $p |- ( ph -> sum_ j e. X sum_ k e. Y D > = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C ) > 454 454:fsumxp.4=eqeltrrd $p |- ( ( ph /\ ( j e. X /\ k e. Y ) > ) -> D e. CC ) > 453 eqeltrrd.2=mulcld $p |- ( ( ph /\ ( j e. X /\ k e. Y > ) ) -> ( A x. B ) e. CC ) > 452 addcld.2=adantrl $p |- ( ( ph /\ ( j e. X /\ k e. > Y ) ) -> B e. CC ) > 451 adant2.1=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B > e. CC ) > 446 addcld.1=adantrr $p |- ( ( ph /\ ( j e. X /\ k e. > Y ) ) -> A e. CC ) > 445 adant2.1=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A > e. CC ) > 435 eqeltrrd.1=fsumdvdsmul.6 $e |- ( ( ph /\ ( j e. X /\ k e. Y > ) ) -> ( A x. B ) = D ) > 426 fsumxp.3=109 $p |- ( ph -> Y e. Fin ) > 425 fsumxp.2=70 $p |- ( ph -> X e. Fin ) > 424 424:fsumxp.1=eqtrdi $p |- ( z = <. j , k >. -> [_ ( x. ` > z ) / i ]_ C = D ) > 423 eqtrdi.2=csbie $p |- [_ ( j x. k ) / i ]_ C = D > 422 csbie.2=fsumdvdsmul.7 $e |- ( i = ( j x. k ) -> C = D ) > 421 csbie.1=ovex $p |- ( j x. k ) e. _V > 413 eqtrdi.1=csbeq1d $p |- ( z = <. j , k >. -> [_ ( x. > ` z ) / i ]_ C = [_ ( j x. k ) / i ]_ C ) > 412 csbeq1d.1=eqtr4di $p |- ( z = <. j , k >. -> ( x. ` > z ) = ( j x. k ) ) > 411 eqtr4di.2=df-ov $a |- ( j x. k ) = ( x. ` <. j > , k >. ) > 407 eqtr4di.1=fveq2 $p |- ( z = <. j , k >. -> ( x. > ` z ) = ( x. ` <. j , k >. ) ) > 370 3eqtr4a.1=sumeq2i $p |- sum_ z e. ( X X. Y ) [_ ( x. ` z > ) / i ]_ C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) > ) ` z > ) / i ]_ C > 369 369:sumeq2i.1=csbeq1d $p |- ( z e. ( X X. Y ) -> [_ ( x. ` > z ) / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) > 368 csbeq1d.1=eqcomd $p |- ( z e. ( X X. Y ) -> ( x. ` z > ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) > 367 eqcomd.1=syl $p |- ( z e. ( X X. Y ) -> ( ( x > e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) > 366 syl.2=exlimivv $p |- ( E. u E. v ( z = <. u , > v >. /\ ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` > z ) > = ( x. ` z ) ) > 365 exlimivv.1=impel $p |- ( ( z = <. u , v >. /\ > ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( > x. ` > z ) ) > 364 impel.2=syl2an $p |- ( ( u e. X /\ v e. Y > ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u > , v > >. ) ) > 363 syl2an.3=3eqtr3g $p |- ( ( u e. CC /\ v e. > CC ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. > u , > v >. ) ) > 362 3eqtr3g.3=df-ov $a |- ( u x. v ) = ( x. > ` <. u , v >. ) > 358 3eqtr3g.2=df-ov $a |- ( u ( x e. CC , y > e. CC |-> ( x x. y ) ) v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u > , v > >. ) > 354 3eqtr3g.1=ovmpot $p |- ( ( u e. CC /\ v > e. CC ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( u x. v ) ) > 333 syl2an.2=sseli $p |- ( v e. Y -> v e. CC > ) > 332 332:sseli.1=sstri $p |- Y C_ CC > 331 sstri.2=nnsscn $p |- NN C_ CC > 330 sstri.1=ssrab3 $p |- Y C_ NN > 329 ssrab3.1=mpodvdsmulf1o.y $e |- Y = { x e. NN > | x || N } > 318 syl2an.1=sseli $p |- ( u e. X -> u e. CC > ) > 317 317:sseli.1=sstri $p |- X C_ CC > 316 sstri.2=nnsscn $p |- NN C_ CC > 315 sstri.1=ssrab3 $p |- X C_ NN > 314 ssrab3.1=mpodvdsmulf1o.x $e |- X = { x e. NN > | x || M } > 294 impel.1=biimpd $p |- ( z = <. u , v >. -> > ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v > >. ) > -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) ) > 293 biimpd.1=eqeq12d $p |- ( z = <. u , v >. > -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u > , v > >. ) <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) ) > 292 eqeq12d.2=eqcoms $p |- ( z = <. u , v >. > -> ( x. ` <. u , v >. ) = ( x. ` z ) ) > 291 eqcoms.1=fveq2 $p |- ( <. u , v >. = > z -> ( x. ` <. u , v >. ) = ( x. ` z ) ) > 282 eqeq12d.1=eqcoms $p |- ( z = <. u , v >. > -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC , > y e. > CC |-> ( x x. y ) ) ` z ) ) > 281 eqcoms.1=fveq2 $p |- ( <. u , v >. = > z -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC > , y > e. CC |-> ( x x. y ) ) ` z ) ) > 250 syl.1=elxpi $p |- ( z e. ( X X. Y ) -> E. u > E. v ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) ) > 174 3eqtrd.2=sumeq2dv $p |- ( ph -> sum_ j e. X ( A x. sum_ k > e. Y B ) = sum_ j e. X sum_ k e. Y D ) > 173 sumeq2dv.1=eqtrd $p |- ( ( ph /\ j e. X ) -> ( A x. sum_ > k e. Y B ) = sum_ k e. Y D ) > 172 eqtrd.2=sumeq2dv $p |- ( ( ph /\ j e. X ) -> sum_ k e. > Y ( A x. B ) = sum_ k e. Y D ) > 171 sumeq2dv.1=anassrs $p |- ( ( ( ph /\ j e. X ) /\ k e. > Y ) -> ( A x. B ) = D ) > 170 anassrs.1=fsumdvdsmul.6 $e |- ( ( ph /\ ( j e. X /\ k e. > Y ) ) -> ( A x. B ) = D ) > 158 eqtrd.1=fsummulc2 $p |- ( ( ph /\ j e. X ) -> ( A x. > sum_ k e. Y B ) = sum_ k e. Y ( A x. B ) ) > 157 fsummulc2.3=adantlr $p |- ( ( ( ph /\ j e. X ) /\ k e. > Y ) -> B e. CC ) > 156 adant2.1=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B e. > CC ) > 146 fsummulc2.2=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A e. CC > ) > 145 fsummulc2.1=adantr $p |- ( ( ph /\ j e. X ) -> Y e. > Fin ) > 144 adantr.1=109 $p |- ( ph -> Y e. Fin ) > 113 3eqtrd.1=fsummulc1 $p |- ( ph -> ( sum_ j e. X A x. sum_ k > e. Y B ) = sum_ j e. X ( A x. sum_ k e. Y B ) ) > 112 fsummulc2.3=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A e. CC ) > 111 fsummulc2.2=fsumcl $p |- ( ph -> sum_ k e. Y B e. CC ) > 110 fsumcl.2=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B e. CC ) > 109 109:fsumcl.1=ssfid $p |- ( ph -> Y e. Fin ) > 108 ssfid.2=eqsstrid $p |- ( ph -> Y C_ ( 1 ... N ) ) > 107 eqsstrid.2=syl $p |- ( ph -> { x e. NN | x || N > } C_ ( 1 ... N ) ) > 106 syl.2=dvdsssfz1 $p |- ( N e. NN -> { x e. NN | > x || N } C_ ( 1 ... N ) ) > 103 syl.1=mpodvdsmulf1o.2 $e |- ( ph -> N e. NN ) > 95 eqsstrid.1=mpodvdsmulf1o.y $e |- Y = { x e. NN | x || N } > 84 ssfid.1=fzfid $p |- ( ph -> ( 1 ... N ) e. Fin ) > 70 70:fsummulc2.1=ssfid $p |- ( ph -> X e. Fin ) > 69 ssfid.2=eqsstrid $p |- ( ph -> X C_ ( 1 ... M ) ) > 68 eqsstrid.2=syl $p |- ( ph -> { x e. NN | x || M } > C_ ( 1 ... M ) ) > 67 syl.2=dvdsssfz1 $p |- ( M e. NN -> { x e. NN | x > || M } C_ ( 1 ... M ) ) > 64 syl.1=mpodvdsmulf1o.1 $e |- ( ph -> M e. NN ) > 56 eqsstrid.1=mpodvdsmulf1o.x $e |- X = { x e. NN | x || M } > 44 ssfid.1=fzfid $p |- ( ph -> ( 1 ... M ) e. Fin ) -- 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 visit https://groups.google.com/d/msgid/metamath/0fc1c358-4e81-487e-8fc2-6f55ace3c5e8n%40googlegroups.com.
