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
|- ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) = ( x e. NN |-> ( ( M + 1 ) x. ( ( x + 1 ) / ( x + ( M + 1 ) ) ) ) ) )

Proof

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