Metamath Proof Explorer

Theorem trireciplem

Description: Lemma for trirecip . Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Hypothesis trireciplem.1 
|- F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
Assertion trireciplem 
|- seq 1 ( + , F ) ~~> 1

Proof

Step Hyp Ref Expression
1 trireciplem.1 
 |-  F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( T. -> 1 e. ZZ )
4 1cnd 
 |-  ( T. -> 1 e. CC )
5 nnex 
 |-  NN e. _V
6 5 mptex 
 |-  ( n e. NN |-> ( 1 / ( n + 1 ) ) ) e. _V
7 6 a1i 
 |-  ( T. -> ( n e. NN |-> ( 1 / ( n + 1 ) ) ) e. _V )
8 oveq1 
 |-  ( n = k -> ( n + 1 ) = ( k + 1 ) )
9 8 oveq2d 
 |-  ( n = k -> ( 1 / ( n + 1 ) ) = ( 1 / ( k + 1 ) ) )
10 eqid 
 |-  ( n e. NN |-> ( 1 / ( n + 1 ) ) ) = ( n e. NN |-> ( 1 / ( n + 1 ) ) )
11 ovex 
 |-  ( 1 / ( k + 1 ) ) e. _V
12 9 10 11 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ` k ) = ( 1 / ( k + 1 ) ) )
13 12 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ` k ) = ( 1 / ( k + 1 ) ) )
14 2 3 4 3 7 13 divcnvshft 
 |-  ( T. -> ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ~~> 0 )
15 seqex 
 |-  seq 1 ( + , F ) e. _V
16 15 a1i 
 |-  ( T. -> seq 1 ( + , F ) e. _V )
17 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
18 17 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( k + 1 ) e. NN )
19 18 nnrecred 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. RR )
20 19 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( k + 1 ) ) e. CC )
21 13 20 eqeltrd 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ` k ) e. CC )
22 13 oveq2d 
 |-  ( ( T. /\ k e. NN ) -> ( 1 - ( ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ` k ) ) = ( 1 - ( 1 / ( k + 1 ) ) ) )
23 elfznn 
 |-  ( j e. ( 1 ... k ) -> j e. NN )
24 23 adantl 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j e. NN )
25 24 nncnd 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j e. CC )
26 peano2cn 
 |-  ( j e. CC -> ( j + 1 ) e. CC )
27 25 26 syl 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j + 1 ) e. CC )
28 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
29 24 28 syl 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j + 1 ) e. NN )
30 24 29 nnmulcld 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j x. ( j + 1 ) ) e. NN )
31 30 nncnd 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j x. ( j + 1 ) ) e. CC )
32 30 nnne0d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j x. ( j + 1 ) ) =/= 0 )
33 27 25 31 32 divsubdird 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( ( j + 1 ) - j ) / ( j x. ( j + 1 ) ) ) = ( ( ( j + 1 ) / ( j x. ( j + 1 ) ) ) - ( j / ( j x. ( j + 1 ) ) ) ) )
34 ax-1cn 
 |-  1 e. CC
35 pncan2 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j + 1 ) - j ) = 1 )
36 25 34 35 sylancl 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j + 1 ) - j ) = 1 )
37 36 oveq1d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( ( j + 1 ) - j ) / ( j x. ( j + 1 ) ) ) = ( 1 / ( j x. ( j + 1 ) ) ) )
38 27 mulid1d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j + 1 ) x. 1 ) = ( j + 1 ) )
39 27 25 mulcomd 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j + 1 ) x. j ) = ( j x. ( j + 1 ) ) )
40 38 39 oveq12d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( ( j + 1 ) x. 1 ) / ( ( j + 1 ) x. j ) ) = ( ( j + 1 ) / ( j x. ( j + 1 ) ) ) )
41 1cnd 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> 1 e. CC )
42 24 nnne0d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> j =/= 0 )
43 29 nnne0d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j + 1 ) =/= 0 )
44 41 25 27 42 43 divcan5d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( ( j + 1 ) x. 1 ) / ( ( j + 1 ) x. j ) ) = ( 1 / j ) )
45 40 44 eqtr3d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j + 1 ) / ( j x. ( j + 1 ) ) ) = ( 1 / j ) )
46 25 mulid1d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j x. 1 ) = j )
47 46 oveq1d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j x. 1 ) / ( j x. ( j + 1 ) ) ) = ( j / ( j x. ( j + 1 ) ) ) )
48 41 27 25 43 42 divcan5d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( j x. 1 ) / ( j x. ( j + 1 ) ) ) = ( 1 / ( j + 1 ) ) )
49 47 48 eqtr3d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( j / ( j x. ( j + 1 ) ) ) = ( 1 / ( j + 1 ) ) )
50 45 49 oveq12d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( ( ( j + 1 ) / ( j x. ( j + 1 ) ) ) - ( j / ( j x. ( j + 1 ) ) ) ) = ( ( 1 / j ) - ( 1 / ( j + 1 ) ) ) )
51 33 37 50 3eqtr3d 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) = ( ( 1 / j ) - ( 1 / ( j + 1 ) ) ) )
52 51 sumeq2dv 
 |-  ( ( T. /\ k e. NN ) -> sum_ j e. ( 1 ... k ) ( 1 / ( j x. ( j + 1 ) ) ) = sum_ j e. ( 1 ... k ) ( ( 1 / j ) - ( 1 / ( j + 1 ) ) ) )
