Metamath Proof Explorer

Theorem faclim2

Description: Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 faclim2.1 
 |-  F = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) )
2 oveq2 
 |-  ( a = 0 -> ( ( n + 1 ) ^ a ) = ( ( n + 1 ) ^ 0 ) )
3 2 oveq2d 
 |-  ( a = 0 -> ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) = ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) )
4 oveq2 
 |-  ( a = 0 -> ( n + a ) = ( n + 0 ) )
5 4 fveq2d 
 |-  ( a = 0 -> ( ! ` ( n + a ) ) = ( ! ` ( n + 0 ) ) )
6 3 5 oveq12d 
 |-  ( a = 0 -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) = ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) )
7 6 mpteq2dv 
 |-  ( a = 0 -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) )
8 7 breq1d 
 |-  ( a = 0 -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) ~~> 1 <-> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ~~> 1 ) )
9 oveq2 
 |-  ( a = m -> ( ( n + 1 ) ^ a ) = ( ( n + 1 ) ^ m ) )
10 9 oveq2d 
 |-  ( a = m -> ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) = ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) )
11 oveq2 
 |-  ( a = m -> ( n + a ) = ( n + m ) )
12 11 fveq2d 
 |-  ( a = m -> ( ! ` ( n + a ) ) = ( ! ` ( n + m ) ) )
13 10 12 oveq12d 
 |-  ( a = m -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) = ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) )
14 13 mpteq2dv 
 |-  ( a = m -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) )
15 14 breq1d 
 |-  ( a = m -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) ~~> 1 <-> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) )
16 oveq2 
 |-  ( a = ( m + 1 ) -> ( ( n + 1 ) ^ a ) = ( ( n + 1 ) ^ ( m + 1 ) ) )
17 16 oveq2d 
 |-  ( a = ( m + 1 ) -> ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) = ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) )
18 oveq2 
 |-  ( a = ( m + 1 ) -> ( n + a ) = ( n + ( m + 1 ) ) )
19 18 fveq2d 
 |-  ( a = ( m + 1 ) -> ( ! ` ( n + a ) ) = ( ! ` ( n + ( m + 1 ) ) ) )
20 17 19 oveq12d 
 |-  ( a = ( m + 1 ) -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) = ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) )
21 20 mpteq2dv 
 |-  ( a = ( m + 1 ) -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) )
22 21 breq1d 
 |-  ( a = ( m + 1 ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) ~~> 1 <-> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ~~> 1 ) )
23 oveq2 
 |-  ( a = M -> ( ( n + 1 ) ^ a ) = ( ( n + 1 ) ^ M ) )
24 23 oveq2d 
 |-  ( a = M -> ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) = ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) )
25 oveq2 
 |-  ( a = M -> ( n + a ) = ( n + M ) )
26 25 fveq2d 
 |-  ( a = M -> ( ! ` ( n + a ) ) = ( ! ` ( n + M ) ) )
27 24 26 oveq12d 
 |-  ( a = M -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) = ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) )
28 27 mpteq2dv 
 |-  ( a = M -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) ) )
29 28 breq1d 
 |-  ( a = M -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ a ) ) / ( ! ` ( n + a ) ) ) ) ~~> 1 <-> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) ) ~~> 1 ) )
30 nnuz 
 |-  NN = ( ZZ>= ` 1 )
31 1zzd 
 |-  ( T. -> 1 e. ZZ )
32 nnex 
 |-  NN e. _V
33 32 mptex 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) e. _V
34 33 a1i 
 |-  ( T. -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) e. _V )
35 1cnd 
 |-  ( T. -> 1 e. CC )
36 fveq2 
 |-  ( n = m -> ( ! ` n ) = ( ! ` m ) )
37 oveq1 
 |-  ( n = m -> ( n + 1 ) = ( m + 1 ) )
38 37 oveq1d 
 |-  ( n = m -> ( ( n + 1 ) ^ 0 ) = ( ( m + 1 ) ^ 0 ) )
39 36 38 oveq12d 
 |-  ( n = m -> ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) = ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) )
40 fvoveq1 
 |-  ( n = m -> ( ! ` ( n + 0 ) ) = ( ! ` ( m + 0 ) ) )
