Metamath Proof Explorer

Theorem faclimlem1

Description: Lemma for faclim . Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion faclimlem1 ( 𝑀 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑎 = 1 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 1 ) )
2 1z ⊢ 1 ∈ ℤ
3 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 1 ) = ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) )
4 2 3 ax-mp ⊢ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 1 ) = ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 )
5 1 4 eqtrdi ⊢ ( 𝑎 = 1 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) )
6 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 + 1 ) = ( 1 + 1 ) )
7 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 + ( 𝑀 + 1 ) ) = ( 1 + ( 𝑀 + 1 ) ) )
8 6 7 oveq12d ⊢ ( 𝑎 = 1 → ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) = ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) )
9 8 oveq2d ⊢ ( 𝑎 = 1 → ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) )
10 5 9 eqeq12d ⊢ ( 𝑎 = 1 → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) ) )
11 10 imbi2d ⊢ ( 𝑎 = 1 → ( ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) ) ) )
12 fveq2 ⊢ ( 𝑎 = 𝑘 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) )
13 oveq1 ⊢ ( 𝑎 = 𝑘 → ( 𝑎 + 1 ) = ( 𝑘 + 1 ) )
14 oveq1 ⊢ ( 𝑎 = 𝑘 → ( 𝑎 + ( 𝑀 + 1 ) ) = ( 𝑘 + ( 𝑀 + 1 ) ) )
15 13 14 oveq12d ⊢ ( 𝑎 = 𝑘 → ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) )
16 15 oveq2d ⊢ ( 𝑎 = 𝑘 → ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) )
17 12 16 eqeq12d ⊢ ( 𝑎 = 𝑘 → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ↔ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) )
18 17 imbi2d ⊢ ( 𝑎 = 𝑘 → ( ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) ) )
19 fveq2 ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) )
20 oveq1 ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( 𝑎 + 1 ) = ( ( 𝑘 + 1 ) + 1 ) )
21 oveq1 ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( 𝑎 + ( 𝑀 + 1 ) ) = ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) )
22 20 21 oveq12d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) = ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) )
23 22 oveq2d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) )
24 19 23 eqeq12d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ↔ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) ) )
25 24 imbi2d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) ) ) )
26 fveq2 ⊢ ( 𝑎 = 𝑏 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) )
27 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 + 1 ) = ( 𝑏 + 1 ) )
28 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 + ( 𝑀 + 1 ) ) = ( 𝑏 + ( 𝑀 + 1 ) ) )
29 27 28 oveq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) = ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) )
30 29 oveq2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) )
31 26 30 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ↔ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) ) )
32 31 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( 𝑀 + 1 ) · ( ( 𝑎 + 1 ) / ( 𝑎 + ( 𝑀 + 1 ) ) ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) ) ) )
33 1nn ⊢ 1 ∈ ℕ
34 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑀 / 𝑛 ) = ( 𝑀 / 1 ) )
35 34 oveq2d ⊢ ( 𝑛 = 1 → ( 1 + ( 𝑀 / 𝑛 ) ) = ( 1 + ( 𝑀 / 1 ) ) )
36 oveq2 ⊢ ( 𝑛 = 1 → ( 1 / 𝑛 ) = ( 1 / 1 ) )
37 36 oveq2d ⊢ ( 𝑛 = 1 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 1 ) ) )
38 35 37 oveq12d ⊢ ( 𝑛 = 1 → ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) = ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) )
39 oveq2 ⊢ ( 𝑛 = 1 → ( ( 𝑀 + 1 ) / 𝑛 ) = ( ( 𝑀 + 1 ) / 1 ) )
40 39 oveq2d ⊢ ( 𝑛 = 1 → ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) = ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) )
41 38 40 oveq12d ⊢ ( 𝑛 = 1 → ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) ) )
42 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) )
43 ovex ⊢ ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) ) ∈ V
44 41 42 43 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) = ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) ) )
45 33 44 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) = ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) )
46 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
47 46 div1d ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 / 1 ) = 𝑀 )
48 47 oveq2d ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( 𝑀 / 1 ) ) = ( 1 + 𝑀 ) )
49 1div1e1 ⊢ ( 1 / 1 ) = 1
50 49 oveq2i ⊢ ( 1 + ( 1 / 1 ) ) = ( 1 + 1 )
51 50 a1i ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( 1 / 1 ) ) = ( 1 + 1 ) )
52 48 51 oveq12d ⊢ ( 𝑀 ∈ ℕ0 → ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) = ( ( 1 + 𝑀 ) · ( 1 + 1 ) ) )
53 nn0p1nn ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
54 53 nncnd ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℂ )
55 54 div1d ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑀 + 1 ) / 1 ) = ( 𝑀 + 1 ) )
56 55 oveq2d ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) = ( 1 + ( 𝑀 + 1 ) ) )
57 52 56 oveq12d ⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) ) = ( ( ( 1 + 𝑀 ) · ( 1 + 1 ) ) / ( 1 + ( 𝑀 + 1 ) ) ) )
58 1cnd ⊢ ( 𝑀 ∈ ℕ0 → 1 ∈ ℂ )
59 58 46 addcomd ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + 𝑀 ) = ( 𝑀 + 1 ) )
60 59 oveq1d ⊢ ( 𝑀 ∈ ℕ0 → ( ( 1 + 𝑀 ) · ( 1 + 1 ) ) = ( ( 𝑀 + 1 ) · ( 1 + 1 ) ) )
61 60 oveq1d ⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 1 + 𝑀 ) · ( 1 + 1 ) ) / ( 1 + ( 𝑀 + 1 ) ) ) = ( ( ( 𝑀 + 1 ) · ( 1 + 1 ) ) / ( 1 + ( 𝑀 + 1 ) ) ) )
62 ax-1cn ⊢ 1 ∈ ℂ
63 62 62 addcli ⊢ ( 1 + 1 ) ∈ ℂ
64 63 a1i ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + 1 ) ∈ ℂ )
65 33 a1i ⊢ ( 𝑀 ∈ ℕ0 → 1 ∈ ℕ )
66 65 53 nnaddcld ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( 𝑀 + 1 ) ) ∈ ℕ )
67 66 nncnd ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( 𝑀 + 1 ) ) ∈ ℂ )
68 66 nnne0d ⊢ ( 𝑀 ∈ ℕ0 → ( 1 + ( 𝑀 + 1 ) ) ≠ 0 )
69 54 64 67 68 divassd ⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 𝑀 + 1 ) · ( 1 + 1 ) ) / ( 1 + ( 𝑀 + 1 ) ) ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) )
70 57 61 69 3eqtrd ⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 1 + ( 𝑀 / 1 ) ) · ( 1 + ( 1 / 1 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 1 ) ) ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) )
71 45 70 eqtrid ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ 1 ) = ( ( 𝑀 + 1 ) · ( ( 1 + 1 ) / ( 1 + ( 𝑀 + 1 ) ) ) ) )
72 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
73 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
74 72 73 eleq2s ⊢ ( 𝑘 ∈ ℕ → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
75 74 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
76 75 adantr ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) ∧ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
77 oveq1 ⊢ ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
78 77 adantl ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) ∧ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
79 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
80 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑀 / 𝑛 ) = ( 𝑀 / ( 𝑘 + 1 ) ) )
81 80 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 + ( 𝑀 / 𝑛 ) ) = ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) )
82 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( 𝑘 + 1 ) ) )
83 82 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) )
84 81 83 oveq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) = ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) )
85 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑀 + 1 ) / 𝑛 ) = ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) )
86 85 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) = ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) )
87 84 86 oveq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) )
88 ovex ⊢ ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ∈ V
89 87 42 88 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) )
90 79 89 syl ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) )
91 90 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ) )
92 91 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ) )
93 53 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℕ )
94 93 nncnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℂ )
95 79 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ )
96 95 nnrpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℝ+ )
97 simpl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑘 ∈ ℕ )
98 97 nnrpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑘 ∈ ℝ+ )
99 93 nnrpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℝ+ )
100 98 99 rpaddcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + ( 𝑀 + 1 ) ) ∈ ℝ+ )
101 96 100 rpdivcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ∈ ℝ+ )
102 101 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ∈ ℂ )
103 1cnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 1 ∈ ℂ )
104 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
105 104 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
106 105 95 nndivred ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 / ( 𝑘 + 1 ) ) ∈ ℝ )
107 106 recnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 / ( 𝑘 + 1 ) ) ∈ ℂ )
108 103 107 addcomd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) = ( ( 𝑀 / ( 𝑘 + 1 ) ) + 1 ) )
109 nn0ge0 ⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
110 109 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ 𝑀 )
111 105 96 110 divge0d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ ( 𝑀 / ( 𝑘 + 1 ) ) )
112 106 111 ge0p1rpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 / ( 𝑘 + 1 ) ) + 1 ) ∈ ℝ+ )
113 108 112 eqeltrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ∈ ℝ+ )
114 1rp ⊢ 1 ∈ ℝ+
115 114 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 1 ∈ ℝ+ )
116 96 rpreccld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ+ )
117 115 116 rpaddcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ∈ ℝ+ )
118 113 117 rpmulcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ∈ ℝ+ )
119 99 96 rpdivcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ∈ ℝ+ )
120 115 119 rpaddcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ∈ ℝ+ )
121 118 120 rpdivcld ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ∈ ℝ+ )
122 121 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
123 94 102 122 mulassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ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 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ∈ ℝ+ )
125 124 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ∈ ℂ )
126 120 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ∈ ℂ )
127 95 nncnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℂ )
128 120 rpne0d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ≠ 0 )
129 95 nnne0d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 1 ) ≠ 0 )
130 125 126 127 128 129 divcan5d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ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 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
132 127 102 131 mul12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ) = ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 𝑘 + 1 ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ) )
133 113 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ∈ ℂ )
134 117 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ∈ ℂ )
135 127 133 134 mulassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) )
136 127 103 107 adddid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( 𝑀 / ( 𝑘 + 1 ) ) ) ) )
137 127 mulid1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · 1 ) = ( 𝑘 + 1 ) )
138 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
139 138 nn0cnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
140 139 127 129 divcan2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 𝑀 / ( 𝑘 + 1 ) ) ) = 𝑀 )
141 137 140 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( 𝑀 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) + 𝑀 ) )
142 97 nncnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
143 142 103 139 addassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) + 𝑀 ) = ( 𝑘 + ( 1 + 𝑀 ) ) )
144 103 139 addcomd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 + 𝑀 ) = ( 𝑀 + 1 ) )
145 144 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + ( 1 + 𝑀 ) ) = ( 𝑘 + ( 𝑀 + 1 ) ) )
146 143 145 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) + 𝑀 ) = ( 𝑘 + ( 𝑀 + 1 ) ) )
147 136 141 146 3eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ) = ( 𝑘 + ( 𝑀 + 1 ) ) )
148 147 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + ( 𝑀 + 1 ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) )
149 135 148 eqtr3d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) = ( ( 𝑘 + ( 𝑀 + 1 ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) )
150 149 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 𝑘 + 1 ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ) = ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 𝑘 + ( 𝑀 + 1 ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) )
151 100 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + ( 𝑀 + 1 ) ) ∈ ℂ )
152 102 151 134 mulassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 𝑘 + ( 𝑀 + 1 ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) )
153 100 rpne0d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + ( 𝑀 + 1 ) ) ≠ 0 )
154 127 151 153 divcan1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 𝑘 + ( 𝑀 + 1 ) ) ) = ( 𝑘 + 1 ) )
155 154 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) )
156 116 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℂ )
157 127 103 156 adddid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( 1 / ( 𝑘 + 1 ) ) ) ) )
158 103 127 129 divcan2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 / ( 𝑘 + 1 ) ) ) = 1 )
159 137 158 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) + 1 ) )
160 155 157 159 3eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) + 1 ) )
161 152 160 eqtr3d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 𝑘 + ( 𝑀 + 1 ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) = ( ( 𝑘 + 1 ) + 1 ) )
162 132 150 161 3eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) + 1 ) )
163 119 rpcnd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ∈ ℂ )
164 127 103 163 adddid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) )
165 94 127 129 divcan2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑀 + 1 ) )
166 137 165 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · 1 ) + ( ( 𝑘 + 1 ) · ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) )
167 164 166 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) )
168 162 167 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) ) ) / ( ( 𝑘 + 1 ) · ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ) = ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) )
169 102 131 126 128 divassd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ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 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ) = ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) )
171 170 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) · ( ( ( 1 + ( 𝑀 / ( 𝑘 + 1 ) ) ) · ( 1 + ( 1 / ( 𝑘 + 1 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) )
172 92 123 171 3eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) )
173 172 adantr ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) ∧ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 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 ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) ∧ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) )
175 174 exp31 ⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ∈ ℕ0 → ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) ) ) )
176 175 a2d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ) → ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑀 + 1 ) · ( ( ( 𝑘 + 1 ) + 1 ) / ( ( 𝑘 + 1 ) + ( 𝑀 + 1 ) ) ) ) ) ) )
177 11 18 25 32 71 176 nnind ⊢ ( 𝑏 ∈ ℕ → ( 𝑀 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) ) )
178 177 impcom ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) )
179 oveq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 + 1 ) = ( 𝑏 + 1 ) )
180 oveq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 + ( 𝑀 + 1 ) ) = ( 𝑏 + ( 𝑀 + 1 ) ) )
181 179 180 oveq12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) = ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) )
182 181 oveq2d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) )
183 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) )
184 ovex ⊢ ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) ∈ V
185 182 183 184 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) )
186 185 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑀 + 1 ) · ( ( 𝑏 + 1 ) / ( 𝑏 + ( 𝑀 + 1 ) ) ) ) )
187 178 186 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) )
188 187 ralrimiva ⊢ ( 𝑀 ∈ ℕ0 → ∀ 𝑏 ∈ ℕ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) )
189 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) )
190 2 189 ax-mp ⊢ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 )
191 73 fneq2i ⊢ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ℕ ↔ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) )
192 190 191 mpbir ⊢ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ℕ
193 ovex ⊢ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ∈ V
194 193 183 fnmpti ⊢ ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) Fn ℕ
195 eqfnfv ⊢ ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) Fn ℕ ∧ ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) Fn ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ↔ ∀ 𝑏 ∈ ℕ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) ) )
196 192 194 195 mp2an ⊢ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ↔ ∀ 𝑏 ∈ ℕ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑏 ) )
197 188 196 sylibr ⊢ ( 𝑀 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑥 + 1 ) / ( 𝑥 + ( 𝑀 + 1 ) ) ) ) ) )