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 1 n n + 1
Assertion trireciplem seq 1 + F 1

Proof

Step Hyp Ref Expression
1 trireciplem.1 F = n 1 n n + 1
2 nnuz = 1
3 1zzd 1
4 1cnd 1
5 nnex V
6 5 mptex n 1 n + 1 V
7 6 a1i n 1 n + 1 V
8 oveq1 n = k n + 1 = k + 1
9 8 oveq2d n = k 1 n + 1 = 1 k + 1
10 eqid n 1 n + 1 = n 1 n + 1
11 ovex 1 k + 1 V
12 9 10 11 fvmpt k n 1 n + 1 k = 1 k + 1
13 12 adantl k n 1 n + 1 k = 1 k + 1
14 2 3 4 3 7 13 divcnvshft n 1 n + 1 0
15 seqex seq 1 + F V
16 15 a1i seq 1 + F V
17 peano2nn k k + 1
18 17 adantl k k + 1
19 18 nnrecred k 1 k + 1
20 19 recnd k 1 k + 1
21 13 20 eqeltrd k n 1 n + 1 k
22 13 oveq2d k 1 n 1 n + 1 k = 1 1 k + 1
23 elfznn j 1 k j
24 23 adantl k j 1 k j
25 24 nncnd k j 1 k j
26 peano2cn j j + 1
27 25 26 syl k j 1 k j + 1
28 peano2nn j j + 1
29 24 28 syl k j 1 k j + 1
30 24 29 nnmulcld k j 1 k j j + 1
31 30 nncnd k j 1 k j j + 1
32 30 nnne0d k j 1 k j j + 1 0
33 27 25 31 32 divsubdird k j 1 k j + 1 - j j j + 1 = j + 1 j j + 1 j j j + 1
34 ax-1cn 1
35 pncan2 j 1 j + 1 - j = 1
36 25 34 35 sylancl k j 1 k j + 1 - j = 1
37 36 oveq1d k j 1 k j + 1 - j j j + 1 = 1 j j + 1
38 27 mulid1d k j 1 k j + 1 1 = j + 1
39 27 25 mulcomd k j 1 k j + 1 j = j j + 1
40 38 39 oveq12d k j 1 k j + 1 1 j + 1 j = j + 1 j j + 1
41 1cnd k j 1 k 1
42 24 nnne0d k j 1 k j 0
43 29 nnne0d k j 1 k j + 1 0
44 41 25 27 42 43 divcan5d k j 1 k j + 1 1 j + 1 j = 1 j
45 40 44 eqtr3d k j 1 k j + 1 j j + 1 = 1 j
46 25 mulid1d k j 1 k j 1 = j
47 46 oveq1d k j 1 k j 1 j j + 1 = j j j + 1
48 41 27 25 43 42 divcan5d k j 1 k j 1 j j + 1 = 1 j + 1
49 47 48 eqtr3d k j 1 k j j j + 1 = 1 j + 1
50 45 49 oveq12d k j 1 k j + 1 j j + 1 j j j + 1 = 1 j 1 j + 1
51 33 37 50 3eqtr3d k j 1 k 1 j j + 1 = 1 j 1 j + 1
52 51 sumeq2dv k j = 1 k 1 j j + 1 = j = 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 syl6eq n = 1 1 n = 1
58 oveq2 n = k + 1 1 n = 1 k + 1
59 nnz k k
60 59 adantl k k
61 18 2 eleqtrdi k k + 1 1
62 elfznn n 1 k + 1 n
63 62 adantl k n 1 k + 1 n
64 63 nnrecred k n 1 k + 1 1 n
65 64 recnd k n 1 k + 1 1 n
66 53 54 57 58 60 61 65 telfsum k j = 1 k 1 j 1 j + 1 = 1 1 k + 1
67 52 66 eqtrd k j = 1 k 1 j 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 n + 1 = j j + 1
71 70 oveq2d n = j 1 n n + 1 = 1 j j + 1
72 ovex 1 j j + 1 V
73 71 1 72 fvmpt j F j = 1 j j + 1
74 24 73 syl k j 1 k F j = 1 j j + 1
75 simpr k k
76 75 2 eleqtrdi k k 1
77 30 nnrecred k j 1 k 1 j j + 1
78 77 recnd k j 1 k 1 j j + 1
79 74 76 78 fsumser k j = 1 k 1 j j + 1 = seq 1 + F k
80 22 67 79 3eqtr2rd k seq 1 + F k = 1 n 1 n + 1 k
81 2 3 14 4 16 21 80 climsubc2 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