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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
emcl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
emcl.3 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
emcl.4 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
Assertion emcllem5 𝐺 = seq 1 ( + , 𝑇 )

Proof

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