Metamath Proof Explorer

Theorem faclim

Description: An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017)

Ref Expression
Hypothesis faclim.1 
|- F = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) )
Assertion faclim 
|- ( A e. NN0 -> seq 1 ( x. , F ) ~~> ( ! ` A ) )

Proof

Step Hyp Ref Expression
1 faclim.1 
 |-  F = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) )
2 seqeq3 
 |-  ( F = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) -> seq 1 ( x. , F ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) ) )
3 1 2 ax-mp 
 |-  seq 1 ( x. , F ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) )
4 oveq2 
 |-  ( a = 0 -> ( ( 1 + ( 1 / n ) ) ^ a ) = ( ( 1 + ( 1 / n ) ) ^ 0 ) )
5 oveq1 
 |-  ( a = 0 -> ( a / n ) = ( 0 / n ) )
6 5 oveq2d 
 |-  ( a = 0 -> ( 1 + ( a / n ) ) = ( 1 + ( 0 / n ) ) )
7 4 6 oveq12d 
 |-  ( a = 0 -> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) = ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) )
8 7 mpteq2dv 
 |-  ( a = 0 -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) )
9 8 seqeq3d 
 |-  ( a = 0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) ) )
10 fveq2 
 |-  ( a = 0 -> ( ! ` a ) = ( ! ` 0 ) )
11 fac0 
 |-  ( ! ` 0 ) = 1
12 10 11 eqtrdi 
 |-  ( a = 0 -> ( ! ` a ) = 1 )
13 9 12 breq12d 
 |-  ( a = 0 -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) ~~> ( ! ` a ) <-> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) ) ~~> 1 ) )
14 oveq2 
 |-  ( a = m -> ( ( 1 + ( 1 / n ) ) ^ a ) = ( ( 1 + ( 1 / n ) ) ^ m ) )
15 oveq1 
 |-  ( a = m -> ( a / n ) = ( m / n ) )
16 15 oveq2d 
 |-  ( a = m -> ( 1 + ( a / n ) ) = ( 1 + ( m / n ) ) )
17 14 16 oveq12d 
 |-  ( a = m -> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) = ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) )
18 17 mpteq2dv 
 |-  ( a = m -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) )
19 18 seqeq3d 
 |-  ( a = m -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) )
20 fveq2 
 |-  ( a = m -> ( ! ` a ) = ( ! ` m ) )
21 19 20 breq12d 
 |-  ( a = m -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) ~~> ( ! ` a ) <-> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) )
22 oveq2 
 |-  ( a = ( m + 1 ) -> ( ( 1 + ( 1 / n ) ) ^ a ) = ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) )
23 oveq1 
 |-  ( a = ( m + 1 ) -> ( a / n ) = ( ( m + 1 ) / n ) )
24 23 oveq2d 
 |-  ( a = ( m + 1 ) -> ( 1 + ( a / n ) ) = ( 1 + ( ( m + 1 ) / n ) ) )
25 22 24 oveq12d 
 |-  ( a = ( m + 1 ) -> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) = ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) )
26 25 mpteq2dv 
 |-  ( a = ( m + 1 ) -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) )
27 26 seqeq3d 
 |-  ( a = ( m + 1 ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) )
28 fveq2 
 |-  ( a = ( m + 1 ) -> ( ! ` a ) = ( ! ` ( m + 1 ) ) )
29 27 28 breq12d 
 |-  ( a = ( m + 1 ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) ~~> ( ! ` a ) <-> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( ! ` ( m + 1 ) ) ) )
30 oveq2 
 |-  ( a = A -> ( ( 1 + ( 1 / n ) ) ^ a ) = ( ( 1 + ( 1 / n ) ) ^ A ) )
31 oveq1 
 |-  ( a = A -> ( a / n ) = ( A / n ) )
32 31 oveq2d 
 |-  ( a = A -> ( 1 + ( a / n ) ) = ( 1 + ( A / n ) ) )
33 30 32 oveq12d 
 |-  ( a = A -> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) = ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) )
34 33 mpteq2dv 
 |-  ( a = A -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) )
35 34 seqeq3d 
 |-  ( a = A -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) = seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) ) )
36 fveq2 
 |-  ( a = A -> ( ! ` a ) = ( ! ` A ) )
37 35 36 breq12d 
 |-  ( a = A -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ a ) / ( 1 + ( a / n ) ) ) ) ) ~~> ( ! ` a ) <-> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) ) ~~> ( ! ` A ) ) )
38 1red 
 |-  ( n e. NN -> 1 e. RR )
39 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
40 38 39 readdcld 
 |-  ( n e. NN -> ( 1 + ( 1 / n ) ) e. RR )
41 40 recnd 
 |-  ( n e. NN -> ( 1 + ( 1 / n ) ) e. CC )
42 41 exp0d 
 |-  ( n e. NN -> ( ( 1 + ( 1 / n ) ) ^ 0 ) = 1 )
43 nncn 
 |-  ( n e. NN -> n e. CC )
44 nnne0 
 |-  ( n e. NN -> n =/= 0 )
45 43 44 div0d 
 |-  ( n e. NN -> ( 0 / n ) = 0 )
46 45 oveq2d 
 |-  ( n e. NN -> ( 1 + ( 0 / n ) ) = ( 1 + 0 ) )
47 1p0e1 
 |-  ( 1 + 0 ) = 1
48 46 47 eqtrdi 
 |-  ( n e. NN -> ( 1 + ( 0 / n ) ) = 1 )
49 42 48 oveq12d 
 |-  ( n e. NN -> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) = ( 1 / 1 ) )
50 1div1e1 
 |-  ( 1 / 1 ) = 1
51 49 50 eqtrdi 
 |-  ( n e. NN -> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) = 1 )
52 51 mpteq2ia 
 |-  ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) = ( n e. NN |-> 1 )
53 fconstmpt 
 |-  ( NN X. { 1 } ) = ( n e. NN |-> 1 )
54 52 53 eqtr4i 
 |-  ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) = ( NN X. { 1 } )
55 seqeq3 
 |-  ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) = ( NN X. { 1 } ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) ) = seq 1 ( x. , ( NN X. { 1 } ) ) )
56 54 55 ax-mp 
 |-  seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) ) = seq 1 ( x. , ( NN X. { 1 } ) )
57 nnuz 
 |-  NN = ( ZZ>= ` 1 )
