Metamath Proof Explorer

Theorem emcllem6

Description: Lemma for emcl . By the previous lemmas, F and G must approach a common limit, which is gamma by definition. (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 emcllem6 ( 𝐹 ⇝ γ ∧ 𝐺 ⇝ γ )

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 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
7 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
8 7 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 𝑘 ) ) )
9 8 fveq2d ⊢ ( 𝑛 = 𝑘 → ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) = ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
10 7 9 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) = ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) )
11 ovex ⊢ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) ∈ V
12 10 4 11 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑇 ‘ 𝑘 ) = ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) )
13 12 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) = ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) )
14 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
15 14 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
16 1rp ⊢ 1 ∈ ℝ+
17 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
18 17 rpreccld ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
19 18 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ+ )
20 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( 1 / 𝑘 ) ∈ ℝ+ ) → ( 1 + ( 1 / 𝑘 ) ) ∈ ℝ+ )
21 16 19 20 sylancr ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 + ( 1 / 𝑘 ) ) ∈ ℝ+ )
22 21 relogcld ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ∈ ℝ )
23 15 22 resubcld ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) ∈ ℝ )
24 23 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) ∈ ℂ )
25 1 2 3 4 emcllem5 ⊢ 𝐺 = seq 1 ( + , 𝑇 )
26 1 2 emcllem1 ⊢ ( 𝐹 : ℕ ⟶ ℝ ∧ 𝐺 : ℕ ⟶ ℝ )
27 26 simpri ⊢ 𝐺 : ℕ ⟶ ℝ
28 27 a1i ⊢ ( ⊤ → 𝐺 : ℕ ⟶ ℝ )
29 1 2 emcllem2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
30 29 simprd ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
31 30 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
32 1nn ⊢ 1 ∈ ℕ
33 26 simpli ⊢ 𝐹 : ℕ ⟶ ℝ
34 33 ffvelcdmi ⊢ ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) ∈ ℝ )
35 32 34 ax-mp ⊢ ( 𝐹 ‘ 1 ) ∈ ℝ
36 27 ffvelcdmi ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
37 36 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
38 33 ffvelcdmi ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
39 38 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
40 35 a1i ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 1 ) ∈ ℝ )
41 fvex ⊢ ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ∈ V
42 9 3 41 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐻 ‘ 𝑘 ) = ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
43 42 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
44 1 2 3 emcllem3 ⊢ ( 𝑘 ∈ ℕ → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
45 44 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
46 43 45 eqtr3d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
47 1re ⊢ 1 ∈ ℝ
48 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ ) → ( 1 + ( 1 / 𝑘 ) ) ∈ ℝ )
49 47 15 48 sylancr ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 1 + ( 1 / 𝑘 ) ) ∈ ℝ )
50 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ+ ) → 1 < ( 1 + ( 1 / 𝑘 ) ) )
51 47 19 50 sylancr ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 1 < ( 1 + ( 1 / 𝑘 ) ) )
52 49 51 rplogcld ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ∈ ℝ+ )
53 46 52 eqeltrrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ+ )
54 53 rpge0d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
55 39 37 subge0d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
56 54 55 mpbid ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
57 fveq2 ⊢ ( 𝑥 = 1 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 1 ) )
58 57 breq1d ⊢ ( 𝑥 = 1 → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 1 ) ↔ ( 𝐹 ‘ 1 ) ≤ ( 𝐹 ‘ 1 ) ) )
59 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
60 59 breq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 1 ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) ) )
61 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
62 61 breq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 1 ) ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 1 ) ) )
63 35 leidi ⊢ ( 𝐹 ‘ 1 ) ≤ ( 𝐹 ‘ 1 )
64 29 simpld ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
65 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
66 33 ffvelcdmi ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
67 65 66 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
68 35 a1i ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 1 ) ∈ ℝ )
69 letr ⊢ ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 1 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 1 ) ) )
70 67 38 68 69 syl3anc ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 1 ) ) )
71 64 70 mpand ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 1 ) ) )
72 58 60 62 60 63 71 nnind ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) )
73 72 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) )
74 37 39 40 56 73 letrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) )
75 74 ralrimiva ⊢ ( ⊤ → ∀ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) )
76 brralrspcev ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 1 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ≤ 𝑥 )
77 35 75 76 sylancr ⊢ ( ⊤ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ≤ 𝑥 )
78 5 6 28 31 77 climsup ⊢ ( ⊤ → 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) )
79 25 78 eqbrtrrid ⊢ ( ⊤ → seq 1 ( + , 𝑇 ) ⇝ sup ( ran 𝐺 , ℝ , < ) )
80 climrel ⊢ Rel ⇝
81 80 releldmi ⊢ ( seq 1 ( + , 𝑇 ) ⇝ sup ( ran 𝐺 , ℝ , < ) → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )
82 79 81 syl ⊢ ( ⊤ → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )
83 5 6 13 24 82 isumclim2 ⊢ ( ⊤ → seq 1 ( + , 𝑇 ) ⇝ Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) )
84 df-em ⊢ γ = Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
85 83 25 84 3brtr4g ⊢ ( ⊤ → 𝐺 ⇝ γ )
86 nnex ⊢ ℕ ∈ V
87 86 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ) ∈ V
88 1 87 eqeltri ⊢ 𝐹 ∈ V
89 88 a1i ⊢ ( ⊤ → 𝐹 ∈ V )
90 1 2 3 emcllem4 ⊢ 𝐻 ⇝ 0
91 90 a1i ⊢ ( ⊤ → 𝐻 ⇝ 0 )
92 37 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
93 39 37 resubcld ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
94 45 93 eqeltrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ℝ )
95 94 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ℂ )
96 45 oveq2d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) + ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐺 ‘ 𝑘 ) + ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) )
97 39 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
98 92 97 pncan3d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) + ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝐹 ‘ 𝑘 ) )
99 96 98 eqtr2d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) + ( 𝐻 ‘ 𝑘 ) ) )
100 5 6 85 89 91 92 95 99 climadd ⊢ ( ⊤ → 𝐹 ⇝ ( γ + 0 ) )
101 85 mptru ⊢ 𝐺 ⇝ γ
102 climcl ⊢ ( 𝐺 ⇝ γ → γ ∈ ℂ )
103 101 102 ax-mp ⊢ γ ∈ ℂ
104 103 addridi ⊢ ( γ + 0 ) = γ
105 100 104 breqtrdi ⊢ ( ⊤ → 𝐹 ⇝ γ )
106 105 mptru ⊢ 𝐹 ⇝ γ
107 106 101 pm3.2i ⊢ ( 𝐹 ⇝ γ ∧ 𝐺 ⇝ γ )