metamath/valid/amc12b-2004-p3.mm (53 lines of code) (raw):

${ amc12b-2004-p3.0 $e |- ( ph -> X e. NN ) $. amc12b-2004-p3.1 $e |- ( ph -> Y e. NN ) $. amc12b-2004-p3.2 $e |- ( ph -> ( ( 2 ^ X ) x. ( 3 ^ Y ) ) = ; ; ; 1 2 9 6 ) $. $( (Contributed by Stanislas Polu, 26-Nov-2020.) $) amc12b-2004-p3 $p |- ( ph -> ( X + Y ) = 8 ) $= ( caddc co c4 c8 c2 c1 c6 cpc c3 cc0 wcel wceq a1i eqtrd c9 cexp cmul nncnd cdc addid1d eqcomd cprime cz 2prm nnzd pcid sylancr cdvds wbr wn cgcd 2z cn 3nn nnnn0d nnexpcld gcdcom wne 2re 2lt3 gtneii wb 3prm prmrp sylancl mpbird wi 2nn rplpwr syl3anc mpd coprm pceq0 oveq12d wa nnne0d jca pcmul 8nn0 1nn0 oveq2d 6nn0 4nn0 ax-frege54c nn0cni mulid2i 0nn0 8cn 8t6e48 mulcomli oveq1i deccl 6cn addid1i eqtri mulid1i dec0h decmul2c 8p4e12 ax-1cn 8p1e9 addcomli decadd decm1mma 2exp4 eqcomi c7 3cn 3nn0 3p1e4 3exp3 2nn0 2cn 3t2e6 nnexpcl 7nn0 mp2an nnne0i zexpcl 3z cmin dvdsmul1 4cn breqtrd subaddrii m1dvdsndvds oveq1d syl2anc addid2d c5 5nn 5cn decnncl nncni 6p2e8 7t3e21 decmul1c jctil expp1i cn0 mpan2 mp1i jctir nn0zi 4t2e8 2t0e0 addid2i 1p0e1 nnzi 5t3e15 6nn 4z 5nn0 0p1e1 5p1e6 cc 4p4e8 ) ABCGHIIGHZJABICIGABKLKUEZUAUEZMUEZNHZIABKKBU BHZOCUBHZUCHZNHZUVHABKUVINHZKUVJNHZGHZUVLABBPGHZUVOAUVPBABABDUDUFUGABUVMPUV NGAUVMBAKUHQZBUIQUVMBRUJABDUKBKULUMUGAUVNPAUVNPRZKUVJUNUOUPZAUVSKUVJUQHZLRZ AUVTUVJKUQHZLAKUIQZUVJUIQZUVTUWBRURAUVJAOCOUSQZAUTSZACEVAVBZUKZKUVJVCUMAOKU QHZLRZUWBLRZAUWJOKVDZUWLAKOVEVFVGSAOUHQZUVQUWJUWLVHUWMAVISZUJOKVJVKVLZAUWEK USQZCUSQUWJUWKVMUWFUWPAVNSZEOKCVOVPVQTAUVQUWDUVSUWAVHUJUWHKUVJVRUMVLAUVQUVJ USQUVRUVSVHUJUWGKUVJVSUMVLUGVTTAUVLUVOAUVQUVIUIQZUVIPVDZWAZUWDUVJPVDZWAZUVL UVORUVQAUJSZAUWRUWSAUVIAKBUWQABDVAVBZUKZAUVIUXDWBWCZAUWDUXAUWHAUVJUWGWBWCZU VIUVJKWDVPUGTAUVKUVGKNFWGTAUVHKKIUBHZOIUBHZUCHZNHZIAUVGUXJKNAUVGLMUEZJLUEZU CHZUXJAUXNUVGUXNUVGRAUXLUXMUVFMLMUXMIJUEZUXOMUEZJLWEWFWRZWHWFWHIJWIWEWRZUXL WJUXPWJUXMUXMUXQWKZWLJLUXOMMPUXMWHWEWFUXMWJZWHWMMJUCHZPGHUXOPGHUXOUYAUXOPGJ MUXOWNWSWOWPWQUXOUXOUXRWKWTXAMLUCHMPMUEMWSXBMWHXCXAXDJLIJUVEUAUXMUXOWEWFWIW EUXTUXOWJXEJLUAWNXFXGXHXIXJSUGAUXLUXHUXMUXIUCUXLUXHRAUXHUXLXKXLSZUXMUXIRAUX IUXMOUXMKXMUEZOIXNXOXPXQKXMJLOKUYCXOXRYBUYCWJWFXRKOUCHZKGHMKGHJUYDMKGOKMXNX SXTWPWQUUAXAUUBUUCUUEXLSZVTTZWGAUXKKUXHNHZKUXINHZGHZIAUVQUXHUIQZUXHPVDZWAZU XIUIQZUXIPVDZWAZUXKUYIRUXCAUYKUYJUYKAUXHUWPIUUFQZUXHUSQZVNWIKIYAYCZYDSUWCUY PUYJURWIKIYEYCUUDZAUYMUYNOUIQZUYMAYFUYTUYPUYMWIOIYEUUGUUHZUXIUWEUYPUXIUSQZU TWIOIYAYCZYDUUIZUXHUXIKWDVPAUYIIPGHZIAUYGIUYHPGAUVQIUIQZUYGIRUJVUFAUURSZIKU LUMAUYHPRZKUXIUNUOUPZAKUXILYGHZUNUOZVUIAKJPUEZVUJUNAKKIPUEZUCHZVULUNAUWCVUM UIQZKVUNUNUOURVUOAVUMIPWIWMWRUUJSKVUMYHUMVUNVULRAIPJPKPVUMXRWIWMVUMWJWMWMKI UCHZPGHJPGHJVUPJPGIKJYIXSUUKWPWQJWNWTXAKPUCHPPPUEUULPWMXCXAXDSYJAVULUXMLYGH ZVUJAVUQVULVUQVULRAUXMLVULUXSXFVULJPWEWMWRWKPLJPJLLVULWMWFWEWMLWFXCZVULWJJW NUUMUUNXIYKSUGAUXMUXILYGUYEYMTYJAUVQUYMVUKVUIVMUXCVUAUXIKYLYNVQAUVQVUBVUHVU IVHUJVUBAVUCSKUXIVSUMVLVTVUEIRAIYIWTSTTTTACOUVGNHZIACOUVKNHZVUSACOUVINHZOUV JNHZGHZVUTACPCGHZVVCAVVDCACACEUDYOUGAPVVACVVBGAVVAPAVVAPRZOUVIUNUOUPZAVVFOU VIUQHZLRZAVVGUVIOUQHZLAUYTUWRVVGVVIRYFUXEOUVIVCUMAKOUQHZLRZVVILRZAVVJUWILAU WCUYTVVJUWIRURUYTAYFSKOVCUMUWOTAUWPUWEBUSQVVKVVLVMUWQUWFDKOBVOVPVQTAUWMUWRV VFVVHVHVIUXEOUVIVRUMVLAUWMUVIUSQVVEVVFVHUWNUXDOUVIVSYNVLUGAVVBCAUWMCUIQVVBC RVIACEUKCOULUMUGVTTAVUTVVCAUWMUWTUXBVUTVVCRUWNUXFUXGUVIUVJOWDVPUGTAUVKUVGON FWGTAVUSOUXJNHZIAUVGUXJONUYFWGAVVMOUXHNHZOUXINHZGHZIAUWMUYLUYOVVMVVPRUWNUYS VUDUXHUXIOWDVPAVVPPIGHIAVVNPVVOIGAVVNPRZOUXHUNUOUPZAOUXHLYGHZUNUOZVVRAOLYPU EZVVSUNAOOYPUCHZVWAUNAUYTYPUIQZOVWBUNUOYFVWCAYPYQUUOSOYPYHUMVWBVWARAYPOVWAY RXNUUPWPSYJAVWAUXLLYGHZVVSVWAVWDRAVWDVWAUXLLVWAUXLLMWFUUQYSYTXFVWALYPWFYQYS YTPLLYPLMLVWAWMWFWFUUSVURVWAWJUUTYPLMYRXFUVAXHXIYKXLSAUXLUXHLYGUYBYMTYJAUWM UYJVVTVVRVMUWNAUXHUYQAUYRSZUKUXHOYLYNVQAUWMUYQVVQVVRVHVIVWEOUXHVSUMVLAUWMVU FVVOIRVIVUGIOULUMVTAIIUVBQAYISYOTTTTVTUVDJRAUVCST $. $}