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 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n = x M + 1 x + 1 x + M + 1

Proof

Step Hyp Ref Expression
1 fveq2 a = 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n 1
2 1z 1
3 seq1 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n 1 = n 1 + M n 1 + 1 n 1 + M + 1 n 1
4 2 3 ax-mp seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n 1 = n 1 + M n 1 + 1 n 1 + M + 1 n 1
5 1 4 eqtrdi a = 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = n 1 + M n 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 a + 1 a + M + 1 = M + 1 1 + 1 1 + M + 1
10 5 9 eqeq12d a = 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n 1 = M + 1 1 + 1 1 + M + 1
11 10 imbi2d a = 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 M 0 n 1 + M n 1 + 1 n 1 + M + 1 n 1 = M + 1 1 + 1 1 + M + 1
12 fveq2 a = k seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = seq 1 × n 1 + M n 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 a + 1 a + M + 1 = M + 1 k + 1 k + M + 1
17 12 16 eqeq12d a = k seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1
18 17 imbi2d a = k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1
19 fveq2 a = k + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = seq 1 × n 1 + M n 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 a + 1 a + M + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
24 19 23 eqeq12d a = k + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
25 24 imbi2d a = k + 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
26 fveq2 a = b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = seq 1 × n 1 + M n 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 a + 1 a + M + 1 = M + 1 b + 1 b + M + 1
31 26 30 eqeq12d a = b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = M + 1 b + 1 b + M + 1
32 31 imbi2d a = b M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n a = M + 1 a + 1 a + M + 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = M + 1 b + 1 b + M + 1
33 1nn 1
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 1 + 1 n = 1 + M 1 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 1 + 1 n 1 + M + 1 n = 1 + M 1 1 + 1 1 1 + M + 1 1
42 eqid n 1 + M n 1 + 1 n 1 + M + 1 n = n 1 + M n 1 + 1 n 1 + M + 1 n
43 ovex 1 + M 1 1 + 1 1 1 + M + 1 1 V
44 41 42 43 fvmpt 1 n 1 + M n 1 + 1 n 1 + M + 1 n 1 = 1 + M 1 1 + 1 1 1 + M + 1 1
45 33 44 ax-mp n 1 + M n 1 + 1 n 1 + M + 1 n 1 = 1 + M 1 1 + 1 1 1 + M + 1 1
46 nn0cn M 0 M
47 46 div1d M 0 M 1 = M
48 47 oveq2d M 0 1 + M 1 = 1 + M
49 1div1e1 1 1 = 1
50 49 oveq2i 1 + 1 1 = 1 + 1
51 50 a1i M 0 1 + 1 1 = 1 + 1
52 48 51 oveq12d M 0 1 + M 1 1 + 1 1 = 1 + M 1 + 1
53 nn0p1nn M 0 M + 1
54 53 nncnd M 0 M + 1
55 54 div1d M 0 M + 1 1 = M + 1
56 55 oveq2d M 0 1 + M + 1 1 = 1 + M + 1
57 52 56 oveq12d M 0 1 + M 1 1 + 1 1 1 + M + 1 1 = 1 + M 1 + 1 1 + M + 1
58 1cnd M 0 1
59 58 46 addcomd M 0 1 + M = M + 1
60 59 oveq1d M 0 1 + M 1 + 1 = M + 1 1 + 1
61 60 oveq1d M 0 1 + M 1 + 1 1 + M + 1 = M + 1 1 + 1 1 + M + 1
62 ax-1cn 1
63 62 62 addcli 1 + 1
64 63 a1i M 0 1 + 1
65 33 a1i M 0 1
66 65 53 nnaddcld M 0 1 + M + 1
67 66 nncnd M 0 1 + M + 1
68 66 nnne0d M 0 1 + M + 1 0
69 54 64 67 68 divassd M 0 M + 1 1 + 1 1 + M + 1 = M + 1 1 + 1 1 + M + 1
70 57 61 69 3eqtrd M 0 1 + M 1 1 + 1 1 1 + M + 1 1 = M + 1 1 + 1 1 + M + 1
71 45 70 syl5eq M 0 n 1 + M n 1 + 1 n 1 + M + 1 n 1 = M + 1 1 + 1 1 + M + 1
72 seqp1 k 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
73 nnuz = 1
74 72 73 eleq2s k seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
75 74 adantr k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
76 75 adantr k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
77 oveq1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
78 77 adantl k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1
79 peano2nn k k + 1
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 1 + 1 n = 1 + M k + 1 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 1 + 1 n 1 + M + 1 n = 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
88 ovex 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 V
89 87 42 88 fvmpt k + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
90 79 89 syl k n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
91 90 oveq2d k M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
92 91 adantr k M 0 M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
93 53 adantl k M 0 M + 1
94 93 nncnd k M 0 M + 1
95 79 adantr k M 0 k + 1
96 95 nnrpd k M 0 k + 1 +
97 simpl k M 0 k
98 97 nnrpd k M 0 k +
99 93 nnrpd k M 0 M + 1 +
100 98 99 rpaddcld k M 0 k + M + 1 +
101 96 100 rpdivcld k M 0 k + 1 k + M + 1 +
102 101 rpcnd k M 0 k + 1 k + M + 1
103 1cnd k M 0 1
104 nn0re M 0 M
105 104 adantl k M 0 M
106 105 95 nndivred k M 0 M k + 1
107 106 recnd k M 0 M k + 1
108 103 107 addcomd k M 0 1 + M k + 1 = M k + 1 + 1
109 nn0ge0 M 0 0 M
110 109 adantl k M 0 0 M
111 105 96 110 divge0d k M 0 0 M k + 1
112 106 111 ge0p1rpd k M 0 M k + 1 + 1 +
113 108 112 eqeltrd k M 0 1 + M k + 1 +
114 1rp 1 +
115 114 a1i k M 0 1 +
116 96 rpreccld k M 0 1 k + 1 +
117 115 116 rpaddcld k M 0 1 + 1 k + 1 +
118 113 117 rpmulcld k M 0 1 + M k + 1 1 + 1 k + 1 +
119 99 96 rpdivcld k M 0 M + 1 k + 1 +
120 115 119 rpaddcld k M 0 1 + M + 1 k + 1 +
121 118 120 rpdivcld k M 0 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 +
122 121 rpcnd k M 0 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
123 94 102 122 mulassd k M 0 M + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 = M + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
124 101 118 rpmulcld k M 0 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 +
125 124 rpcnd k M 0 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1
126 120 rpcnd k M 0 1 + M + 1 k + 1
127 95 nncnd k M 0 k + 1
128 120 rpne0d k M 0 1 + M + 1 k + 1 0
129 95 nnne0d k M 0 k + 1 0
130 125 126 127 128 129 divcan5d k M 0 k + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 k + 1 1 + M + 1 k + 1 = k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
131 118 rpcnd k M 0 1 + M k + 1 1 + 1 k + 1
132 127 102 131 mul12d k M 0 k + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 = k + 1 k + M + 1 k + 1 1 + M k + 1 1 + 1 k + 1
133 113 rpcnd k M 0 1 + M k + 1
134 117 rpcnd k M 0 1 + 1 k + 1
135 127 133 134 mulassd k M 0 k + 1 1 + M k + 1 1 + 1 k + 1 = k + 1 1 + M k + 1 1 + 1 k + 1
136 127 103 107 adddid k M 0 k + 1 1 + M k + 1 = k + 1 1 + k + 1 M k + 1
137 127 mulid1d k M 0 k + 1 1 = k + 1
138 simpr k M 0 M 0
139 138 nn0cnd k M 0 M
140 139 127 129 divcan2d k M 0 k + 1 M k + 1 = M
141 137 140 oveq12d k M 0 k + 1 1 + k + 1 M k + 1 = k + 1 + M
142 97 nncnd k M 0 k
143 142 103 139 addassd k M 0 k + 1 + M = k + 1 + M
144 103 139 addcomd k M 0 1 + M = M + 1
145 144 oveq2d k M 0 k + 1 + M = k + M + 1
146 143 145 eqtrd k M 0 k + 1 + M = k + M + 1
147 136 141 146 3eqtrd k M 0 k + 1 1 + M k + 1 = k + M + 1
148 147 oveq1d k M 0 k + 1 1 + M k + 1 1 + 1 k + 1 = k + M + 1 1 + 1 k + 1
149 135 148 eqtr3d k M 0 k + 1 1 + M k + 1 1 + 1 k + 1 = k + M + 1 1 + 1 k + 1
150 149 oveq2d k M 0 k + 1 k + M + 1 k + 1 1 + M k + 1 1 + 1 k + 1 = k + 1 k + M + 1 k + M + 1 1 + 1 k + 1
151 100 rpcnd k M 0 k + M + 1
152 102 151 134 mulassd k M 0 k + 1 k + M + 1 k + M + 1 1 + 1 k + 1 = k + 1 k + M + 1 k + M + 1 1 + 1 k + 1
153 100 rpne0d k M 0 k + M + 1 0
154 127 151 153 divcan1d k M 0 k + 1 k + M + 1 k + M + 1 = k + 1
155 154 oveq1d k M 0 k + 1 k + M + 1 k + M + 1 1 + 1 k + 1 = k + 1 1 + 1 k + 1
156 116 rpcnd k M 0 1 k + 1
157 127 103 156 adddid k M 0 k + 1 1 + 1 k + 1 = k + 1 1 + k + 1 1 k + 1
158 103 127 129 divcan2d k M 0 k + 1 1 k + 1 = 1
159 137 158 oveq12d k M 0 k + 1 1 + k + 1 1 k + 1 = k + 1 + 1
160 155 157 159 3eqtrd k M 0 k + 1 k + M + 1 k + M + 1 1 + 1 k + 1 = k + 1 + 1
161 152 160 eqtr3d k M 0 k + 1 k + M + 1 k + M + 1 1 + 1 k + 1 = k + 1 + 1
162 132 150 161 3eqtrd k M 0 k + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 = k + 1 + 1
163 119 rpcnd k M 0 M + 1 k + 1
164 127 103 163 adddid k M 0 k + 1 1 + M + 1 k + 1 = k + 1 1 + k + 1 M + 1 k + 1
165 94 127 129 divcan2d k M 0 k + 1 M + 1 k + 1 = M + 1
166 137 165 oveq12d k M 0 k + 1 1 + k + 1 M + 1 k + 1 = k + 1 + M + 1
167 164 166 eqtrd k M 0 k + 1 1 + M + 1 k + 1 = k + 1 + M + 1
168 162 167 oveq12d k M 0 k + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 k + 1 1 + M + 1 k + 1 = k + 1 + 1 k + 1 + M + 1
169 102 131 126 128 divassd k M 0 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 = k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1
170 130 168 169 3eqtr3rd k M 0 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 = k + 1 + 1 k + 1 + M + 1
171 170 oveq2d k M 0 M + 1 k + 1 k + M + 1 1 + M k + 1 1 + 1 k + 1 1 + M + 1 k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
172 92 123 171 3eqtrd k M 0 M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
173 172 adantr k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 M + 1 k + 1 k + M + 1 n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
174 76 78 173 3eqtrd k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
175 174 exp31 k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
176 175 a2d k M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k = M + 1 k + 1 k + M + 1 M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n k + 1 = M + 1 k + 1 + 1 k + 1 + M + 1
177 11 18 25 32 71 176 nnind b M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = M + 1 b + 1 b + M + 1
178 177 impcom M 0 b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = M + 1 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 + 1 x + M + 1 = M + 1 b + 1 b + M + 1
183 eqid x M + 1 x + 1 x + M + 1 = x M + 1 x + 1 x + M + 1
184 ovex M + 1 b + 1 b + M + 1 V
185 182 183 184 fvmpt b x M + 1 x + 1 x + M + 1 b = M + 1 b + 1 b + M + 1
186 185 adantl M 0 b x M + 1 x + 1 x + M + 1 b = M + 1 b + 1 b + M + 1
187 178 186 eqtr4d M 0 b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = x M + 1 x + 1 x + M + 1 b
188 187 ralrimiva M 0 b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = x M + 1 x + 1 x + M + 1 b
189 seqfn 1 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn 1
190 2 189 ax-mp seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn 1
191 73 fneq2i seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn 1
192 190 191 mpbir seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn
193 ovex M + 1 x + 1 x + M + 1 V
194 193 183 fnmpti x M + 1 x + 1 x + M + 1 Fn
195 eqfnfv seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n Fn x M + 1 x + 1 x + M + 1 Fn seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n = x M + 1 x + 1 x + M + 1 b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = x M + 1 x + 1 x + M + 1 b
196 192 194 195 mp2an seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n = x M + 1 x + 1 x + M + 1 b seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n b = x M + 1 x + 1 x + M + 1 b
197 188 196 sylibr M 0 seq 1 × n 1 + M n 1 + 1 n 1 + M + 1 n = x M + 1 x + 1 x + M + 1