Metamath Proof Explorer

Theorem trirecip

Description: The sum of the reciprocals of the triangle numbers converge to two. This is Metamath 100 proof #42. (Contributed by Scott Fenton, 23-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion trirecip 
|- sum_ k e. NN ( 2 / ( k x. ( k + 1 ) ) ) = 2

Proof

Step Hyp Ref Expression
1 2cnd 
 |-  ( k e. NN -> 2 e. CC )
2 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
3 nnmulcl 
 |-  ( ( k e. NN /\ ( k + 1 ) e. NN ) -> ( k x. ( k + 1 ) ) e. NN )
4 2 3 mpdan 
 |-  ( k e. NN -> ( k x. ( k + 1 ) ) e. NN )
5 4 nncnd 
 |-  ( k e. NN -> ( k x. ( k + 1 ) ) e. CC )
6 4 nnne0d 
 |-  ( k e. NN -> ( k x. ( k + 1 ) ) =/= 0 )
7 1 5 6 divrecd 
 |-  ( k e. NN -> ( 2 / ( k x. ( k + 1 ) ) ) = ( 2 x. ( 1 / ( k x. ( k + 1 ) ) ) ) )
8 7 sumeq2i 
 |-  sum_ k e. NN ( 2 / ( k x. ( k + 1 ) ) ) = sum_ k e. NN ( 2 x. ( 1 / ( k x. ( k + 1 ) ) ) )
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 1zzd 
 |-  ( T. -> 1 e. ZZ )
11 id 
 |-  ( n = k -> n = k )
12 oveq1 
 |-  ( n = k -> ( n + 1 ) = ( k + 1 ) )
13 11 12 oveq12d 
 |-  ( n = k -> ( n x. ( n + 1 ) ) = ( k x. ( k + 1 ) ) )
14 13 oveq2d 
 |-  ( n = k -> ( 1 / ( n x. ( n + 1 ) ) ) = ( 1 / ( k x. ( k + 1 ) ) ) )
15 eqid 
 |-  ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
16 ovex 
 |-  ( 1 / ( k x. ( k + 1 ) ) ) e. _V
17 14 15 16 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ` k ) = ( 1 / ( k x. ( k + 1 ) ) ) )
18 17 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ` k ) = ( 1 / ( k x. ( k + 1 ) ) ) )
19 4 nnrecred 
 |-  ( k e. NN -> ( 1 / ( k x. ( k + 1 ) ) ) e. RR )
20 19 recnd 
 |-  ( k e. NN -> ( 1 / ( k x. ( k + 1 ) ) ) e. CC )
21 20 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( k x. ( k + 1 ) ) ) e. CC )
22 15 trireciplem 
 |-  seq 1 ( + , ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ) ~~> 1
23 22 a1i 
 |-  ( T. -> seq 1 ( + , ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ) ~~> 1 )
24 climrel 
 |-  Rel ~~>
25 24 releldmi 
 |-  ( seq 1 ( + , ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ) ~~> 1 -> seq 1 ( + , ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ) e. dom ~~> )
26 23 25 syl 
 |-  ( T. -> seq 1 ( + , ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) ) e. dom ~~> )
27 2cnd 
 |-  ( T. -> 2 e. CC )
28 9 10 18 21 26 27 isummulc2 
 |-  ( T. -> ( 2 x. sum_ k e. NN ( 1 / ( k x. ( k + 1 ) ) ) ) = sum_ k e. NN ( 2 x. ( 1 / ( k x. ( k + 1 ) ) ) ) )
29 9 10 18 21 23 isumclim 
 |-  ( T. -> sum_ k e. NN ( 1 / ( k x. ( k + 1 ) ) ) = 1 )
30 29 oveq2d 
 |-  ( T. -> ( 2 x. sum_ k e. NN ( 1 / ( k x. ( k + 1 ) ) ) ) = ( 2 x. 1 ) )
31 28 30 eqtr3d 
 |-  ( T. -> sum_ k e. NN ( 2 x. ( 1 / ( k x. ( k + 1 ) ) ) ) = ( 2 x. 1 ) )
32 31 mptru 
 |-  sum_ k e. NN ( 2 x. ( 1 / ( k x. ( k + 1 ) ) ) ) = ( 2 x. 1 )
33 2t1e2 
 |-  ( 2 x. 1 ) = 2
34 8 32 33 3eqtri 
 |-  sum_ k e. NN ( 2 / ( k x. ( k + 1 ) ) ) = 2