41 39 40 oveq12d 
 |-  ( n = m -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) = ( ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) / ( ! ` ( m + 0 ) ) ) )
42 eqid 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) )
43 ovex 
 |-  ( ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) / ( ! ` ( m + 0 ) ) ) e. _V
44 41 42 43 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ` m ) = ( ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) / ( ! ` ( m + 0 ) ) ) )
45 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
46 45 nncnd 
 |-  ( m e. NN -> ( m + 1 ) e. CC )
47 46 exp0d 
 |-  ( m e. NN -> ( ( m + 1 ) ^ 0 ) = 1 )
48 47 oveq2d 
 |-  ( m e. NN -> ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) = ( ( ! ` m ) x. 1 ) )
49 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
50 faccl 
 |-  ( m e. NN0 -> ( ! ` m ) e. NN )
51 49 50 syl 
 |-  ( m e. NN -> ( ! ` m ) e. NN )
52 51 nncnd 
 |-  ( m e. NN -> ( ! ` m ) e. CC )
53 52 mulridd 
 |-  ( m e. NN -> ( ( ! ` m ) x. 1 ) = ( ! ` m ) )
54 48 53 eqtrd 
 |-  ( m e. NN -> ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) = ( ! ` m ) )
55 nncn 
 |-  ( m e. NN -> m e. CC )
56 55 addridd 
 |-  ( m e. NN -> ( m + 0 ) = m )
57 56 fveq2d 
 |-  ( m e. NN -> ( ! ` ( m + 0 ) ) = ( ! ` m ) )
58 54 57 oveq12d 
 |-  ( m e. NN -> ( ( ( ! ` m ) x. ( ( m + 1 ) ^ 0 ) ) / ( ! ` ( m + 0 ) ) ) = ( ( ! ` m ) / ( ! ` m ) ) )
59 51 nnne0d 
 |-  ( m e. NN -> ( ! ` m ) =/= 0 )
60 52 59 dividd 
 |-  ( m e. NN -> ( ( ! ` m ) / ( ! ` m ) ) = 1 )
61 44 58 60 3eqtrd 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ` m ) = 1 )
62 61 adantl 
 |-  ( ( T. /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ` m ) = 1 )
63 30 31 34 35 62 climconst 
 |-  ( T. -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ~~> 1 )
64 63 mptru 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ 0 ) ) / ( ! ` ( n + 0 ) ) ) ) ~~> 1
65 1zzd 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> 1 e. ZZ )
66 simpr 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 )
67 32 mptex 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) e. _V
68 67 a1i 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) e. _V )
69 1zzd 
 |-  ( m e. NN0 -> 1 e. ZZ )
70 1cnd 
 |-  ( m e. NN0 -> 1 e. CC )
71 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
72 71 nnzd 
 |-  ( m e. NN0 -> ( m + 1 ) e. ZZ )
73 32 mptex 
 |-  ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) e. _V
74 73 a1i 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) e. _V )
75 oveq1 
 |-  ( n = k -> ( n + 1 ) = ( k + 1 ) )
76 oveq1 
 |-  ( n = k -> ( n + ( m + 1 ) ) = ( k + ( m + 1 ) ) )
77 75 76 oveq12d 
 |-  ( n = k -> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) = ( ( k + 1 ) / ( k + ( m + 1 ) ) ) )
78 eqid 
 |-  ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) = ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) )
79 ovex 
 |-  ( ( k + 1 ) / ( k + ( m + 1 ) ) ) e. _V
80 77 78 79 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) = ( ( k + 1 ) / ( k + ( m + 1 ) ) ) )
81 80 adantl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) = ( ( k + 1 ) / ( k + ( m + 1 ) ) ) )
82 30 69 70 72 74 81 divcnvlin 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ~~> 1 )
83 82 adantr 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ~~> 1 )
84 simpr 
 |-  ( ( m e. NN0 /\ n e. NN ) -> n e. NN )
85 84 nnnn0d 
 |-  ( ( m e. NN0 /\ n e. NN ) -> n e. NN0 )
86 faccl 
 |-  ( n e. NN0 -> ( ! ` n ) e. NN )
