metamath/valid/induction-sum-1oktkp1.mm

${
  $d N k x $.
  $d k y x $.
  $d ph x y $.
  induction-sum-1oktkp1.0 $e |- ( ph -> N e. NN ) $.
  $( (Contributed by Stanislas Polu, 14-Oct-2020.) $)
  induction-sum-1oktkp1 $p |- ( ph -> sum_ k e. ( 1 ... N ) ( 1 / ( k x. ( k + 
1 ) ) ) = ( N / ( N + 1 ) ) ) $=
( wcel c1 cfz co caddc cmul cdiv csu id oveq1 cc oveq2d eqtrd adantl oveq1d 
wceq vx vy cn cv oveq2 sumeq1d oveq12d eqeq12d csn cz fzsn ax-mp a1i ax-1cn 1z 
1red cc0 cle wbr 0le1 ge0p1rpd rprecred recnd df-2 syl6eqr mulid2i eqtri c2 2cn 
syl6eq sumsn sylancr wa cuz cfv nnuz syl6eleq elfznn nncnd peano2nnd mulcld 
nnmulcld nnne0d reccld fsump1 ad2antlr nncn addcld peano2nn divcan2d 1cnd 
divcld eqcomd divdiv1d mulcomd mulne0d divassd adddird mulid2d mulid1d addassd 
adddid simpr divdird divcan5rd adantr eqtr4d nnindd mpdan ) ACUCEFC 
GHZFBUDZXKFIHZJHZKHZBLZCCFIHZKHZTZDAFUAUDZGHZXNBLZXSXSFIHZKHZTFFGHZXNBLZFFF 
IHZKHZTFUBUDZGHZXNBLZYHYHFIHZKHZTZFYKGHZXNBLZYKYKFIHZKHZTXRUAUBCXSFTZYAYEYC 
YGYRXTYDXNBXSFFGUEUFYRXSFYBYFKYRMXSFFINUGUHXSYHTZYAYJYCYLYSXTYIXNBXSYHFGUEU 
FYSXSYHYBYKKYSMXSYHFINUGUHXSYKTZYAYOYCYQYTXTYNXNBXSYKFGUEUFYTXSYKYBYPKYTMXS 
YKFINUGUHXSCTZYAXOYCXQUUAXTXJXNBXSCFGUEUFUUAXSCYBXPKUUAMXSCFINUGUHAYEFUIZXN 
BLZYGAYDUUBXNBYDUUBTZAFUJEUUDUOFUKULUMUFAFOEYGOEUUCYGTUNAYGAYFAFAUPUQFURUSA 
UTUMVAVBVCXNYGBFOXKFTZXMYFFKUUEXMFXLJHZYFXKFXLJNUUEUUFFVHJHZYFUUEXLVHFJUUEX 
LYFVHXKFFINVDVEPUUGVHYFVHVIVFVDVGVJQPVKVLQAYHUCEZVMZYMVMZYOYJFYKYPJHZKHZIHZ 
YQUUHYOUUMTAYMUUHXNUULBFYHUUHYHUCFVNVOUUHMVPVQUUHXKYNEZVMZXMUUOXKXLUUNXKOEU 
UHUUNXKXKYKVRZVSRUUOXLUUOXKUUNXKUCEUUHUUPRZVTZVSWAUUOXMUUOXKXLUUQUURWBWCWDX 
KYKTZXMUUKFKUUSXKYKXLYPJUUSMXKYKFINUGPWEWFUUJYQYLUULIHZUUMUUIYQUUTTYMUUIYQY 
HYPJHZUUKKHZUULIHZUUTUUIYQUVAFIHZUUKKHZUVCUUHYQUVETAUUHYQYHYKJHZYHFJHZIHZFI 
HZUUKKHZUVEUUHYQUVFYKIHZUUKKHZUVJUUHYQYKYKJHZUUKKHZUVLUUHYQYKYKUUKKHZJHZUVN 
UUHYQYKYKYPYKJHZKHZJHZUVPUUHYQYKYQYKKHZJHZUVSUUHUWAYQUUHYQYKUUHYKYPUUHYHFYH 
WGZUUHWKZWHZUUHYKFUWDUWCWHZUUHYPUUHYKYHWIZVTWCZWLUWDUUHYKUWFWCZWJWMUUHUVTUV 
RYKJUUHYKYPYKUWDUWEUWDUWGUWHWNPQUUHUVRUVOYKJUUHUVQUUKYKKUUHYPYKUWEUWDWOPPQU 
UHUVNUVPUUHYKYKUUKUWDUWDUUHYKYPUWDUWEWAUUHYKYPUWDUWEUWHUWGWPWQWMQUUHUVMUVKU 
UKKUUHUVMUVFFYKJHZIHUVKUUHYHFYKUWBUWCUWDWRUUHUWIYKUVFIUUHYKUWDWSPQSQUUHUVKU 
VIUUKKUUHUVKUVFUVGFIHZIHZUVIUUHYKUWJUVFIUUHYHUVGFIUUHUVGYHUUHYHUWBWTWMSPUUH 
UVIUWKUUHUVFUVGFUUHYHYKUWBUWDWAUUHYHFUWBUWCWAUWCXAWMQSQUUHUVIUVDUUKKUUHUVHU 
VAFIUUHUVAUVHUUHYHYKFUWBUWDUWCXBWMSSQRUUIUVAFUUKUUIYHYPUUHYHOEAUWBRZUUHYPOE 
AUWERZWAUUIWKUUIYKYPUUHYKOEAUWDRZUWMWAUUIUUKUUIYKYPUUIYHAUUHXCVTZUUIYKUWOVT 
ZWBWCXDQUUIUVBYLUULIUUIYHYKYPUWLUWNUWMUUIYKUWOWCUUIYPUWPWCXESQXFUUJYJYLUULI 
UUIYMXCSXGXGXHXI $. 
$}