Metamath Proof Explorer

Theorem faclimlem2

Description: Lemma for faclim . Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion faclimlem2 
|- ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) ~~> ( M + 1 ) )

Proof

Step Hyp Ref Expression
1 faclimlem1 
 |-  ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) = ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( M e. NN0 -> 1 e. ZZ )
4 1cnd 
 |-  ( M e. NN0 -> 1 e. CC )
5 nn0p1nn 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN )
6 5 nnzd 
 |-  ( M e. NN0 -> ( M + 1 ) e. ZZ )
7 nnex 
 |-  NN e. _V
8 7 mptex 
 |-  ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) e. _V
9 8 a1i 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) e. _V )
10 oveq1 
 |-  ( m = k -> ( m + 1 ) = ( k + 1 ) )
11 oveq1 
 |-  ( m = k -> ( m + ( M + 1 ) ) = ( k + ( M + 1 ) ) )
12 10 11 oveq12d 
 |-  ( m = k -> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) = ( ( k + 1 ) / ( k + ( M + 1 ) ) ) )
13 eqid 
 |-  ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) = ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) )
14 ovex 
 |-  ( ( k + 1 ) / ( k + ( M + 1 ) ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( k e. NN -> ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) = ( ( k + 1 ) / ( k + ( M + 1 ) ) ) )
16 15 adantl 
 |-  ( ( M e. NN0 /\ k e. NN ) -> ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) = ( ( k + 1 ) / ( k + ( M + 1 ) ) ) )
17 2 3 4 6 9 16 divcnvlin 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ~~> 1 )
18 5 nncnd 
 |-  ( M e. NN0 -> ( M + 1 ) e. CC )
19 7 mptex 
 |-  ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) e. _V
20 19 a1i 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) e. _V )
21 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
22 21 adantl 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( m + 1 ) e. NN )
23 22 nnred 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( m + 1 ) e. RR )
24 simpr 
 |-  ( ( M e. NN0 /\ m e. NN ) -> m e. NN )
25 5 adantr 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( M + 1 ) e. NN )
26 24 25 nnaddcld 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( m + ( M + 1 ) ) e. NN )
27 23 26 nndivred 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) e. RR )
28 27 recnd 
 |-  ( ( M e. NN0 /\ m e. NN ) -> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) e. CC )
29 28 fmpttd 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) : NN --> CC )
30 29 ffvelcdmda 
 |-  ( ( M e. NN0 /\ k e. NN ) -> ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) e. CC )
31 12 oveq2d 
 |-  ( m = k -> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) = ( ( M + 1 ) x. ( ( k + 1 ) / ( k + ( M + 1 ) ) ) ) )
32 eqid 
 |-  ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) = ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) )
33 ovex 
 |-  ( ( M + 1 ) x. ( ( k + 1 ) / ( k + ( M + 1 ) ) ) ) e. _V
34 31 32 33 fvmpt 
 |-  ( k e. NN -> ( ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) ` k ) = ( ( M + 1 ) x. ( ( k + 1 ) / ( k + ( M + 1 ) ) ) ) )
35 15 oveq2d 
 |-  ( k e. NN -> ( ( M + 1 ) x. ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) ) = ( ( M + 1 ) x. ( ( k + 1 ) / ( k + ( M + 1 ) ) ) ) )
36 34 35 eqtr4d 
 |-  ( k e. NN -> ( ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) ` k ) = ( ( M + 1 ) x. ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) ) )
37 36 adantl 
 |-  ( ( M e. NN0 /\ k e. NN ) -> ( ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) ` k ) = ( ( M + 1 ) x. ( ( m e. NN |-> ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ` k ) ) )
38 2 3 17 18 20 30 37 climmulc2 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) ~~> ( ( M + 1 ) x. 1 ) )
39 18 mulridd 
 |-  ( M e. NN0 -> ( ( M + 1 ) x. 1 ) = ( M + 1 ) )
40 38 39 breqtrd 
 |-  ( M e. NN0 -> ( m e. NN |-> ( ( M + 1 ) x. ( ( m + 1 ) / ( m + ( M + 1 ) ) ) ) ) ~~> ( M + 1 ) )
41 1 40 eqbrtrd 
 |-  ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) ~~> ( M + 1 ) )