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 syl5eq ( 𝑀 ∈ ℕ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 ) ) ) ) ) )