58 1zzd 
 |-  ( T. -> 1 e. ZZ )
59 57 58 climprod1 
 |-  ( T. -> seq 1 ( x. , ( NN X. { 1 } ) ) ~~> 1 )
60 59 mptru 
 |-  seq 1 ( x. , ( NN X. { 1 } ) ) ~~> 1
61 56 60 eqbrtri 
 |-  seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ 0 ) / ( 1 + ( 0 / n ) ) ) ) ) ~~> 1
62 1zzd 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> 1 e. ZZ )
63 simpr 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) )
64 seqex 
 |-  seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) e. _V
65 64 a1i 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) e. _V )
66 faclimlem2 
 |-  ( m e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( m + 1 ) )
67 66 adantr 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( m + 1 ) )
68 elnnuz 
 |-  ( a e. NN <-> a e. ( ZZ>= ` 1 ) )
69 68 biimpi 
 |-  ( a e. NN -> a e. ( ZZ>= ` 1 ) )
70 69 adantl 
 |-  ( ( m e. NN0 /\ a e. NN ) -> a e. ( ZZ>= ` 1 ) )
71 1rp 
 |-  1 e. RR+
72 71 a1i 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 1 e. RR+ )
73 nnrp 
 |-  ( n e. NN -> n e. RR+ )
74 73 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
75 74 adantl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 / n ) e. RR+ )
76 72 75 rpaddcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( 1 / n ) ) e. RR+ )
77 nn0z 
 |-  ( m e. NN0 -> m e. ZZ )
78 77 adantr 
 |-  ( ( m e. NN0 /\ n e. NN ) -> m e. ZZ )
79 76 78 rpexpcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( 1 + ( 1 / n ) ) ^ m ) e. RR+ )
80 1cnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 1 e. CC )
81 nn0nndivcl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( m / n ) e. RR )
82 81 recnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( m / n ) e. CC )
83 80 82 addcomd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( m / n ) ) = ( ( m / n ) + 1 ) )
84 nn0ge0div 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 0 <_ ( m / n ) )
85 81 84 ge0p1rpd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( m / n ) + 1 ) e. RR+ )
86 83 85 eqeltrd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( m / n ) ) e. RR+ )
87 79 86 rpdivcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) e. RR+ )
88 87 rpcnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) e. CC )
89 88 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) : NN --> CC )
90 elfznn 
 |-  ( b e. ( 1 ... a ) -> b e. NN )
91 ffvelrn 
 |-  ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) : NN --> CC /\ b e. NN ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) e. CC )
92 89 90 91 syl2an 
 |-  ( ( m e. NN0 /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) e. CC )
93 92 adantlr 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) e. CC )
94 mulcl 
 |-  ( ( b e. CC /\ x e. CC ) -> ( b x. x ) e. CC )
95 94 adantl 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ ( b e. CC /\ x e. CC ) ) -> ( b x. x ) e. CC )
96 70 93 95 seqcl 
 |-  ( ( m e. NN0 /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ` a ) e. CC )
