Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
4 | 3 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (1 + (1 / 𝑛)) = (1 + (1 / 𝑘))) |
5 | 4 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (log‘(1 + (1 / 𝑛))) = (log‘(1 + (1 / 𝑘)))) |
6 | 3, 5 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))) = ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))) |
7 | | emcl.4 |
. . . . . . . . 9
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 /
𝑛))))) |
8 | | ovex 6577 |
. . . . . . . . 9
⊢ ((1 /
𝑘) − (log‘(1 +
(1 / 𝑘)))) ∈
V |
9 | 6, 7, 8 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑇‘𝑘) = ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))) |
11 | | nnrecre 10934 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
12 | 11 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / 𝑘) ∈ ℝ) |
13 | | 1rp 11712 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ+ |
14 | | nnrp 11718 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
15 | 14 | rpreccld 11758 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
16 | 15 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / 𝑘) ∈
ℝ+) |
17 | | rpaddcl 11730 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ+ ∧ (1 / 𝑘) ∈ ℝ+) → (1 + (1
/ 𝑘)) ∈
ℝ+) |
18 | 13, 16, 17 | sylancr 694 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 + (1 / 𝑘)) ∈
ℝ+) |
19 | 18 | relogcld 24173 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (log‘(1 + (1 / 𝑘))) ∈ ℝ) |
20 | 12, 19 | resubcld 10337 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) ∈
ℝ) |
21 | 20 | recnd 9947 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) ∈
ℂ) |
22 | | emcl.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) |
23 | | emcl.2 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) |
24 | | emcl.3 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 /
𝑛)))) |
25 | 22, 23, 24, 7 | emcllem5 24526 |
. . . . . . . . 9
⊢ 𝐺 = seq1( + , 𝑇) |
26 | 22, 23 | emcllem1 24522 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ⟶ℝ ∧
𝐺:ℕ⟶ℝ) |
27 | 26 | simpri 477 |
. . . . . . . . . . 11
⊢ 𝐺:ℕ⟶ℝ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐺:ℕ⟶ℝ) |
29 | 22, 23 | emcllem2 24523 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ∧ (𝐺‘𝑘) ≤ (𝐺‘(𝑘 + 1)))) |
30 | 29 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐺‘(𝑘 + 1))) |
31 | 30 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ≤ (𝐺‘(𝑘 + 1))) |
32 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
33 | 26 | simpli 473 |
. . . . . . . . . . . . 13
⊢ 𝐹:ℕ⟶ℝ |
34 | 33 | ffvelrni 6266 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ → (𝐹‘1)
∈ ℝ) |
35 | 32, 34 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐹‘1) ∈
ℝ |
36 | 27 | ffvelrni 6266 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
38 | 33 | ffvelrni 6266 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℝ) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
40 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘1) ∈ ℝ) |
41 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘(1 + (1 / 𝑘))) ∈ V |
42 | 5, 24, 41 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = (log‘(1 + (1 / 𝑘)))) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) = (log‘(1 + (1 / 𝑘)))) |
44 | 22, 23, 24 | emcllem3 24524 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) |
46 | 43, 45 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (log‘(1 + (1 / 𝑘))) = ((𝐹‘𝑘) − (𝐺‘𝑘))) |
47 | | 1re 9918 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
48 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → (1 + (1 / 𝑘)) ∈
ℝ) |
49 | 47, 12, 48 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 + (1 / 𝑘)) ∈ ℝ) |
50 | | ltaddrp 11743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → 1 <
(1 + (1 / 𝑘))) |
51 | 47, 16, 50 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 1 < (1 + (1 / 𝑘))) |
52 | 49, 51 | rplogcld 24179 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (log‘(1 + (1 / 𝑘))) ∈
ℝ+) |
53 | 46, 52 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈
ℝ+) |
54 | 53 | rpge0d 11752 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 0 ≤ ((𝐹‘𝑘) − (𝐺‘𝑘))) |
55 | 39, 37 | subge0d 10496 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (0 ≤ ((𝐹‘𝑘) − (𝐺‘𝑘)) ↔ (𝐺‘𝑘) ≤ (𝐹‘𝑘))) |
56 | 54, 55 | mpbid 221 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ≤ (𝐹‘𝑘)) |
57 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
58 | 57 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → ((𝐹‘𝑥) ≤ (𝐹‘1) ↔ (𝐹‘1) ≤ (𝐹‘1))) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → (𝐹‘𝑥) = (𝐹‘𝑘)) |
60 | 59 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → ((𝐹‘𝑥) ≤ (𝐹‘1) ↔ (𝐹‘𝑘) ≤ (𝐹‘1))) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
62 | 61 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ≤ (𝐹‘1) ↔ (𝐹‘(𝑘 + 1)) ≤ (𝐹‘1))) |
63 | 35 | leidi 10441 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘1) ≤ (𝐹‘1) |
64 | 29 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
65 | | peano2nn 10909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
66 | 33 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 1) ∈ ℕ →
(𝐹‘(𝑘 + 1)) ∈
ℝ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
68 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝐹‘1) ∈
ℝ) |
69 | | letr 10010 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘(𝑘 + 1)) ∈ ℝ ∧ (𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘1) ∈ ℝ) → (((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ≤ (𝐹‘1)) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘1))) |
70 | 67, 38, 68, 69 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ∧ (𝐹‘𝑘) ≤ (𝐹‘1)) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘1))) |
71 | 64, 70 | mpand 707 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) ≤ (𝐹‘1) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘1))) |
72 | 58, 60, 62, 60, 63, 71 | nnind 10915 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ≤ (𝐹‘1)) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘1)) |
74 | 37, 39, 40, 56, 73 | letrd 10073 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ≤ (𝐹‘1)) |
75 | 74 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (⊤
→ ∀𝑘 ∈
ℕ (𝐺‘𝑘) ≤ (𝐹‘1)) |
76 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐹‘1) → ((𝐺‘𝑘) ≤ 𝑥 ↔ (𝐺‘𝑘) ≤ (𝐹‘1))) |
77 | 76 | ralbidv 2969 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐹‘1) → (∀𝑘 ∈ ℕ (𝐺‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝐺‘𝑘) ≤ (𝐹‘1))) |
78 | 77 | rspcev 3282 |
. . . . . . . . . . 11
⊢ (((𝐹‘1) ∈ ℝ ∧
∀𝑘 ∈ ℕ
(𝐺‘𝑘) ≤ (𝐹‘1)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝐺‘𝑘) ≤ 𝑥) |
79 | 35, 75, 78 | sylancr 694 |
. . . . . . . . . 10
⊢ (⊤
→ ∃𝑥 ∈
ℝ ∀𝑘 ∈
ℕ (𝐺‘𝑘) ≤ 𝑥) |
80 | 1, 2, 28, 31, 79 | climsup 14248 |
. . . . . . . . 9
⊢ (⊤
→ 𝐺 ⇝ sup(ran
𝐺, ℝ, <
)) |
81 | 25, 80 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ (⊤
→ seq1( + , 𝑇) ⇝
sup(ran 𝐺, ℝ, <
)) |
82 | | climrel 14071 |
. . . . . . . . 9
⊢ Rel
⇝ |
83 | 82 | releldmi 5283 |
. . . . . . . 8
⊢ (seq1( +
, 𝑇) ⇝ sup(ran 𝐺, ℝ, < ) → seq1( +
, 𝑇) ∈ dom ⇝
) |
84 | 81, 83 | syl 17 |
. . . . . . 7
⊢ (⊤
→ seq1( + , 𝑇) ∈
dom ⇝ ) |
85 | 1, 2, 10, 21, 84 | isumclim2 14331 |
. . . . . 6
⊢ (⊤
→ seq1( + , 𝑇) ⇝
Σ𝑘 ∈ ℕ ((1
/ 𝑘) − (log‘(1
+ (1 / 𝑘))))) |
86 | | df-em 24519 |
. . . . . 6
⊢ γ =
Σ𝑘 ∈ ℕ ((1
/ 𝑘) − (log‘(1
+ (1 / 𝑘)))) |
87 | 85, 25, 86 | 3brtr4g 4617 |
. . . . 5
⊢ (⊤
→ 𝐺 ⇝
γ) |
88 | | nnex 10903 |
. . . . . . . 8
⊢ ℕ
∈ V |
89 | 88 | mptex 6390 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦
(Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) ∈ V |
90 | 22, 89 | eqeltri 2684 |
. . . . . 6
⊢ 𝐹 ∈ V |
91 | 90 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐹 ∈
V) |
92 | 22, 23, 24 | emcllem4 24525 |
. . . . . 6
⊢ 𝐻 ⇝ 0 |
93 | 92 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐻 ⇝
0) |
94 | 37 | recnd 9947 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℂ) |
95 | 39, 37 | resubcld 10337 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ) |
96 | 45, 95 | eqeltrd 2688 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) ∈ ℝ) |
97 | 96 | recnd 9947 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) ∈ ℂ) |
98 | 45 | oveq2d 6565 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐺‘𝑘) + (𝐻‘𝑘)) = ((𝐺‘𝑘) + ((𝐹‘𝑘) − (𝐺‘𝑘)))) |
99 | 39 | recnd 9947 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
100 | 94, 99 | pncan3d 10274 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝐺‘𝑘) + ((𝐹‘𝑘) − (𝐺‘𝑘))) = (𝐹‘𝑘)) |
101 | 98, 100 | eqtr2d 2645 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) = ((𝐺‘𝑘) + (𝐻‘𝑘))) |
102 | 1, 2, 87, 91, 93, 94, 97, 101 | climadd 14210 |
. . . 4
⊢ (⊤
→ 𝐹 ⇝ (γ +
0)) |
103 | 87 | trud 1484 |
. . . . . 6
⊢ 𝐺 ⇝
γ |
104 | | climcl 14078 |
. . . . . 6
⊢ (𝐺 ⇝ γ → γ
∈ ℂ) |
105 | 103, 104 | ax-mp 5 |
. . . . 5
⊢ γ
∈ ℂ |
106 | 105 | addid1i 10102 |
. . . 4
⊢ (γ
+ 0) = γ |
107 | 102, 106 | syl6breq 4624 |
. . 3
⊢ (⊤
→ 𝐹 ⇝
γ) |
108 | 107 | trud 1484 |
. 2
⊢ 𝐹 ⇝
γ |
109 | 108, 103 | pm3.2i 470 |
1
⊢ (𝐹 ⇝ γ ∧ 𝐺 ⇝
γ) |