> Last theorem proved: > [...] > Nice challenge, I enjoyed it Congratulations! Despite being very busy with my own challenge I actually enjoyed watching this.
[email protected] schrieb am Sonntag, 15. Dezember 2024 um 01:16:55 UTC+1: > Last theorem proved: > > ${ > $d x y z a b c B $. $d x y z a b c .o. $. $d M a b c $. > > mendpadmbi.a $e |- B = ( Base ` M ) $. > mendpadmbi.b $e |- .o. = ( +g ` M ) $. > mendpadmbi.c $e |- B =/= (/) $. > mendpadmbi.d $e |- M e. Mgm $. > $( Boolean groups are characterized by an identiy of N.S. Mendelsohn and > R. Padmanabhan. $) > mendpadmbi $p |- ( A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. ( x > .o. ( z .o. y ) ) ) = z <-> ( M e. Abel /\ ( gEx ` M ) || 2 ) ) $= > ( va vb vc cv co wceq wral wcel oveq1 oveq2d cabl cgex cfv c2 cdvds > wbr c0g > wa wne a1i cmgm weq oveq12d eqeq1d 2ralbidv cbvralvw biimpi mendpadm > simpld > c0 mendpadmbilem4 jca cgrp wi simpl ablgrp grpass 3exp2 3syl > mendpadmbilem5 > imp41 ad3antrrr mgmcl mp3an1 oveq2 eqeq12d rspc2v sylan adantlll mpd > ablcom > id ad5ant145 3eqtr3rd ralrimiva cbvral3vw sylib impbii ) > ANZBNZFOZWICNZWJFO > > ZFOZFOZWLPZCDQBDQZADQZEUARZEUBUCUDUEUFZUHZWRWSWTWRWSKNZXBFOEUGUCPKDQWRKBCDE > > FGHDUTUIWRIUJEUKRZWRJUJWRXBWJFOZXBWMFOZFOZWLPZCDQBDQZKDQWQXHAKDAKULZWPXGBCD > > DXIWOXFWLXIWKXDWNXEFWIXBWJFSWIXBWMFSUMUNUOUPUQURUSABCDEFGHIJVAVBXAXBLNZFOZX > > BMNZXJFOZFOZFOZXLPZMDQZLDQZKDQWRXAXRKDXAXBDRZUHZXQLDXTXJDRZUHZXPMDYBXLDRZUH > > ZXKXKXLFOZFOZXKXBXJXLFOZFOZFOXLXOYDYEYHXKFXAXSYAYCYEYHPZXAWSEVCRZXSYAYCYIVD > > VDVDWSWTVEEVFYJXSYAYCYIDFEXBXJXLGHVGVHVIVKTYDWIWKFOZWJPZBDQADQZYFXLPZXAYMXS > > YAYCABDEFGHVJVLXSYAYCYMYNVDZXAXSYAUHXKDRZYCYOXCXSYAYPJDEXBXJFGHVMVNYLYNXKXK > > WJFOZFOZWJPABXKXLDDWIXKPZYKYRWJYSWIXKWKYQFYSWBWIXKWJFSUMUNBMULZYRYFWJXLYTYQ > > YEXKFWJXLXKFVOTYTWBVPVQVRVSVTYDYHXNXKFYDYGXMXBFWSYAYCYGXMPWTXSDFEXJXLGHWAWC > > TTWDWEWEWEXPWPWIXJFOZWIXMFOZFOZXLPWKWIXLWJFOZFOZFOZXLPKLMABCDDDKAULZXOUUCXL > > UUGXKUUAXNUUBFXBWIXJFSXBWIXMFSUMUNLBULZUUCUUFXLUUHUUAWKUUBUUEFXJWJWIFVOUUHX > > MUUDWIFXJWJXLFVOTUMUNMCULZUUFWOXLWLUUIUUEWNWKFUUIUUDWMWIFXLWLWJFSTTUUIWBVPW > FWGWH $. > $} > > I guess this is the end. Nice challenge, I enjoyed it. > -- 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/eed18b16-cf40-4b86-9696-ace5a9096cd3n%40googlegroups.com.