97 96 adantlr 
 |-  ( ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ` a ) e. CC )
98 86 76 rpmulcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) e. RR+ )
99 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
100 99 nnrpd 
 |-  ( m e. NN0 -> ( m + 1 ) e. RR+ )
101 rpdivcl 
 |-  ( ( ( m + 1 ) e. RR+ /\ n e. RR+ ) -> ( ( m + 1 ) / n ) e. RR+ )
102 100 73 101 syl2an 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( m + 1 ) / n ) e. RR+ )
103 72 102 rpaddcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( ( m + 1 ) / n ) ) e. RR+ )
104 98 103 rpdivcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) e. RR+ )
105 104 rpcnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) e. CC )
106 105 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) : NN --> CC )
107 ffvelrn 
 |-  ( ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) : NN --> CC /\ b e. NN ) -> ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) e. CC )
108 106 90 107 syl2an 
 |-  ( ( m e. NN0 /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) e. CC )
109 108 adantlr 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) e. CC )
110 70 109 95 seqcl 
 |-  ( ( m e. NN0 /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) e. CC )
111 110 adantlr 
 |-  ( ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) e. CC )
112 faclimlem3 
 |-  ( ( m e. NN0 /\ b e. NN ) -> ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) = ( ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) x. ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) ) )
113 oveq2 
 |-  ( n = b -> ( 1 / n ) = ( 1 / b ) )
114 113 oveq2d 
 |-  ( n = b -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / b ) ) )
115 114 oveq1d 
 |-  ( n = b -> ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) = ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) )
116 oveq2 
 |-  ( n = b -> ( ( m + 1 ) / n ) = ( ( m + 1 ) / b ) )
117 116 oveq2d 
 |-  ( n = b -> ( 1 + ( ( m + 1 ) / n ) ) = ( 1 + ( ( m + 1 ) / b ) ) )
118 115 117 oveq12d 
 |-  ( n = b -> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) = ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
119 eqid 
 |-  ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) )
120 ovex 
 |-  ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) e. _V
121 118 119 120 fvmpt 
 |-  ( b e. NN -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
122 121 adantl 
 |-  ( ( m e. NN0 /\ b e. NN ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
123 114 oveq1d 
 |-  ( n = b -> ( ( 1 + ( 1 / n ) ) ^ m ) = ( ( 1 + ( 1 / b ) ) ^ m ) )
124 oveq2 
 |-  ( n = b -> ( m / n ) = ( m / b ) )
125 124 oveq2d 
 |-  ( n = b -> ( 1 + ( m / n ) ) = ( 1 + ( m / b ) ) )
126 123 125 oveq12d 
 |-  ( n = b -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) = ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) )
127 eqid 
 |-  ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) )
128 ovex 
 |-  ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) e. _V
129 126 127 128 fvmpt 
 |-  ( b e. NN -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) = ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) )
130 125 114 oveq12d 
 |-  ( n = b -> ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) = ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) )
131 130 117 oveq12d 
 |-  ( n = b -> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) = ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
132 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 ) ) ) )
133 ovex 
 |-  ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) e. _V
134 131 132 133 fvmpt 
 |-  ( b e. NN -> ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
135 129 134 oveq12d 
 |-  ( b e. NN -> ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) x. ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) ) = ( ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) x. ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) ) )
136 135 adantl 
 |-  ( ( m e. NN0 /\ b e. NN ) -> ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) x. ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) ) = ( ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) x. ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) ) )
137 112 122 136 3eqtr4d 
 |-  ( ( m e. NN0 /\ b e. NN ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) x. ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) ) )
138 90 137 sylan2 
 |-  ( ( m e. NN0 /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) x. ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) ) )
139 138 adantlr 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) = ( ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) x. ( ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ` b ) ) )
140 70 93 109 139 prodfmul 
 |-  ( ( m e. NN0 /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) = ( ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ` a ) x. ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) ) )
141 140 adantlr 
 |-  ( ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) = ( ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ` a ) x. ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ` a ) ) )
142 57 62 63 65 67 97 111 141 climmul 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( ( ! ` m ) x. ( m + 1 ) ) )
143 facp1 
 |-  ( m e. NN0 -> ( ! ` ( m + 1 ) ) = ( ( ! ` m ) x. ( m + 1 ) ) )
144 143 adantr 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> ( ! ` ( m + 1 ) ) = ( ( ! ` m ) x. ( m + 1 ) ) )
145 142 144 breqtrrd 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( ! ` ( m + 1 ) ) )
146 145 ex 
 |-  ( m e. NN0 -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) ) ~~> ( ! ` ( m + 1 ) ) ) )
147 13 21 29 37 61 146 nn0ind 
 |-  ( A e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) ) ~~> ( ! ` A ) )
148 3 147 eqbrtrid 
 |-  ( A e. NN0 -> seq 1 ( x. , F ) ~~> ( ! ` A ) )