87 85 86 syl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ! ` n ) e. NN )
88 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
89 nnexpcl 
 |-  ( ( ( n + 1 ) e. NN /\ m e. NN0 ) -> ( ( n + 1 ) ^ m ) e. NN )
90 88 89 sylan 
 |-  ( ( n e. NN /\ m e. NN0 ) -> ( ( n + 1 ) ^ m ) e. NN )
91 90 ancoms 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( n + 1 ) ^ m ) e. NN )
92 87 91 nnmulcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) e. NN )
93 92 nnred 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) e. RR )
94 nnnn0addcl 
 |-  ( ( n e. NN /\ m e. NN0 ) -> ( n + m ) e. NN )
95 94 ancoms 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( n + m ) e. NN )
96 95 nnnn0d 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( n + m ) e. NN0 )
97 faccl 
 |-  ( ( n + m ) e. NN0 -> ( ! ` ( n + m ) ) e. NN )
98 96 97 syl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ! ` ( n + m ) ) e. NN )
99 93 98 nndivred 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) e. RR )
100 99 recnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) e. CC )
101 100 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) : NN --> CC )
102 101 ffvelcdmda 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) e. CC )
103 102 adantlr 
 |-  ( ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) e. CC )
104 88 adantl 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( n + 1 ) e. NN )
105 104 nnred 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( n + 1 ) e. RR )
106 71 adantr 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( m + 1 ) e. NN )
107 84 106 nnaddcld 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( n + ( m + 1 ) ) e. NN )
108 105 107 nndivred 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) e. RR )
109 108 recnd 
 |-  ( ( m e. NN0 /\ n e. NN ) -> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) e. CC )
110 109 fmpttd 
 |-  ( m e. NN0 -> ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) : NN --> CC )
111 110 ffvelcdmda 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) e. CC )
112 111 adantlr 
 |-  ( ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) e. CC )
113 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
114 113 adantl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + 1 ) e. NN )
115 114 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + 1 ) e. CC )
116 simpl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> m e. NN0 )
117 115 116 expp1d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( k + 1 ) ^ ( m + 1 ) ) = ( ( ( k + 1 ) ^ m ) x. ( k + 1 ) ) )
118 117 oveq2d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) = ( ( ! ` k ) x. ( ( ( k + 1 ) ^ m ) x. ( k + 1 ) ) ) )
119 simpr 
 |-  ( ( m e. NN0 /\ k e. NN ) -> k e. NN )
120 119 nnnn0d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> k e. NN0 )
121 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
122 120 121 syl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` k ) e. NN )
123 122 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` k ) e. CC )
124 nnexpcl 
 |-  ( ( ( k + 1 ) e. NN /\ m e. NN0 ) -> ( ( k + 1 ) ^ m ) e. NN )
125 113 124 sylan 
 |-  ( ( k e. NN /\ m e. NN0 ) -> ( ( k + 1 ) ^ m ) e. NN )
126 125 ancoms 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( k + 1 ) ^ m ) e. NN )
127 126 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( k + 1 ) ^ m ) e. CC )
128 123 127 115 mulassd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) x. ( k + 1 ) ) = ( ( ! ` k ) x. ( ( ( k + 1 ) ^ m ) x. ( k + 1 ) ) ) )
129 118 128 eqtr4d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) x. ( k + 1 ) ) )
130 120 116 nn0addcld 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + m ) e. NN0 )
131 facp1 
 |-  ( ( k + m ) e. NN0 -> ( ! ` ( ( k + m ) + 1 ) ) = ( ( ! ` ( k + m ) ) x. ( ( k + m ) + 1 ) ) )
132 130 131 syl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( ( k + m ) + 1 ) ) = ( ( ! ` ( k + m ) ) x. ( ( k + m ) + 1 ) ) )
133 119 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> k e. CC )
134 116 nn0cnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> m e. CC )
135 1cnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> 1 e. CC )
136 133 134 135 addassd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( k + m ) + 1 ) = ( k + ( m + 1 ) ) )
137 136 fveq2d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( ( k + m ) + 1 ) ) = ( ! ` ( k + ( m + 1 ) ) ) )
138 136 oveq2d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ! ` ( k + m ) ) x. ( ( k + m ) + 1 ) ) = ( ( ! ` ( k + m ) ) x. ( k + ( m + 1 ) ) ) )
139 132 137 138 3eqtr3d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( k + ( m + 1 ) ) ) = ( ( ! ` ( k + m ) ) x. ( k + ( m + 1 ) ) ) )
140 129 139 oveq12d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) = ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) x. ( k + 1 ) ) / ( ( ! ` ( k + m ) ) x. ( k + ( m + 1 ) ) ) ) )
141 122 126 nnmulcld 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) e. NN )
142 141 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) e. CC )
143 faccl 
 |-  ( ( k + m ) e. NN0 -> ( ! ` ( k + m ) ) e. NN )
