metamath/valid/induction-seq-mul2pnp1.mm

${
  $d N x $.
  $d U n y $.
  $d U x y $.
  $d ph x y $.
  induction-seq-mul2pnp1.0 $e |- ( ph -> N e. NN0 ) $.
  induction-seq-mul2pnp1.1 $e |- ( ph -> ( U ` 0 ) = 0 ) $.
  induction-seq-mul2pnp1.2 $e |- ( ph -> A. n e. NN0 ( U ` ( n + 1 ) ) = ( ( 2 
x. ( U ` n ) ) + ( n + 1 ) ) ) $.
  $( (Contributed by Stanislas Polu, 13-Oct-2020.) $)
  induction-seq-mul2pnp1 $p |- ( ph -> ( U ` N ) = ( ( 2 ^ ( N + 1 ) ) - ( N + 
2 ) ) ) $=
( wcel c2 c1 caddc co cexp cmin wceq cc0 oveq1 oveq2d cmul eqtrd vx cn0 cfv vy 
cv fveq2 oveq12d eqeq12d 0p1e1 oveq2i 2cn addid2i oveq12i cc exp1 oveq1d mp1i 
subidi syl6eq syl5eq eqtr4d wa wral fveq2d rspccva sylan adantr adantl oveq2 
2cnd peano2nn0 expcld nn0cn addcld subdid expp1d mulcomd wne 2ne0 a1i eqcomd 
nn0zd peano2zd ad2antlr expclzd mulcld nn0cnd subadd23d cneg negsubd negcld 
addcomd subnegd negsubdi3d 1nn0 nn0addcld subcld adddid 1cnd addsubd cz 
subsub4d 2timesd pncand c4 2p2e4 oveq1i c3 4cn ax-1cn 3cn 3p1e4 addcomli 
subaddrii addsubassd addassd 2p1e3 3eqtr4d add32d nn0indd mpdan ) ADUBHDBUC 
ZIDJKLZMLZDIKLZNLZOZEAUAUEZBUCZIYHJKLZMLZYHIKLZNLZOPBUCZIPJKLZMLZPIKLZNLZOU 
DUEZBUCZIYSJKLZMLZYSIKLZNLZOZUUABUCZIUUAJKLZMLZUUAIKLZNLZOYGUAUDDYHPOZYIYNY 
MYRYHPBUFUUKYKYPYLYQNUUKYJYOIMYHPJKQRYHPIKQUGUHYHYSOZYIYTYMUUDYHYSBUFUULYKU 
UBYLUUCNUULYJUUAIMYHYSJKQRYHYSIKQUGUHYHUUAOZYIUUFYMUUJYHUUABUFUUMYKUUHYLUUI 
NUUMYJUUGIMYHUUAJKQRYHUUAIKQUGUHYHDOZYIYBYMYFYHDBUFUUNYKYDYLYENUUNYJYCIMYHD 
JKQRYHDIKQUGUHAYNPYRFAYRIJMLZINLZPYPUUOYQINYOJIMUIUJIUKULUMAUUPIINLPAUUOIIN 
IUNHUUOIOAUKIUOUQUPIUKURUSUTVAAYSUBHZVBZUUEVBZUUFIYTSLZUUAKLZUUJUURUUFUVAOZ 
UUEACUEZJKLZBUCZIUVCBUCZSLZUVDKLZOZCUBVCUUQUVBGUVIUVBCYSUBUVCYSOZUVEUUFUVHU 
VAUVJUVDUUABUVCYSJKQZVDUVJUVGUUTUVDUUAKUVJUVFYTISUVCYSBUFRUVKUGUHVEVFVGUUSU 
VAIUUDSLZUUAKLZUUJUUSUUTUVLUUAKUUEUUTUVLOUURYTUUDISVIVHUPUUSUVMIUUBSLZIUUCS 
LZNLZUUAKLZUUJUUSUVLUVPUUAKUUSIUUBUUCUUSVJZUURUUBUNHUUEUURIUUAUURVJZUUQUUAU 
BHAYSVKZVHZVLVGUURUUCUNHUUEUURYSIUUQYSUNHAYSVMZVHZUVSVNZVGZVOUPUUSUVQUUHUVO 
NLZUUAKLZUUJUUSUVPUWFUUAKUURUVPUWFOUUEUURUVNUUHUVONUURUUHUVNUUQUUHUVNOAUUQU 
UHUUBISLUVNUUQIUUAUUQVJZUVTVPUUQIUUBUWHUUQIUUAUWHUVTVLVQVAVHWAUPVGUPUUSUWGU 
UHUUAUVONLZKLZUUJUUSUUHUVOUUAUUSIUUGUVRIPVRUUSVSVTUUQUUGXAHAUUEUUQUUAUUQUUA 
UVTWBWCWDWEUUSIUUCUVRUWEWFUURUUAUNHUUEUURUUAUWAWGZVGWHUURUWJUUJOUUEUURUWJUU 
HUVOUUANLZNLZUUJUURUWJUUHUWLWIZKLUWMUURUWIUWNUUHKUUQUWIUWNOAUUQUWIUUAUVOWIZ 
KLZUWNUUQUWPUWIUUQUUAUVOUUQUUAUVTWGZUUQIUUCUWHUUQYSIUWBUWHVNWFZWJWAUUQUWPUW 
OUUAWINLZUWNUUQUWPUWOUUAKLZUWSUUQUUAUWOUWQUUQUVOUWRWKZWLUUQUWSUWTUUQUWOUUAU 
XAUWQWMWATUUQUWNUWSUUQUVOUUAUWRUWQWNWATTVHRUURUUHUWLUURIUUGUVSUURUUAJUWAJUB 
HUURWOVTWPVLUURUVOUUAUURIUUCUVSUWDWFUWKWQWJTUURUWLUUIUUHNUURUWLUUCJKLZUUIUU 
RUWLIYSSLZIISLZKLZUUANLZUXBUURUVOUXEUUANUURIYSIUVSUWCUVSWRUPUURUXFUXEYSNLZJ 
NLZUXBUURUXHUXFUURUXEYSJUURUXCUXDUURIYSUVSUWCWFUURIIUVSUVSWFVNUWCUURWSZXBWA 
UUQUXHUXBOAUUQUXHUXCYSNLZUXDKLZJNLZUXBUUQUXGUXKJNUUQUXCUXDYSUUQIYSUWHUWBWFU 
UQIIUWHUWHWFUWBWTUPUUQUXLYSIIKLZKLZJNLZUXBUUQUXKUXNJNUUQUXJYSUXDUXMKUUQUXJY 
SYSKLZYSNLYSUUQUXCUXPYSNUUQYSUWBXCUPUUQYSYSUWBUWBXDTUUQIUWHXCUGUPUUQUXOYSXE 
KLZJNLZUXBUXNUXQJNUXMXEYSKXFUJXGUUQYSXEJNLZKLYSXHKLZUXRUXBUUQUXSXHYSKUXSXHO 
UUQXEJXHXIXJXKXHJXEXKXJXLXMXNVTRUUQYSXEJUWBXEUNHUUQXIVTUUQWSZXOUUQUXBYSIJKL 
ZKLUXTUUQYSIJUWBUWHUYAXPUUQUYBXHYSKUYBXHOUUQXQVTRTXRUTTTVHTTUURYSIJUWCUVSUX 
IXSTRTVGTTTTTXTYA $. 
$}