53 oveq2 
 |-  ( n = j -> ( 1 / n ) = ( 1 / j ) )
54 oveq2 
 |-  ( n = ( j + 1 ) -> ( 1 / n ) = ( 1 / ( j + 1 ) ) )
55 oveq2 
 |-  ( n = 1 -> ( 1 / n ) = ( 1 / 1 ) )
56 1div1e1 
 |-  ( 1 / 1 ) = 1
57 55 56 eqtrdi 
 |-  ( n = 1 -> ( 1 / n ) = 1 )
58 oveq2 
 |-  ( n = ( k + 1 ) -> ( 1 / n ) = ( 1 / ( k + 1 ) ) )
59 nnz 
 |-  ( k e. NN -> k e. ZZ )
60 59 adantl 
 |-  ( ( T. /\ k e. NN ) -> k e. ZZ )
61 18 2 eleqtrdi 
 |-  ( ( T. /\ k e. NN ) -> ( k + 1 ) e. ( ZZ>= ` 1 ) )
62 elfznn 
 |-  ( n e. ( 1 ... ( k + 1 ) ) -> n e. NN )
63 62 adantl 
 |-  ( ( ( T. /\ k e. NN ) /\ n e. ( 1 ... ( k + 1 ) ) ) -> n e. NN )
64 63 nnrecred 
 |-  ( ( ( T. /\ k e. NN ) /\ n e. ( 1 ... ( k + 1 ) ) ) -> ( 1 / n ) e. RR )
65 64 recnd 
 |-  ( ( ( T. /\ k e. NN ) /\ n e. ( 1 ... ( k + 1 ) ) ) -> ( 1 / n ) e. CC )
66 53 54 57 58 60 61 65 telfsum 
 |-  ( ( T. /\ k e. NN ) -> sum_ j e. ( 1 ... k ) ( ( 1 / j ) - ( 1 / ( j + 1 ) ) ) = ( 1 - ( 1 / ( k + 1 ) ) ) )
67 52 66 eqtrd 
 |-  ( ( T. /\ k e. NN ) -> sum_ j e. ( 1 ... k ) ( 1 / ( j x. ( j + 1 ) ) ) = ( 1 - ( 1 / ( k + 1 ) ) ) )
68 id 
 |-  ( n = j -> n = j )
69 oveq1 
 |-  ( n = j -> ( n + 1 ) = ( j + 1 ) )
70 68 69 oveq12d 
 |-  ( n = j -> ( n x. ( n + 1 ) ) = ( j x. ( j + 1 ) ) )
71 70 oveq2d 
 |-  ( n = j -> ( 1 / ( n x. ( n + 1 ) ) ) = ( 1 / ( j x. ( j + 1 ) ) ) )
72 ovex 
 |-  ( 1 / ( j x. ( j + 1 ) ) ) e. _V
73 71 1 72 fvmpt 
 |-  ( j e. NN -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
74 24 73 syl 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
75 simpr 
 |-  ( ( T. /\ k e. NN ) -> k e. NN )
76 75 2 eleqtrdi 
 |-  ( ( T. /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
77 30 nnrecred 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
78 77 recnd 
 |-  ( ( ( T. /\ k e. NN ) /\ j e. ( 1 ... k ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
79 74 76 78 fsumser 
 |-  ( ( T. /\ k e. NN ) -> sum_ j e. ( 1 ... k ) ( 1 / ( j x. ( j + 1 ) ) ) = ( seq 1 ( + , F ) ` k ) )
80 22 67 79 3eqtr2rd 
 |-  ( ( T. /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) = ( 1 - ( ( n e. NN |-> ( 1 / ( n + 1 ) ) ) ` k ) ) )
81 2 3 14 4 16 21 80 climsubc2 
 |-  ( T. -> seq 1 ( + , F ) ~~> ( 1 - 0 ) )
82 81 mptru 
 |-  seq 1 ( + , F ) ~~> ( 1 - 0 )
83 1m0e1 
 |-  ( 1 - 0 ) = 1
84 82 83 breqtri 
 |-  seq 1 ( + , F ) ~~> 1