144 130 143 syl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( k + m ) ) e. NN )
145 144 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( k + m ) ) e. CC )
146 71 adantr 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( m + 1 ) e. NN )
147 119 146 nnaddcld 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + ( m + 1 ) ) e. NN )
148 147 nncnd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + ( m + 1 ) ) e. CC )
149 144 nnne0d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ! ` ( k + m ) ) =/= 0 )
150 147 nnne0d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( k + ( m + 1 ) ) =/= 0 )
151 142 145 115 148 149 150 divmuldivd 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) x. ( ( k + 1 ) / ( k + ( m + 1 ) ) ) ) = ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) x. ( k + 1 ) ) / ( ( ! ` ( k + m ) ) x. ( k + ( m + 1 ) ) ) ) )
152 140 151 eqtr4d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) = ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) x. ( ( k + 1 ) / ( k + ( m + 1 ) ) ) ) )
153 fveq2 
 |-  ( n = k -> ( ! ` n ) = ( ! ` k ) )
154 75 oveq1d 
 |-  ( n = k -> ( ( n + 1 ) ^ ( m + 1 ) ) = ( ( k + 1 ) ^ ( m + 1 ) ) )
155 153 154 oveq12d 
 |-  ( n = k -> ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) = ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) )
156 fvoveq1 
 |-  ( n = k -> ( ! ` ( n + ( m + 1 ) ) ) = ( ! ` ( k + ( m + 1 ) ) ) )
157 155 156 oveq12d 
 |-  ( n = k -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) )
158 eqid 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) )
159 ovex 
 |-  ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) e. _V
160 157 158 159 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ` k ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) )
161 160 adantl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ` k ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( k + ( m + 1 ) ) ) ) )
162 75 oveq1d 
 |-  ( n = k -> ( ( n + 1 ) ^ m ) = ( ( k + 1 ) ^ m ) )
163 153 162 oveq12d 
 |-  ( n = k -> ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) = ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) )
164 fvoveq1 
 |-  ( n = k -> ( ! ` ( n + m ) ) = ( ! ` ( k + m ) ) )
165 163 164 oveq12d 
 |-  ( n = k -> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) )
166 eqid 
 |-  ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) )
167 ovex 
 |-  ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) e. _V
168 165 166 167 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) = ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) )
169 168 80 oveq12d 
 |-  ( k e. NN -> ( ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) x. ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) ) = ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) x. ( ( k + 1 ) / ( k + ( m + 1 ) ) ) ) )
170 169 adantl 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) x. ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) ) = ( ( ( ( ! ` k ) x. ( ( k + 1 ) ^ m ) ) / ( ! ` ( k + m ) ) ) x. ( ( k + 1 ) / ( k + ( m + 1 ) ) ) ) )
171 152 161 170 3eqtr4d 
 |-  ( ( m e. NN0 /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ` k ) = ( ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) x. ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) ) )
172 171 adantlr 
 |-  ( ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ` k ) = ( ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ` k ) x. ( ( n e. NN |-> ( ( n + 1 ) / ( n + ( m + 1 ) ) ) ) ` k ) ) )
173 30 65 66 68 83 103 112 172 climmul 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ~~> ( 1 x. 1 ) )
174 1t1e1 
 |-  ( 1 x. 1 ) = 1
175 173 174 breqtrdi 
 |-  ( ( m e. NN0 /\ ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 ) -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ~~> 1 )
176 175 ex 
 |-  ( m e. NN0 -> ( ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ m ) ) / ( ! ` ( n + m ) ) ) ) ~~> 1 -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ ( m + 1 ) ) ) / ( ! ` ( n + ( m + 1 ) ) ) ) ) ~~> 1 ) )
177 8 15 22 29 64 176 nn0ind 
 |-  ( M e. NN0 -> ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) ) ~~> 1 )
178 1 177 eqbrtrid 
 |-  ( M e. NN0 -> F ~~> 1 )