Metamath Proof Explorer

Theorem emcllem3

Description: Lemma for emcl . The function H is the difference between F and 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 / 𝑛 ) ) ) )
Assertion emcllem3 ( 𝑁 ∈ ℕ → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) − ( 𝐺 ‘ 𝑁 ) ) )

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 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
5 4 nnrpd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ+ )
6 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
7 5 6 relogdivd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
8 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
9 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
10 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
11 8 9 8 10 divdird ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) = ( ( 𝑁 / 𝑁 ) + ( 1 / 𝑁 ) ) )
12 8 10 dividd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
13 12 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 𝑁 ) + ( 1 / 𝑁 ) ) = ( 1 + ( 1 / 𝑁 ) ) )
14 11 13 eqtr2d ⊢ ( 𝑁 ∈ ℕ → ( 1 + ( 1 / 𝑁 ) ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
15 14 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 1 + ( 1 / 𝑁 ) ) ) = ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
16 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
17 elfznn ⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → 𝑚 ∈ ℕ )
18 17 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑚 ∈ ℕ )
19 18 nnrecred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑚 ) ∈ ℝ )
20 16 19 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) ∈ ℝ )
21 20 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) ∈ ℂ )
22 6 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℝ )
23 22 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℂ )
24 5 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
25 24 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
26 21 23 25 nnncan1d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) − ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ) = ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
27 7 15 26 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 1 + ( 1 / 𝑁 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) − ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ) )
28 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 / 𝑛 ) = ( 1 / 𝑁 ) )
29 28 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 𝑁 ) ) )
30 29 fveq2d ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) = ( log ‘ ( 1 + ( 1 / 𝑁 ) ) ) )
31 fvex ⊢ ( log ‘ ( 1 + ( 1 / 𝑁 ) ) ) ∈ V
32 30 3 31 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐻 ‘ 𝑁 ) = ( log ‘ ( 1 + ( 1 / 𝑁 ) ) ) )
33 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
34 33 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) )
35 fveq2 ⊢ ( 𝑛 = 𝑁 → ( log ‘ 𝑛 ) = ( log ‘ 𝑁 ) )
36 34 35 oveq12d ⊢ ( 𝑛 = 𝑁 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) )
37 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ∈ V
38 36 1 37 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) )
39 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝑛 + 1 ) ) = ( log ‘ ( 𝑁 + 1 ) ) )
40 34 39 oveq12d ⊢ ( 𝑛 = 𝑁 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
41 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ V
42 40 2 41 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 ‘ 𝑁 ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
43 38 42 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 ‘ 𝑁 ) − ( 𝐺 ‘ 𝑁 ) ) = ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) − ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ) )
44 27 32 43 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) − ( 𝐺 ‘ 𝑁 ) ) )