metamath/valid/induction-sum-odd.mm

${
  $d N k x $.
  $d k y x $.
  $d ph x y $.
  induction-sum-odd.0 $e |- ( ph -> N e. NN ) $.
  $( (Contributed by Stanislas Polu, 14-Oct-2020.) $)
  induction-sum-odd $p |- ( ph -> sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) = ( 
N ^ 2 ) ) $=
( cn wcel c1 cfz co c2 cmul cmin csu cexp caddc oveq2 sumeq1d oveq1 eqeq12d 
wceq vx vy cv csn cz 1z ax-mp a1i cc ax-1cn oveq1d 2t1e2 oveq1i 2m1e1 eqtri 
fzsn syl6eq sumsn mp2an sq1 syl6eqr wa cuz cfv id syl6eleq cr elfznn adantl 
nnuz nnred remulcld 1red resubcld recnd fsump1 ad2antlr nncn sqcld peano2nn 2re 
2nn nnmulcld nncnd 1cnd addsubassd binom21 mulcld addassd eqcomd eqtr4d syl 
2cnd adddid oveq2i oveq2d 3eqtrd eqtr3d sylan9eqr eqtrd nnindd mpdan ) 
ACEFGCHIZJBUCZKIZGLIZBMZCJNIZTZDAGUAUCZHIZXFBMZXJJNIZTGGHIZXFBMZGJNIZTGUBUC 
ZHIZXFBMZXQJNIZTZGXQGOIZHIZXFBMZYBJNIZTXIUAUBCXJGTZXLXOXMXPYFXKXNXFBXJGGHPQ 
XJGJNRSXJXQTZXLXSXMXTYGXKXRXFBXJXQGHPQXJXQJNRSXJYBTZXLYDXMYEYHXKYCXFBXJYBGH 
PQXJYBJNRSXJCTZXLXGXMXHYIXKXCXFBXJCGHPQXJCJNRSAXOGXPAXOGUDZXFBMZGAXNYJXFBXN 
YJTZAGUEFYLUFGUPUGUHQGUIFZYMYKGTUJUJXFGBGUIXDGTZXFJGKIZGLIZGYNXEYOGLXDGJKPU 
KYPJGLIZGYOJGLULUMUNUOUQURUSUQUTVAAXQEFZVBZYAVBYDXSJYBKIZGLIZOIZYEYRYDUUBTA 
YAYRXFUUABGXQYRXQEGVCVDYRVEVJVFYRXDYCFZVBZXFUUDXEGUUDJXDJVGFUUDWAUHUUDXDUUC 
XDEFYRXDYBVHVIVKVLUUDVMVNVOXDYBTXEYTGLXDYBJKPUKVPVQYAYSUUBXTUUAOIZYEXSXTUUA 
ORYRUUEYETAYRXTYTOIGLIZUUEYEYRXTYTGYRXQXQVRZVSZYRYTYRJYBJEFYRWBUHXQVTWCWDYR 
WEZWFZYRUUFUUEYEUUJYRYEXTJXQKIZGOIZOIZUUEYRYEXTUUKOIGOIZUUMYRXQUIFYEUUNTUUG 
XQWGWLYRUUNUUMYRXTUUKGUUHYRJXQYRWMZUUGWHZUUIWIWJWKYRUUAUULXTOYRUUAUUKJOIZGL 
IUUKYQOIUULYRYTUUQGLYRYTUUKYOOIUUQYRJXQGUUOUUGUUIWNYOJUUKOULWOUQUKYRUUKJGUU 
PUUOUUIWFYRYQGUUKOYQGTYRUNUHWPWQWPWKWKWRVIWSWTXAXB $.
$}