metamath/valid/induction-divisibility-3divnto3m2n.mm (43 lines of code) (raw):

${ $d N x $. $d ph x y $. induction-divisibility-3divnto3m2n.0 $e |- ( ph -> N e. NN0 ) $. $( (Contributed by Stanislas Polu, 9-Oct-2020.) $) induction-divisibility-3divnto3m2n $p |- ( ph -> 3 || ( ( N ^ 3 ) + ( 2 x. N ) ) ) $= ( wcel c3 cexp co c2 cmul caddc cdvds cc0 c1 cz a1i oveq2d adantr cc addcld wceq vx vy cn0 wbr cv oveq1 oveq2 oveq12d breq2d 3z dvds0 ax-mp cn 3nn 0exp 2t0e0 oveq12i 00id eqtri breq2i mpbir nn0z zsqcl syl 1zzd zmulcld sq1 nn0cn mulid1d eqtrd oveq1d peano2zd eqeltrd zaddcld dvdsmul1 sylancr adantl simpr wa 3nn0 zexpcl sylancl ad2antlr 2z dvds2addd 3cn 1cnd mulcld adddid breqtrd sqcld df-3 2cn ax-1cn addcomi 3t1e3 3eqtr4d expcl ax-mulcl syl5eqel addassd 1exp 2cnd eqcomd add32d expcld ad2antrr binom3 syl2anc 2t1e2 eqtr2d nn0indd mpdan ) ABUCDEBEFGZHBIGZJGZKUDZCAEUAUEZEFGZHXRIGZJGZKUDELEFGZHLIGZJGZKUDZEU BUEZEFGZHYFIGZJGZKUDZEYFMJGZEFGZHYKIGZJGZKUDXQUAUBBXRLTZYAYDEKYOXSYBXTYCJXR LEFUFXRLHIUGUHUIXRYFTZYAYIEKYPXSYGXTYHJXRYFEFUFXRYFHIUGUHUIXRYKTZYAYNEKYQXS YLXTYMJXRYKEFUFXRYKHIUGUHUIXRBTZYAXPEKYRXSXNXTXOJXRBEFUFXRBHIUGUHUIYEAYEELK UDZENDZYSUJEUKULYDLEKYDLLJGLYBLYCLJEUMDYBLTUNEUOULUPUQURUSUTVAOAYFUCDZVSZYJ VSZEYGEYFHFGZMIGZIGZJGZEYFMHFGZIGZIGZMEFGZJGZJGZYHHJGZJGZYNKUUCEUUMYHJGZHJG ZUUOKUUCEUUGYHJGZUULJGZHJGZUUQKUUCEUURUULHJGZJGZUUTKUUCEYIUUFJGZUUJUUKHJGZJ GZJGZUVBKUUCEYIUUFUVEJGZJGZUVFKUUCEYIUUFUUJEMIGZJGZJGZJGZUVHKUUCEYIUUFEUUIM JGZIGZJGZJGZUVLKUUCEYIEUUEUVMJGZIGZJGUVPKUUCEYIUVRYTUUCUJOUUBEUVRKUDZYJUUAU VSAUUAYTUVQNDUVSUJUUAUUEUVMUUAUUDMUUAYFNDZUUDNDZYFVBZYFVCVDZUUAVEVFUUAUVMYK NUUAUUIYFMJUUAUUIYFMIGZYFUUAUUHMYFIUUHMTZUUAVGOPUUAYFYFVHZVIVJVKUUAYFUWBVLZ VMVNEUVQVOVPVQQUUBYJVRUUBUVRNDYJUUBEUVQYTUUBUJOUUBUUEUVMUUBUUDMUUAUWAAUWCVQ UUBVEVFUUBUVMYKNUUBUUIYFMJUUBUUIUWDYFUUBUUHMYFIUWEUUBVGOPUUBYFUUAYFRDZAUWFV QZVIVJVKUUAYKNDAUWGVQVMVNVFQUUCYGYHUUAYGNDZAYJUUAUVTEUCDZUWJUWBVTYFEWAWBWCU UBYHNDYJUUBHYFHNDUUBWDOUUAUVTAUWBVQVFQVNWEUUCUVRUVOYIJUUBUVRUVOTYJUUBEUUEUV MERDUUBWFOZUUBUUDMUUBYFUWIWKUUBWGZWHZUUBUUIMUUBYFUUHUWIUUBMUWMWKWHZUWMSWIQP WJUUCUVOUVKYIJUUCUVNUVJUUFJUUBUVNUVJTYJUUBEUUIMUWLUWOUWMWIQPPWJUUCUVKUVGYIJ UUBUVKUVGTYJUUBUVJUVEUUFJUUBUVIUVDUUJJUUBEMHJGZUVIUVDEUWPTUUBEHMJGUWPWLHMWM WNWOUSOUVIETUUBWPOUUBUUKMHJUUKMTZUUBYTUWQUJEXBULZOVKWQPPQPWJUUBUVHUVFTYJUUB UVFUVHUUBYIUUFUVEUUBYGYHUUBUWHUWKYGRDUWIVTYFEWRWBZUUBHRDUWHYHRDWMUWIHYFWSVP ZSUUBEUUEUWLUWNWHZUUBUUJUVDUUBEUUIUWLUWOWHZUUBUUKHAUUKRDZUUAAUUKMRUWRAWGWTZ QZUUBXCZSSXAXDQWJUUBUVFUVBTYJUUBUVCUURUVEUVAJUUBYGYHUUFUWSUWTUXAXEUUBUVAUVE UUBUUJUUKHUXBUXEUXFXAXDUHQWJUUBUVBUUTTYJUUBUUTUVBUUBUURUULHUUBUUGYHUUBYGUUF UWSUXASZUWTSUUBUUJUUKUXBUXESZUXFXAXDQWJUUBUUTUUQTYJUUBUUSUUPHJUUBUUGYHUULUX GUWTUXHXEVKQWJUUCUUMYHHUUCUUGUULUUCYGUUFUUCYFEUUAUWHAYJUWFWCZUWKUUCVTOXFUUB UUFRDYJUXAQSUUCUUJUUKUUBUUJRDYJUXBQAUXCUUAYJUXDXGSSUUCHYFUUCXCZUXIWHUXJXAWJ UUBUUOYNTYJUUBUUMYLUUNYMJUUAUUMYLTAUUAYLUUMUUAUWHMRDYLUUMTUWFUUAWGYFMXHXIXD VQUUBYMYHHMIGZJGUUNUUBHYFMUXFUWIUWMWIUUBUXKHYHJUXKHTUUBXJOPXKUHQWJXLXM $. $}