Metamath Proof Explorer


Theorem emcllem5

Description: Lemma for emcl . The partial sums of the series T , which is used in Definition df-em , is in fact the same as G . (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses emcl.1 F = n m = 1 n 1 m log n
emcl.2 G = n m = 1 n 1 m log n + 1
emcl.3 H = n log 1 + 1 n
emcl.4 T = n 1 n log 1 + 1 n
Assertion emcllem5 G = seq 1 + T

Proof

Step Hyp Ref Expression
1 emcl.1 F = n m = 1 n 1 m log n
2 emcl.2 G = n m = 1 n 1 m log n + 1
3 emcl.3 H = n log 1 + 1 n
4 emcl.4 T = n 1 n log 1 + 1 n
5 elfznn m 1 n m
6 5 adantl n m 1 n m
7 6 nncnd n m 1 n m
8 1cnd n m 1 n 1
9 6 nnne0d n m 1 n m 0
10 7 8 7 9 divdird n m 1 n m + 1 m = m m + 1 m
11 7 9 dividd n m 1 n m m = 1
12 11 oveq1d n m 1 n m m + 1 m = 1 + 1 m
13 10 12 eqtrd n m 1 n m + 1 m = 1 + 1 m
14 13 fveq2d n m 1 n log m + 1 m = log 1 + 1 m
15 peano2nn m m + 1
16 6 15 syl n m 1 n m + 1
17 16 nnrpd n m 1 n m + 1 +
18 6 nnrpd n m 1 n m +
19 17 18 relogdivd n m 1 n log m + 1 m = log m + 1 log m
20 14 19 eqtr3d n m 1 n log 1 + 1 m = log m + 1 log m
21 20 sumeq2dv n m = 1 n log 1 + 1 m = m = 1 n log m + 1 log m
22 fveq2 x = m log x = log m
23 fveq2 x = m + 1 log x = log m + 1
24 fveq2 x = 1 log x = log 1
25 fveq2 x = n + 1 log x = log n + 1
26 nnz n n
27 peano2nn n n + 1
28 nnuz = 1
29 27 28 eleqtrdi n n + 1 1
30 elfznn x 1 n + 1 x
31 30 adantl n x 1 n + 1 x
32 31 nnrpd n x 1 n + 1 x +
33 32 relogcld n x 1 n + 1 log x
34 33 recnd n x 1 n + 1 log x
35 22 23 24 25 26 29 34 telfsum2 n m = 1 n log m + 1 log m = log n + 1 log 1
36 log1 log 1 = 0
37 36 oveq2i log n + 1 log 1 = log n + 1 0
38 27 nnrpd n n + 1 +
39 38 relogcld n log n + 1
40 39 recnd n log n + 1
41 40 subid1d n log n + 1 0 = log n + 1
42 37 41 syl5eq n log n + 1 log 1 = log n + 1
43 21 35 42 3eqtrd n m = 1 n log 1 + 1 m = log n + 1
44 43 oveq2d n m = 1 n 1 m m = 1 n log 1 + 1 m = m = 1 n 1 m log n + 1
45 fzfid n 1 n Fin
46 6 nnrecred n m 1 n 1 m
47 46 recnd n m 1 n 1 m
48 1rp 1 +
49 18 rpreccld n m 1 n 1 m +
50 rpaddcl 1 + 1 m + 1 + 1 m +
51 48 49 50 sylancr n m 1 n 1 + 1 m +
52 51 relogcld n m 1 n log 1 + 1 m
53 52 recnd n m 1 n log 1 + 1 m
54 45 47 53 fsumsub n m = 1 n 1 m log 1 + 1 m = m = 1 n 1 m m = 1 n log 1 + 1 m
55 oveq2 n = m 1 n = 1 m
56 55 oveq2d n = m 1 + 1 n = 1 + 1 m
57 56 fveq2d n = m log 1 + 1 n = log 1 + 1 m
58 55 57 oveq12d n = m 1 n log 1 + 1 n = 1 m log 1 + 1 m
59 ovex 1 m log 1 + 1 m V
60 58 4 59 fvmpt m T m = 1 m log 1 + 1 m
61 6 60 syl n m 1 n T m = 1 m log 1 + 1 m
62 id n n
63 62 28 eleqtrdi n n 1
64 46 52 resubcld n m 1 n 1 m log 1 + 1 m
65 64 recnd n m 1 n 1 m log 1 + 1 m
66 61 63 65 fsumser n m = 1 n 1 m log 1 + 1 m = seq 1 + T n
67 54 66 eqtr3d n m = 1 n 1 m m = 1 n log 1 + 1 m = seq 1 + T n
68 44 67 eqtr3d n m = 1 n 1 m log n + 1 = seq 1 + T n
69 68 mpteq2ia n m = 1 n 1 m log n + 1 = n seq 1 + T n
70 1z 1
71 seqfn 1 seq 1 + T Fn 1
72 70 71 ax-mp seq 1 + T Fn 1
73 28 fneq2i seq 1 + T Fn seq 1 + T Fn 1
74 72 73 mpbir seq 1 + T Fn
75 dffn5 seq 1 + T Fn seq 1 + T = n seq 1 + T n
76 74 75 mpbi seq 1 + T = n seq 1 + T n
77 69 2 76 3eqtr4i G = seq 1 + T