Step | Hyp | Ref
| Expression |
1 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑎 = 1 → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1)) |
2 | | 1z 12348 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
3 | | seq1 13730 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . 9
⊢ (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) |
5 | 1, 4 | eqtrdi 2796 |
. . . . . . . 8
⊢ (𝑎 = 1 → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1)) |
6 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (𝑎 + 1) = (1 + 1)) |
7 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 1 → (𝑎 + (𝑀 + 1)) = (1 + (𝑀 + 1))) |
8 | 6, 7 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑎 = 1 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((1 + 1) / (1 + (𝑀 + 1)))) |
9 | 8 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑎 = 1 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1))))) |
10 | 5, 9 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑎 = 1 → ((seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))) |
11 | 10 | imbi2d 341 |
. . . . . 6
⊢ (𝑎 = 1 → ((𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1))))))) |
12 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑎 = 𝑘 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘)) |
13 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → (𝑎 + 1) = (𝑘 + 1)) |
14 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → (𝑎 + (𝑀 + 1)) = (𝑘 + (𝑀 + 1))) |
15 | 13, 14 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑎 = 𝑘 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) |
16 | 15 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑎 = 𝑘 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) |
17 | 12, 16 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))) |
18 | 17 | imbi2d 341 |
. . . . . 6
⊢ (𝑎 = 𝑘 → ((𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))))) |
19 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑎 = (𝑘 + 1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1))) |
20 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑘 + 1) → (𝑎 + 1) = ((𝑘 + 1) + 1)) |
21 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑘 + 1) → (𝑎 + (𝑀 + 1)) = ((𝑘 + 1) + (𝑀 + 1))) |
22 | 20, 21 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑎 = (𝑘 + 1) → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))) |
23 | 22 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑎 = (𝑘 + 1) → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))) |
24 | 19, 23 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑎 = (𝑘 + 1) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))) |
25 | 24 | imbi2d 341 |
. . . . . 6
⊢ (𝑎 = (𝑘 + 1) → ((𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))))) |
26 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏)) |
27 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑎 + 1) = (𝑏 + 1)) |
28 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑎 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1))) |
29 | 27, 28 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) |
30 | 29 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))) |
31 | 26, 30 | eqeq12d 2756 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))) |
32 | 31 | imbi2d 341 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))) |
33 | | 1nn 11982 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
34 | | oveq2 7277 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝑀 / 𝑛) = (𝑀 / 1)) |
35 | 34 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / 1))) |
36 | | oveq2 7277 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) |
37 | 36 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (1 + (1 / 𝑛)) = (1 + (1 /
1))) |
38 | 35, 37 | oveq12d 7287 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / 1)) · (1 + (1 /
1)))) |
39 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / 1)) |
40 | 39 | oveq2d 7285 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / 1))) |
41 | 38, 40 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 +
((𝑀 + 1) /
1)))) |
42 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))) |
43 | | ovex 7302 |
. . . . . . . . 9
⊢ (((1 +
(𝑀 / 1)) · (1 + (1 /
1))) / (1 + ((𝑀 + 1) / 1)))
∈ V |
44 | 41, 42, 43 | fvmpt 6870 |
. . . . . . . 8
⊢ (1 ∈
ℕ → ((𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 +
((𝑀 + 1) /
1)))) |
45 | 33, 44 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 +
((𝑀 + 1) /
1))) |
46 | | nn0cn 12241 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
47 | 46 | div1d 11741 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (𝑀 / 1) = 𝑀) |
48 | 47 | oveq2d 7285 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (1 + (𝑀 / 1)) = (1 +
𝑀)) |
49 | | 1div1e1 11663 |
. . . . . . . . . . . 12
⊢ (1 / 1) =
1 |
50 | 49 | oveq2i 7280 |
. . . . . . . . . . 11
⊢ (1 + (1 /
1)) = (1 + 1) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (1 + (1 / 1)) = (1 + 1)) |
52 | 48, 51 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ ((1 + (𝑀 / 1))
· (1 + (1 / 1))) = ((1 + 𝑀) · (1 + 1))) |
53 | | nn0p1nn 12270 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
54 | 53 | nncnd 11987 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℂ) |
55 | 54 | div1d 11741 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ ((𝑀 + 1) / 1) =
(𝑀 + 1)) |
56 | 55 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (1 + ((𝑀 + 1) / 1))
= (1 + (𝑀 +
1))) |
57 | 52, 56 | oveq12d 7287 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (((1 + (𝑀 / 1))
· (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1)))) |
58 | | 1cnd 10969 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 1 ∈ ℂ) |
59 | 58, 46 | addcomd 11175 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (1 + 𝑀) = (𝑀 + 1)) |
60 | 59 | oveq1d 7284 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ ((1 + 𝑀) · (1
+ 1)) = ((𝑀 + 1) ·
(1 + 1))) |
61 | 60 | oveq1d 7284 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (((1 + 𝑀) ·
(1 + 1)) / (1 + (𝑀 + 1))) =
(((𝑀 + 1) · (1 + 1))
/ (1 + (𝑀 +
1)))) |
62 | | ax-1cn 10928 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
63 | 62, 62 | addcli 10980 |
. . . . . . . . . 10
⊢ (1 + 1)
∈ ℂ |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (1 + 1) ∈ ℂ) |
65 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 1 ∈ ℕ) |
66 | 65, 53 | nnaddcld 12023 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (1 + (𝑀 + 1)) ∈
ℕ) |
67 | 66 | nncnd 11987 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (1 + (𝑀 + 1)) ∈
ℂ) |
68 | 66 | nnne0d 12021 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (1 + (𝑀 + 1)) ≠
0) |
69 | 54, 64, 67, 68 | divassd 11784 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (((𝑀 + 1) ·
(1 + 1)) / (1 + (𝑀 + 1))) =
((𝑀 + 1) · ((1 + 1)
/ (1 + (𝑀 +
1))))) |
70 | 57, 61, 69 | 3eqtrd 2784 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (((1 + (𝑀 / 1))
· (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1))))) |
71 | 45, 70 | eqtrid 2792 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ ((𝑛 ∈ ℕ
↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1))))) |
72 | | seqp1 13732 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
73 | | nnuz 12618 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
74 | 72, 73 | eleq2s 2859 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
75 | 74 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
76 | 75 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
∧ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
77 | | oveq1 7276 |
. . . . . . . . . 10
⊢ ((seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
78 | 77 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
∧ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)))) |
79 | | peano2nn 11983 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
80 | | oveq2 7277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → (𝑀 / 𝑛) = (𝑀 / (𝑘 + 1))) |
81 | 80 | oveq2d 7285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / (𝑘 + 1)))) |
82 | | oveq2 7277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) |
83 | 82 | oveq2d 7285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → (1 + (1 / 𝑛)) = (1 + (1 / (𝑘 + 1)))) |
84 | 81, 83 | oveq12d 7287 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) |
85 | | oveq2 7277 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / (𝑘 + 1))) |
86 | 85 | oveq2d 7285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / (𝑘 + 1)))) |
87 | 84, 86 | oveq12d 7287 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) |
88 | | ovex 7302 |
. . . . . . . . . . . . . . 15
⊢ (((1 +
(𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ V |
89 | 87, 42, 88 | fvmpt 6870 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) |
90 | 79, 89 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) |
91 | 90 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) |
92 | 91 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑀 + 1) ·
((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) |
93 | 53 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 + 1) ∈
ℕ) |
94 | 93 | nncnd 11987 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 + 1) ∈
ℂ) |
95 | 79 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℕ) |
96 | 95 | nnrpd 12767 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℝ+) |
97 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑘 ∈
ℕ) |
98 | 97 | nnrpd 12767 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑘 ∈
ℝ+) |
99 | 93 | nnrpd 12767 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 + 1) ∈
ℝ+) |
100 | 98, 99 | rpaddcld 12784 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + (𝑀 + 1)) ∈
ℝ+) |
101 | 96, 100 | rpdivcld 12786 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈
ℝ+) |
102 | 101 | rpcnd 12771 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℂ) |
103 | | 1cnd 10969 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 1 ∈ ℂ) |
104 | | nn0re 12240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℝ) |
106 | 105, 95 | nndivred 12025 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 / (𝑘 + 1)) ∈
ℝ) |
107 | 106 | recnd 11002 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 / (𝑘 + 1)) ∈
ℂ) |
108 | 103, 107 | addcomd 11175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + (𝑀 / (𝑘 + 1))) = ((𝑀 / (𝑘 + 1)) + 1)) |
109 | | nn0ge0 12256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ 𝑀) |
110 | 109 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 0 ≤ 𝑀) |
111 | 105, 96, 110 | divge0d 12809 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 0 ≤ (𝑀 / (𝑘 + 1))) |
112 | 106, 111 | ge0p1rpd 12799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 / (𝑘 + 1)) + 1) ∈
ℝ+) |
113 | 108, 112 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + (𝑀 / (𝑘 + 1))) ∈
ℝ+) |
114 | | 1rp 12731 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 1 ∈ ℝ+) |
116 | 96 | rpreccld 12779 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 / (𝑘 + 1)) ∈
ℝ+) |
117 | 115, 116 | rpaddcld 12784 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + (1 / (𝑘 + 1)))
∈ ℝ+) |
118 | 113, 117 | rpmulcld 12785 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 /
(𝑘 + 1)))) ∈
ℝ+) |
119 | 99, 96 | rpdivcld 12786 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 + 1) / (𝑘 + 1)) ∈
ℝ+) |
120 | 115, 119 | rpaddcld 12784 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + ((𝑀 + 1) /
(𝑘 + 1))) ∈
ℝ+) |
121 | 118, 120 | rpdivcld 12786 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 /
(𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈
ℝ+) |
122 | 121 | rpcnd 12771 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 /
(𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℂ) |
123 | 94, 102, 122 | mulassd 10997 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑀 + 1) ·
((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = ((𝑀 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))) |
124 | 101, 118 | rpmulcld 12785 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈
ℝ+) |
125 | 124 | rpcnd 12771 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈
ℂ) |
126 | 120 | rpcnd 12771 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + ((𝑀 + 1) /
(𝑘 + 1))) ∈
ℂ) |
127 | 95 | nncnd 11987 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℂ) |
128 | 120 | rpne0d 12774 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + ((𝑀 + 1) /
(𝑘 + 1))) ≠
0) |
129 | 95 | nnne0d 12021 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 1) ≠
0) |
130 | 125, 126,
127, 128, 129 | divcan5d 11775 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
(((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) |
131 | 118 | rpcnd 12771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 /
(𝑘 + 1)))) ∈
ℂ) |
132 | 127, 102,
131 | mul12d 11182 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) ·
(((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))))) |
133 | 113 | rpcnd 12771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + (𝑀 / (𝑘 + 1))) ∈
ℂ) |
134 | 117 | rpcnd 12771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + (1 / (𝑘 + 1)))
∈ ℂ) |
135 | 127, 133,
134 | mulassd 10997 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
(1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 /
(𝑘 + 1)))) = ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) |
136 | 127, 103,
107 | adddid 10998 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
+ (𝑀 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1))))) |
137 | 127 | mulid1d 10991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · 1)
= (𝑘 + 1)) |
138 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℕ0) |
139 | 138 | nn0cnd 12293 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℂ) |
140 | 139, 127,
129 | divcan2d 11751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) ·
(𝑀 / (𝑘 + 1))) = 𝑀) |
141 | 137, 140 | oveq12d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
1) + ((𝑘 + 1) ·
(𝑀 / (𝑘 + 1)))) = ((𝑘 + 1) + 𝑀)) |
142 | 97 | nncnd 11987 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑘 ∈
ℂ) |
143 | 142, 103,
139 | addassd 10996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) + 𝑀) = (𝑘 + (1 + 𝑀))) |
144 | 103, 139 | addcomd 11175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 + 𝑀) = (𝑀 + 1)) |
145 | 144 | oveq2d 7285 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + (1 + 𝑀)) = (𝑘 + (𝑀 + 1))) |
146 | 143, 145 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) + 𝑀) = (𝑘 + (𝑀 + 1))) |
147 | 136, 141,
146 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
+ (𝑀 / (𝑘 + 1)))) = (𝑘 + (𝑀 + 1))) |
148 | 147 | oveq1d 7284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
(1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 /
(𝑘 + 1)))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) |
149 | 135, 148 | eqtr3d 2782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) ·
((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 /
(𝑘 + 1))))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) |
150 | 149 | oveq2d 7285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))) |
151 | 100 | rpcnd 12771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + (𝑀 + 1)) ∈
ℂ) |
152 | 102, 151,
134 | mulassd 10997 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))) |
153 | 100 | rpne0d 12774 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + (𝑀 + 1)) ≠ 0) |
154 | 127, 151,
153 | divcan1d 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) = (𝑘 + 1)) |
155 | 154 | oveq1d 7284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · (1 + (1 / (𝑘 + 1))))) |
156 | 116 | rpcnd 12771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (1 / (𝑘 + 1)) ∈
ℂ) |
157 | 127, 103,
156 | adddid 10998 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
+ (1 / (𝑘 + 1)))) =
(((𝑘 + 1) · 1) +
((𝑘 + 1) · (1 /
(𝑘 +
1))))) |
158 | 103, 127,
129 | divcan2d 11751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
/ (𝑘 + 1))) =
1) |
159 | 137, 158 | oveq12d 7287 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
1) + ((𝑘 + 1) · (1 /
(𝑘 + 1)))) = ((𝑘 + 1) + 1)) |
160 | 155, 157,
159 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1)) |
161 | 152, 160 | eqtr3d 2782 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + 1) + 1)) |
162 | 132, 150,
161 | 3eqtrd 2784 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) ·
(((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = ((𝑘 + 1) + 1)) |
163 | 119 | rpcnd 12771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 + 1) / (𝑘 + 1)) ∈
ℂ) |
164 | 127, 103,
163 | adddid 10998 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
+ ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1))))) |
165 | 94, 127, 129 | divcan2d 11751 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) ·
((𝑀 + 1) / (𝑘 + 1))) = (𝑀 + 1)) |
166 | 137, 165 | oveq12d 7287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
1) + ((𝑘 + 1) ·
((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1))) |
167 | 164, 166 | eqtrd 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑘 + 1) · (1
+ ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1))) |
168 | 162, 167 | oveq12d 7287 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) ·
(((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))) |
169 | 102, 131,
126, 128 | divassd 11784 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) |
170 | 130, 168,
169 | 3eqtr3rd 2789 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))) |
171 | 170 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 + 1) ·
(((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))) |
172 | 92, 123, 171 | 3eqtrd 2784 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((𝑀 + 1) ·
((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))) |
173 | 172 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
∧ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))) |
174 | 76, 78, 173 | 3eqtrd 2784 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
∧ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))) |
175 | 174 | exp31 420 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑀 ∈ ℕ0
→ ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))))) |
176 | 175 | a2d 29 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑀 ∈ ℕ0
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (𝑀 ∈ ℕ0 → (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))))) |
177 | 11, 18, 25, 32, 71, 176 | nnind 11989 |
. . . . 5
⊢ (𝑏 ∈ ℕ → (𝑀 ∈ ℕ0
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))) |
178 | 177 | impcom 408 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))) |
179 | | oveq1 7276 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥 + 1) = (𝑏 + 1)) |
180 | | oveq1 7276 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1))) |
181 | 179, 180 | oveq12d 7287 |
. . . . . . 7
⊢ (𝑥 = 𝑏 → ((𝑥 + 1) / (𝑥 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) |
182 | 181 | oveq2d 7285 |
. . . . . 6
⊢ (𝑥 = 𝑏 → ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))) |
183 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) |
184 | | ovex 7302 |
. . . . . 6
⊢ ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) ∈ V |
185 | 182, 183,
184 | fvmpt 6870 |
. . . . 5
⊢ (𝑏 ∈ ℕ → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))) |
186 | 185 | adantl 482 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ ((𝑥 ∈ ℕ
↦ ((𝑀 + 1) ·
((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))) |
187 | 178, 186 | eqtr4d 2783 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏)) |
188 | 187 | ralrimiva 3110 |
. 2
⊢ (𝑀 ∈ ℕ0
→ ∀𝑏 ∈
ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏)) |
189 | | seqfn 13729 |
. . . . 5
⊢ (1 ∈
ℤ → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn
(ℤ≥‘1)) |
190 | 2, 189 | ax-mp 5 |
. . . 4
⊢ seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn
(ℤ≥‘1) |
191 | 73 | fneq2i 6528 |
. . . 4
⊢ (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ↔ seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn
(ℤ≥‘1)) |
192 | 190, 191 | mpbir 230 |
. . 3
⊢ seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ |
193 | | ovex 7302 |
. . . 4
⊢ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) ∈ V |
194 | 193, 183 | fnmpti 6573 |
. . 3
⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ |
195 | | eqfnfv 6904 |
. . 3
⊢ ((seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ∧ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ) → (seq1( ·
, (𝑛 ∈ ℕ ↦
(((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))) |
196 | 192, 194,
195 | mp2an 689 |
. 2
⊢ (seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (𝑀 /
𝑛)) · (1 + (1 /
𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏)) |
197 | 188, 196 | sylibr 233 |
1
⊢ (𝑀 ∈ ℕ0
→ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))) |