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 eqtrid 
 |-  ( 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 mulridd 
 |-  ( ( 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 ) ) ) ) ) )