Step | Hyp | Ref
| Expression |
1 | | faclimlem1 33709 |
. 2
⊢ (𝑀 ∈ ℕ0
→ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))))) |
2 | | nnuz 12621 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
3 | | 1zzd 12351 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ 1 ∈ ℤ) |
4 | | 1cnd 10970 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ 1 ∈ ℂ) |
5 | | nn0p1nn 12272 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
6 | 5 | nnzd 12425 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℤ) |
7 | | nnex 11979 |
. . . . . . 7
⊢ ℕ
∈ V |
8 | 7 | mptex 7099 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) ∈ V |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) ∈ V) |
10 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1)) |
11 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝑚 + (𝑀 + 1)) = (𝑘 + (𝑀 + 1))) |
12 | 10, 11 | oveq12d 7293 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / (𝑚 + (𝑀 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) |
13 | | eqid 2738 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) = (𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) |
14 | | ovex 7308 |
. . . . . . 7
⊢ ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ V |
15 | 12, 13, 14 | fvmpt 6875 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) |
16 | 15 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑚 ∈ ℕ
↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) |
17 | 2, 3, 4, 6, 9, 16 | divcnvlin 33698 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) ⇝ 1) |
18 | 5 | nncnd 11989 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℂ) |
19 | 7 | mptex 7099 |
. . . . 5
⊢ (𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) ∈ V |
20 | 19 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑀 + 1) ·
((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) ∈ V) |
21 | | peano2nn 11985 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
22 | 21 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ (𝑚 + 1) ∈
ℕ) |
23 | 22 | nnred 11988 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ (𝑚 + 1) ∈
ℝ) |
24 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℕ) |
25 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ (𝑀 + 1) ∈
ℕ) |
26 | 24, 25 | nnaddcld 12025 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ (𝑚 + (𝑀 + 1)) ∈
ℕ) |
27 | 23, 26 | nndivred 12027 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))) ∈ ℝ) |
28 | 27 | recnd 11003 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈ ℕ)
→ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))) ∈ ℂ) |
29 | 28 | fmpttd 6989 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑚 + 1) / (𝑚 + (𝑀 +
1)))):ℕ⟶ℂ) |
30 | 29 | ffvelrnda 6961 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑚 ∈ ℕ
↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘) ∈ ℂ) |
31 | 12 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) |
32 | | eqid 2738 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) = (𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) |
33 | | ovex 7308 |
. . . . . . 7
⊢ ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) ∈ V |
34 | 31, 32, 33 | fvmpt 6875 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) |
35 | 15 | oveq2d 7291 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑀 + 1) · ((𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘)) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) |
36 | 34, 35 | eqtr4d 2781 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑚 + 1) / (𝑚 + (𝑀 + 1)))))‘𝑘) = ((𝑀 + 1) · ((𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘))) |
37 | 36 | adantl 482 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑚 ∈ ℕ
↦ ((𝑀 + 1) ·
((𝑚 + 1) / (𝑚 + (𝑀 + 1)))))‘𝑘) = ((𝑀 + 1) · ((𝑚 ∈ ℕ ↦ ((𝑚 + 1) / (𝑚 + (𝑀 + 1))))‘𝑘))) |
38 | 2, 3, 17, 18, 20, 30, 37 | climmulc2 15346 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑀 + 1) ·
((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) ⇝ ((𝑀 + 1) · 1)) |
39 | 18 | mulid1d 10992 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ((𝑀 + 1) · 1)
= (𝑀 + 1)) |
40 | 38, 39 | breqtrd 5100 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑚 ∈ ℕ
↦ ((𝑀 + 1) ·
((𝑚 + 1) / (𝑚 + (𝑀 + 1))))) ⇝ (𝑀 + 1)) |
41 | 1, 40 | eqbrtrd 5096 |
1
⊢ (𝑀 ∈ ℕ0
→ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1)) |