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

${ $d N x $. $d ph x y $. induction-divisibility-3div2tooddnp1.0 $e |- ( ph -> N e. NN0 ) $. $( (Contributed by Stanislas Polu, 9-Oct-2020.) $) induction-divisibility-3div2tooddnp1 $p |- ( ph -> 3 || ( ( 2 ^ ( ( 2 x. N ) + 1 ) ) + 1 ) ) $= ( wcel c3 c2 cmul co c1 caddc cexp cdvds wbr wceq oveq1d oveq2d a1i c4 cmin breqtrd vx vy cn0 id cv cc0 oveq2 breq2d cz iddvds ax-mp 2t0e0 oveq1i 0p1e1 3z eqtri oveq2i 2nn0 numexp1 2p1e3 breqtrrd nn0mulcld 1nn0 nn0addcld adantl wa 2z zexpcl sylancr adantr peano2zd simpr dvdsmultr1d zcnd mulcomd zmulcld 4z cc 4cn dvds2subd 2cnd expcld adddid mulid1d mulcld 3cn addsubassd eqcomi 1cnd sq2 ax-1cn 3p1e4 subaddrii oveq12d nn0cnd addcomd expaddd eqtrd eqcomd nn0cn 2t1e2 add32d eqtr2d nn0indd syl2anc ) AABUCDEFFBGHZIJHZKHZIJHZLMZAUDC AEFFUAUEZGHZIJHZKHZIJHZLMEFFUFGHZIJHZKHZIJHZLMEFFUBUEZGHZIJHZKHZIJHZLMZEFFX TIJHZGHZIJHZKHZIJHZLMXJUAUBBXKUFNZXOXSELYKXNXRIJYKXMXQFKYKXLXPIJXKUFFGUGOPO UHXKXTNZXOYDELYLXNYCIJYLXMYBFKYLXLYAIJXKXTFGUGOPOUHXKYFNZXOYJELYMXNYIIJYMXM YHFKYMXLYGIJXKYFFGUGOPOUHXKBNZXOXIELYNXNXHIJYNXMXGFKYNXLXFIJXKBFGUGOPOUHAEE XSLEELMZAEUIDZYOUOEUJUKZQXSENAXSFIJHEXRFIJXRFIKHFXQIFKXQUFIJHIXPUFIJULUMUNU PUQFURUSUPUMUTUPQVAAXTUCDZVFZYEVFZEFYBFJHZKHZIJHZYJLYTEFFKHZYCGHZIJHZUUCLYT ERYCGHZRESHZJHZUUFLYTEUUGRJHZESHZUUILYTEUUGRIGHZJHZESHZUUKLYTERYDGHZESHUUNL YTEUUOEYPYTUOQZYTEYDRGHUUOLYTEYDRUUPYTYCYSYCUIDZYEYSFUIDYBUCDZUUQVGYRUURAYR YAIYRFXTFUCDZYRURQYRUDVBIUCDYRVCQVDVEZFYBVHVIVJVKZRUIDYTVQQZYSYEVLVMYTYDRYT YDUVAVNRVRDZYTVSQZVOTYOYTYQQYTRYDUVBUVAVPUUPVTYTUUOUUMESYTRYCIUVDYSYCVRDYEY SFYBYSWAZUUTWBZVJYTWIWCOTYSUUNUUKNYEYSUUMUUJESYSUULRUUGJYSRUVCYSVSQZWDPOVJT YTUUGREYSUUGVRDYEYSRYCUVGUVFWEVJUVDEVRDYTWFQWGTYTUUGUUEUUHIJYTRUUDYCGRUUDNY TUUDRWJWHQOUUHINYTREIVSWFWKWLWMQWNTYSUUFUUCNYEYSUUEUUBIJYSUUBUUEYSUUBFFYBJH ZKHUUEYSUUAUVHFKYSYBFYSYBUUTWOUVEWPPYSFFYBUVEUUTUUSYSURQWQWRWSOVJTYTUUBYIIJ YSUUBYINYEYSUUAYHFKYRUUAYHNAYRYHYAFJHZIJHUUAYRYGUVIIJYRYGYAFIGHZJHUVIYRFXTI YRWAZXTWTZYRWIZWCYRUVJFYAJUVJFNYRXAQPWROYRYAFIYRFXTUVKUVLWEUVKUVMXBXCVEPVJO TXDXE $. $}