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/27f7b052-78a8-4b02-b269-0e817bb9bb65n%40googlegroups.com.
