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 ⊢ F = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n
emcl.2 ⊢ G = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1
emcl.3 ⊢ H = n ∈ ℕ ⟼ log ⁡ 1 + 1 n
emcl.4 ⊢ T = n ∈ ℕ ⟼ 1 n − log ⁡ 1 + 1 n
Assertion emcllem6 ⊢ F ⇝ γ ∧ G ⇝ γ

Proof

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