Metamath Proof Explorer

Theorem emcllem4

Description: Lemma for emcl . The difference between series F and G tends to zero. (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 emcllem4 𝐻 ⇝ 0

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 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
6 ax-1cn ⊢ 1 ∈ ℂ
7 divcnv ⊢ ( 1 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
8 6 7 mp1i ⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
9 nnex ⊢ ℕ ∈ V
10 9 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) ∈ V
11 3 10 eqeltri ⊢ 𝐻 ∈ V
12 11 a1i ⊢ ( ⊤ → 𝐻 ∈ V )
13 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1 / 𝑛 ) = ( 1 / 𝑚 ) )
14 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
15 ovex ⊢ ( 1 / 𝑚 ) ∈ V
16 13 14 15 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑚 ) = ( 1 / 𝑚 ) )
17 16 adantl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑚 ) = ( 1 / 𝑚 ) )
18 nnrecre ⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℝ )
19 18 adantl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 1 / 𝑚 ) ∈ ℝ )
20 17 19 eqeltrd ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑚 ) ∈ ℝ )
21 13 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 𝑚 ) ) )
22 21 fveq2d ⊢ ( 𝑛 = 𝑚 → ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) = ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) )
23 fvex ⊢ ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) ∈ V
24 22 3 23 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝐻 ‘ 𝑚 ) = ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) )
25 24 adantl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) = ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) )
26 1rp ⊢ 1 ∈ ℝ+
27 nnrp ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
28 27 adantl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
29 28 rpreccld ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 1 / 𝑚 ) ∈ ℝ+ )
30 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( 1 / 𝑚 ) ∈ ℝ+ ) → ( 1 + ( 1 / 𝑚 ) ) ∈ ℝ+ )
31 26 29 30 sylancr ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 1 + ( 1 / 𝑚 ) ) ∈ ℝ+ )
32 31 rpred ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 1 + ( 1 / 𝑚 ) ) ∈ ℝ )
33 1re ⊢ 1 ∈ ℝ
34 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ ( 1 / 𝑚 ) ∈ ℝ+ ) → 1 < ( 1 + ( 1 / 𝑚 ) ) )
35 33 29 34 sylancr ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → 1 < ( 1 + ( 1 / 𝑚 ) ) )
36 32 35 rplogcld ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) ∈ ℝ+ )
37 25 36 eqeltrd ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ∈ ℝ+ )
38 37 rpred ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ∈ ℝ )
39 31 relogcld ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) ∈ ℝ )
40 efgt1p ⊢ ( ( 1 / 𝑚 ) ∈ ℝ+ → ( 1 + ( 1 / 𝑚 ) ) < ( exp ‘ ( 1 / 𝑚 ) ) )
41 29 40 syl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 1 + ( 1 / 𝑚 ) ) < ( exp ‘ ( 1 / 𝑚 ) ) )
42 19 rpefcld ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( exp ‘ ( 1 / 𝑚 ) ) ∈ ℝ+ )
43 logltb ⊢ ( ( ( 1 + ( 1 / 𝑚 ) ) ∈ ℝ+ ∧ ( exp ‘ ( 1 / 𝑚 ) ) ∈ ℝ+ ) → ( ( 1 + ( 1 / 𝑚 ) ) < ( exp ‘ ( 1 / 𝑚 ) ) ↔ ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) < ( log ‘ ( exp ‘ ( 1 / 𝑚 ) ) ) ) )
44 31 42 43 syl2anc ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( ( 1 + ( 1 / 𝑚 ) ) < ( exp ‘ ( 1 / 𝑚 ) ) ↔ ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) < ( log ‘ ( exp ‘ ( 1 / 𝑚 ) ) ) ) )
45 41 44 mpbid ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) < ( log ‘ ( exp ‘ ( 1 / 𝑚 ) ) ) )
46 19 relogefd ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( exp ‘ ( 1 / 𝑚 ) ) ) = ( 1 / 𝑚 ) )
47 45 46 breqtrd ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) < ( 1 / 𝑚 ) )
48 39 19 47 ltled ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑚 ) ) ) ≤ ( 1 / 𝑚 ) )
49 48 25 17 3brtr4d ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑚 ) )
50 37 rpge0d ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( 𝐻 ‘ 𝑚 ) )
51 4 5 8 12 20 38 49 50 climsqz2 ⊢ ( ⊤ → 𝐻 ⇝ 0 )
52 51 mptru ⊢ 𝐻 ⇝ 0