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 bilani 
 |-  ( ( m e. NN0 /\ a e. NN ) -> a e. ( ZZ>= ` 1 ) )
70 1rp 
 |-  1 e. RR+
71 70 a1i 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 1 e. RR+ )
72 nnrp 
 |-  ( n e. NN -> n e. RR+ )
73 72 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
74 73 adantl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 / n ) e. RR+ )
75 71 74 rpaddcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( 1 / n ) ) e. RR+ )
76 nn0z 
 |-  ( m e. NN0 -> m e. ZZ )
77 76 adantr 
 |-  ( ( m e. NN0 /\ n e. NN ) -> m e. ZZ )
78 75 77 rpexpcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( 1 + ( 1 / n ) ) ^ m ) e. RR+ )
79 1cnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 1 e. CC )
80 nn0nndivcl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( m / n ) e. RR )
81 80 recnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( m / n ) e. CC )
82 79 81 addcomd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( m / n ) ) = ( ( m / n ) + 1 ) )
83 nn0ge0div 
 |-  ( ( m e. NN0 /\ n e. NN ) -> 0 <_ ( m / n ) )
84 80 83 ge0p1rpd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( m / n ) + 1 ) e. RR+ )
85 82 84 eqeltrd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( m / n ) ) e. RR+ )
86 78 85 rpdivcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) e. RR+ )
87 86 rpcnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) e. CC )
88 87 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) : NN --> CC )
89 elfznn 
 |-  ( b e. ( 1 ... a ) -> b e. NN )
90 ffvelcdm 
 |-  ( ( ( 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 )
91 88 89 90 syl2an 
 |-  ( ( m e. NN0 /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) e. CC )
92 91 adantlr 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ b e. ( 1 ... a ) ) -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) e. CC )
93 mulcl 
 |-  ( ( b e. CC /\ x e. CC ) -> ( b x. x ) e. CC )
94 93 adantl 
 |-  ( ( ( m e. NN0 /\ a e. NN ) /\ ( b e. CC /\ x e. CC ) ) -> ( b x. x ) e. CC )
95 69 92 94 seqcl 
 |-  ( ( m e. NN0 /\ a e. NN ) -> ( seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ` a ) e. CC )
96 95 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 )
97 85 75 rpmulcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) e. RR+ )
98 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
99 98 nnrpd 
 |-  ( m e. NN0 -> ( m + 1 ) e. RR+ )
100 rpdivcl 
 |-  ( ( ( m + 1 ) e. RR+ /\ n e. RR+ ) -> ( ( m + 1 ) / n ) e. RR+ )
101 99 72 100 syl2an 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( m + 1 ) / n ) e. RR+ )
102 71 101 rpaddcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( 1 + ( ( m + 1 ) / n ) ) e. RR+ )
103 97 102 rpdivcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) e. RR+ )
104 103 rpcnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) e. CC )
105 104 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) ) : NN --> CC )
106 ffvelcdm 
 |-  ( ( ( 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 )
107 105 89 106 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 )
108 107 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 )
109 69 108 94 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 )
110 109 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 )
111 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 ) ) ) ) )
112 oveq2 
 |-  ( n = b -> ( 1 / n ) = ( 1 / b ) )
113 112 oveq2d 
 |-  ( n = b -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / b ) ) )
114 113 oveq1d 
 |-  ( n = b -> ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) = ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) )
115 oveq2 
 |-  ( n = b -> ( ( m + 1 ) / n ) = ( ( m + 1 ) / b ) )
116 115 oveq2d 
 |-  ( n = b -> ( 1 + ( ( m + 1 ) / n ) ) = ( 1 + ( ( m + 1 ) / b ) ) )
117 114 116 oveq12d 
 |-  ( n = b -> ( ( ( 1 + ( 1 / n ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / n ) ) ) = ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) )
118 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 ) ) ) )
119 ovex 
 |-  ( ( ( 1 + ( 1 / b ) ) ^ ( m + 1 ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) e. _V
120 117 118 119 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 ) ) ) )
121 120 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 ) ) ) )
122 113 oveq1d 
 |-  ( n = b -> ( ( 1 + ( 1 / n ) ) ^ m ) = ( ( 1 + ( 1 / b ) ) ^ m ) )
123 oveq2 
 |-  ( n = b -> ( m / n ) = ( m / b ) )
124 123 oveq2d 
 |-  ( n = b -> ( 1 + ( m / n ) ) = ( 1 + ( m / b ) ) )
125 122 124 oveq12d 
 |-  ( n = b -> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) = ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) )
126 eqid 
 |-  ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) = ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) )
127 ovex 
 |-  ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) e. _V
128 125 126 127 fvmpt 
 |-  ( b e. NN -> ( ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ` b ) = ( ( ( 1 + ( 1 / b ) ) ^ m ) / ( 1 + ( m / b ) ) ) )
129 124 113 oveq12d 
 |-  ( n = b -> ( ( 1 + ( m / n ) ) x. ( 1 + ( 1 / n ) ) ) = ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) )
130 129 116 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 ) ) ) )
131 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 ) ) ) )
132 ovex 
 |-  ( ( ( 1 + ( m / b ) ) x. ( 1 + ( 1 / b ) ) ) / ( 1 + ( ( m + 1 ) / b ) ) ) e. _V
133 130 131 132 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 ) ) ) )
134 128 133 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 ) ) ) ) )
135 134 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 ) ) ) ) )
136 111 121 135 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 ) ) )
137 89 136 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 ) ) )
138 137 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 ) ) )
139 69 92 108 138 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 ) ) )
140 139 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 ) ) )
141 57 62 63 65 67 96 110 140 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 ) ) )
142 facp1 
 |-  ( m e. NN0 -> ( ! ` ( m + 1 ) ) = ( ( ! ` m ) x. ( m + 1 ) ) )
143 142 adantr 
 |-  ( ( m e. NN0 /\ seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ m ) / ( 1 + ( m / n ) ) ) ) ) ~~> ( ! ` m ) ) -> ( ! ` ( m + 1 ) ) = ( ( ! ` m ) x. ( m + 1 ) ) )
144 141 143 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 ) ) )
145 144 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 ) ) ) )
146 13 21 29 37 61 145 nn0ind 
 |-  ( A e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( 1 / n ) ) ^ A ) / ( 1 + ( A / n ) ) ) ) ) ~~> ( ! ` A ) )
147 3 146 eqbrtrid 
 |-  ( A e. NN0 -> seq 1 ( x. , F ) ~~> ( ! ` A ) )