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 ffvelrni ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) ∈ ℝ )
35 32 34 ax-mp ( 𝐹 ‘ 1 ) ∈ ℝ
36 27 ffvelrni ( 𝑘 ∈ ℕ → ( 𝐺𝑘 ) ∈ ℝ )
37 36 adantl ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺𝑘 ) ∈ ℝ )
38 33 ffvelrni ( 𝑘 ∈ ℕ → ( 𝐹𝑘 ) ∈ ℝ )
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 ffvelrni ( ( 𝑘 + 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 addid1i ( γ + 0 ) = γ
105 100 104 breqtrdi ( ⊤ → 𝐹 ⇝ γ )
106 105 mptru 𝐹 ⇝ γ
107 106 101 pm3.2i ( 𝐹 ⇝ γ ∧ 𝐺 ⇝ γ )