metamath/valid/induction-sum2kp1npqsqm1.mm

${
  $d N k x $.
  $d k ph x y $.
  induction-sum2kp1npqsqm1.0 $e |- ( ph -> N e. NN ) $.
  $( (Contributed by Stanislas Polu, 22-Sep-2020.) $)
  induction-sum2kp1npqsqm1 $p |- ( ph -> sum_ k e. ( 1 ... N ) ( ( 2 x. k ) + 1 
) = ( ( ( N + 1 ) ^ 2 ) - 1 ) ) $=
( cn wcel c1 cfz co c2 cmul caddc csu cexp cmin wceq oveq2 oveq1d c3 eqtrd vx 
vy cv sumeq1d oveq1 eqeq12d cz cc 1z ax-1cn mulcli addcli fsum1 mp2an c4 2cn 
a1i 4cn 3cn addcomi df-4 eqtr4i subaddrii eqcomi 2t1e2 df-3 sq2 3eqtr4a oveq1i 
1p1e2 syl6eqr cuz cfv simpr nnuz syl6eleq elfznn adantl nnmulcl mpan 2nn syl 
peano2nnd nncnd fsump1 adantr eqidd oveq12d peano2nn sqcld nnmulcld wa nnrpd 
rpcnd subadd23d pncand oveq2d oveq2i addcld addsubd syl5eqr npcand 1cnd sq1 
eqtr2d binom2 sylancl mulid1d eqcomd nnindd mpdan ) ACEFGCHIZJBUCZ 
KIZGLIZBMZCGLIZJNIZGOIZPZDAGUAUCZHIZXOBMZYAGLIZJNIZGOIZPGGHIZXOBMZGGLIZJNIZ 
GOIZPGUBUCZHIZXOBMZYLGLIZJNIZGOIZPZGYOHIZXOBMZYOGLIZJNIZGOIZPXTUAUBCYAGPZYC 
YHYFYKUUDYBYGXOBYAGGHQUDUUDYEYJGOUUDYDYIJNYAGGLUERRUFYAYLPZYCYNYFYQUUEYBYMX 
OBYAYLGHQUDUUEYEYPGOUUEYDYOJNYAYLGLUERRUFYAYOPZYCYTYFUUCUUFYBYSXOBYAYOGHQUD 
UUFYEUUBGOUUFYDUUAJNYAYOGLUERRUFYACPZYCXPYFXSUUGYBXLXOBYACGHQUDUUGYEXRGOUUG 
YDXQJNYACGLUERRUFAYHJJNIZGOIZYKAYHJGKIZGLIZUUIYHUUKPZAGUGFUUKUHFUULUIUUJGJG 
UPUJUKUJULXOUUKBGXMGPXNUUJGLXMGJKQRUMUNUQASUOGOIZUUKUUIUUMSUOGSURUJUSGSLISG 
LIUOGSUJUSUTVAVBVCVDUUKSPAUUKJGLISUUJJGLVEVIVFVBUQUUIUUMPAUUHUOGOVGVIUQVHTY 
JUUHGOYIJJNVJVIVIVKAYLEFZWLZYRWLZYTYNJYOKIZGLIZLIZUUCUUOYTUUSPYRUUOXOUURBGY 
LUUOYLEGVLVMAUUNVNVOVPUUOXMYSFZWLZXOUVAXNUVAXMEFZXNEFZUUTUVBUUOXMYOVQVRJEFZ 
UVBUVCWAJXMVSVTWBWCWDXMYOPXNUUQGLXMYOJKQRWEWFUUPUUSYQUURLIZUUCUUPYNYQUURUUR 
LUUOYRVNUUPUURWGWHUUOUVEUUCPZYRUUNUVFAUUNUVEYPUUQLIZUUCUUNUVEYPUURGOIZLIUVG 
UUNYPGUURUUNYOUUNYOYLWIZWDZWJZUUNXCZUUNUURUUNUURUUNUUQUUNJYOUVDUUNWAUQUVIWK 
ZWCWMWNWOUUNUVHUUQYPLUUNUUQGUUNUUQUVMWDZUVLWPWQTUUNUVGUVGGJNIZLIZGOIZUUCUUN 
UVQUVGGOIGLIZUVGUUNUVQUVGGLIZGOIUVRUVSUVPGOGUVOUVGLUVOGXDVDWRVIUUNUVGGGUUNY 
PUUQUVKUVNWSZUVLUVLWTXAUUNUVGGUVTUVLXBXEUUNUVPUUBGOUUNUUBUVPUUNUUBYPJYOGKIZ 
KIZLIZUVOLIZUVPUUNYOUHFGUHFUUBUWDPUVJUJYOGXFXGUUNUWCUVGUVOLUUNUWBUUQYPLUUNU 
WAYOJKUUNYOUVJXHWQWQRTXIRTTVRWFTTXJXK $. 
$}