Metamath Proof Explorer


Theorem faclbnd4lem1

Description: Lemma for faclbnd4 . Prepare the induction step. (Contributed by NM, 20-Dec-2005)

Ref Expression
Hypotheses faclbnd4lem1.1 N
faclbnd4lem1.2 K 0
faclbnd4lem1.3 M 0
Assertion faclbnd4lem1 N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !

Proof

Step Hyp Ref Expression
1 faclbnd4lem1.1 N
2 faclbnd4lem1.2 K 0
3 faclbnd4lem1.3 M 0
4 1 nnrei N
5 1re 1
6 lelttric N 1 N 1 1 < N
7 4 5 6 mp2an N 1 1 < N
8 nnge1 N 1 N
9 1 8 ax-mp 1 N
10 4 5 letri3i N = 1 N 1 1 N
11 9 10 mpbiran2 N = 1 N 1
12 0le1 0 1
13 5 12 pm3.2i 1 0 1
14 2re 2
15 1nn 1
16 nn0nnaddcl K 0 1 K + 1
17 2 15 16 mp2an K + 1
18 17 nnnn0i K + 1 0
19 2nn0 2 0
20 18 19 nn0expcli K + 1 2 0
21 reexpcl 2 K + 1 2 0 2 K + 1 2
22 14 20 21 mp2an 2 K + 1 2
23 13 22 pm3.2i 1 0 1 2 K + 1 2
24 3 nn0rei M
25 3 nn0ge0i 0 M
26 24 25 pm3.2i M 0 M
27 nn0nnaddcl M 0 K + 1 M + K + 1
28 3 17 27 mp2an M + K + 1
29 28 nnnn0i M + K + 1 0
30 3 29 nn0expcli M M + K + 1 0
31 30 nn0rei M M + K + 1
32 26 31 pm3.2i M 0 M M M + K + 1
33 23 32 pm3.2i 1 0 1 2 K + 1 2 M 0 M M M + K + 1
34 2cn 2
35 exp0 2 2 0 = 1
36 34 35 ax-mp 2 0 = 1
37 1le2 1 2
38 nn0uz 0 = 0
39 20 38 eleqtri K + 1 2 0
40 leexp2a 2 1 2 K + 1 2 0 2 0 2 K + 1 2
41 14 37 39 40 mp3an 2 0 2 K + 1 2
42 36 41 eqbrtrri 1 2 K + 1 2
43 elnn0 M 0 M M = 0
44 nncn M M
45 44 exp1d M M 1 = M
46 nnge1 M 1 M
47 nnuz = 1
48 28 47 eleqtri M + K + 1 1
49 leexp2a M 1 M M + K + 1 1 M 1 M M + K + 1
50 24 48 49 mp3an13 1 M M 1 M M + K + 1
51 46 50 syl M M 1 M M + K + 1
52 45 51 eqbrtrrd M M M M + K + 1
53 30 nn0ge0i 0 M M + K + 1
54 breq1 M = 0 M M M + K + 1 0 M M + K + 1
55 53 54 mpbiri M = 0 M M M + K + 1
56 52 55 jaoi M M = 0 M M M + K + 1
57 43 56 sylbi M 0 M M M + K + 1
58 3 57 ax-mp M M M + K + 1
59 42 58 pm3.2i 1 2 K + 1 2 M M M + K + 1
60 lemul12a 1 0 1 2 K + 1 2 M 0 M M M + K + 1 1 2 K + 1 2 M M M + K + 1 1 M 2 K + 1 2 M M + K + 1
61 33 59 60 mp2 1 M 2 K + 1 2 M M + K + 1
62 oveq1 N = 1 N K + 1 = 1 K + 1
63 17 nnzi K + 1
64 1exp K + 1 1 K + 1 = 1
65 63 64 ax-mp 1 K + 1 = 1
66 62 65 eqtrdi N = 1 N K + 1 = 1
67 oveq2 N = 1 M N = M 1
68 3 nn0cni M
69 exp1 M M 1 = M
70 68 69 ax-mp M 1 = M
71 67 70 eqtrdi N = 1 M N = M
72 66 71 oveq12d N = 1 N K + 1 M N = 1 M
73 fveq2 N = 1 N ! = 1 !
74 fac1 1 ! = 1
75 73 74 eqtrdi N = 1 N ! = 1
76 75 oveq2d N = 1 2 K + 1 2 M M + K + 1 N ! = 2 K + 1 2 M M + K + 1 1
77 22 recni 2 K + 1 2
78 30 nn0cni M M + K + 1
79 77 78 mulcli 2 K + 1 2 M M + K + 1
80 79 mulid1i 2 K + 1 2 M M + K + 1 1 = 2 K + 1 2 M M + K + 1
81 76 80 eqtrdi N = 1 2 K + 1 2 M M + K + 1 N ! = 2 K + 1 2 M M + K + 1
82 72 81 breq12d N = 1 N K + 1 M N 2 K + 1 2 M M + K + 1 N ! 1 M 2 K + 1 2 M M + K + 1
83 61 82 mpbiri N = 1 N K + 1 M N 2 K + 1 2 M M + K + 1 N !
84 11 83 sylbir N 1 N K + 1 M N 2 K + 1 2 M M + K + 1 N !
85 84 adantr N 1 N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !
86 reexpcl N K + 1 0 N K + 1
87 4 18 86 mp2an N K + 1
88 1 nnnn0i N 0
89 reexpcl M N 0 M N
90 24 88 89 mp2an M N
91 87 90 remulcli N K + 1 M N
92 91 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N
93 2 19 nn0expcli K 2 0
94 reexpcl 2 K 2 0 2 K 2
95 14 93 94 mp2an 2 K 2
96 19 2 nn0expcli 2 K 0
97 96 nn0rei 2 K
98 95 97 remulcli 2 K 2 2 K
99 faccl N 0 N !
100 88 99 ax-mp N !
101 100 nnnn0i N ! 0
102 30 101 nn0mulcli M M + K + 1 N ! 0
103 102 nn0rei M M + K + 1 N !
104 98 103 remulcli 2 K 2 2 K M M + K + 1 N !
105 104 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K 2 2 K M M + K + 1 N !
106 22 103 remulcli 2 K + 1 2 M M + K + 1 N !
107 106 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K + 1 2 M M + K + 1 N !
108 1 nncni N
109 expp1 N K 0 N K + 1 = N K N
110 108 2 109 mp2an N K + 1 = N K N
111 expm1t M N M N = M N 1 M
112 68 1 111 mp2an M N = M N 1 M
113 110 112 oveq12i N K + 1 M N = N K N M N 1 M
114 reexpcl N K 0 N K
115 4 2 114 mp2an N K
116 115 recni N K
117 elnnnn0 N N N 1 0
118 1 117 mpbi N N 1 0
119 118 simpri N 1 0
120 3 119 nn0expcli M N 1 0
121 120 3 nn0mulcli M N 1 M 0
122 121 nn0cni M N 1 M
123 116 108 122 mulassi N K N M N 1 M = N K N M N 1 M
124 113 123 eqtri N K + 1 M N = N K N M N 1 M
125 88 121 nn0mulcli N M N 1 M 0
126 125 nn0rei N M N 1 M
127 115 126 remulcli N K N M N 1 M
128 127 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K N M N 1 M
129 119 nn0rei N 1
130 reexpcl N 1 K 0 N 1 K
131 129 2 130 mp2an N 1 K
132 120 nn0rei M N 1
133 131 132 remulcli N 1 K M N 1
134 96 88 nn0mulcli 2 K N 0
135 134 3 nn0mulcli 2 K N M 0
136 135 nn0rei 2 K N M
137 133 136 remulcli N 1 K M N 1 2 K N M
138 137 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N 1 K M N 1 2 K N M
139 3 2 nn0addcli M + K 0
140 reexpcl M M + K 0 M M + K
141 24 139 140 mp2an M M + K
142 95 141 remulcli 2 K 2 M M + K
143 faccl N 1 0 N 1 !
144 119 143 ax-mp N 1 !
145 144 nnrei N 1 !
146 142 145 remulcli 2 K 2 M M + K N 1 !
147 146 136 remulcli 2 K 2 M M + K N 1 ! 2 K N M
148 147 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K 2 M M + K N 1 ! 2 K N M
149 97 131 remulcli 2 K N 1 K
150 125 nn0ge0i 0 N M N 1 M
151 126 150 pm3.2i N M N 1 M 0 N M N 1 M
152 115 149 151 3pm3.2i N K 2 K N 1 K N M N 1 M 0 N M N 1 M
153 nnltp1le 1 N 1 < N 1 + 1 N
154 15 1 153 mp2an 1 < N 1 + 1 N
155 df-2 2 = 1 + 1
156 155 breq1i 2 N 1 + 1 N
157 154 156 bitr4i 1 < N 2 N
158 expubnd N K 0 2 N N K 2 K N 1 K
159 4 2 158 mp3an12 2 N N K 2 K N 1 K
160 157 159 sylbi 1 < N N K 2 K N 1 K
161 lemul1a N K 2 K N 1 K N M N 1 M 0 N M N 1 M N K 2 K N 1 K N K N M N 1 M 2 K N 1 K N M N 1 M
162 152 160 161 sylancr 1 < N N K N M N 1 M 2 K N 1 K N M N 1 M
163 96 nn0cni 2 K
164 131 recni N 1 K
165 163 164 108 122 mul4i 2 K N 1 K N M N 1 M = 2 K N N 1 K M N 1 M
166 120 nn0cni M N 1
167 164 166 68 mulassi N 1 K M N 1 M = N 1 K M N 1 M
168 167 oveq2i 2 K N N 1 K M N 1 M = 2 K N N 1 K M N 1 M
169 134 nn0cni 2 K N
170 133 recni N 1 K M N 1
171 169 170 68 mul12i 2 K N N 1 K M N 1 M = N 1 K M N 1 2 K N M
172 165 168 171 3eqtr2i 2 K N 1 K N M N 1 M = N 1 K M N 1 2 K N M
173 162 172 breqtrdi 1 < N N K N M N 1 M N 1 K M N 1 2 K N M
174 173 adantr 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K N M N 1 M N 1 K M N 1 2 K N M
175 135 nn0ge0i 0 2 K N M
176 136 175 pm3.2i 2 K N M 0 2 K N M
177 133 146 176 3pm3.2i N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K N M 0 2 K N M
178 lemul1a N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K N M 0 2 K N M N 1 K M N 1 2 K 2 M M + K N 1 ! N 1 K M N 1 2 K N M 2 K 2 M M + K N 1 ! 2 K N M
179 177 178 mpan N 1 K M N 1 2 K 2 M M + K N 1 ! N 1 K M N 1 2 K N M 2 K 2 M M + K N 1 ! 2 K N M
180 179 adantl 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N 1 K M N 1 2 K N M 2 K 2 M M + K N 1 ! 2 K N M
181 128 138 148 174 180 letrd 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K N M N 1 M 2 K 2 M M + K N 1 ! 2 K N M
182 163 108 68 mul32i 2 K N M = 2 K M N
183 182 oveq2i 2 K 2 M M + K N 1 ! 2 K N M = 2 K 2 M M + K N 1 ! 2 K M N
184 expp1 M M + K 0 M M + K + 1 = M M + K M
185 68 139 184 mp2an M M + K + 1 = M M + K M
186 2 nn0cni K
187 ax-1cn 1
188 68 186 187 addassi M + K + 1 = M + K + 1
189 188 oveq2i M M + K + 1 = M M + K + 1
190 185 189 eqtr3i M M + K M = M M + K + 1
191 190 oveq2i 2 K 2 2 K M M + K M = 2 K 2 2 K M M + K + 1
192 95 recni 2 K 2
193 141 recni M M + K
194 192 163 193 68 mul4i 2 K 2 2 K M M + K M = 2 K 2 M M + K 2 K M
195 191 194 eqtr3i 2 K 2 2 K M M + K + 1 = 2 K 2 M M + K 2 K M
196 facnn2 N N ! = N 1 ! N
197 1 196 ax-mp N ! = N 1 ! N
198 195 197 oveq12i 2 K 2 2 K M M + K + 1 N ! = 2 K 2 M M + K 2 K M N 1 ! N
199 142 recni 2 K 2 M M + K
200 144 nncni N 1 !
201 163 68 mulcli 2 K M
202 199 200 201 108 mul4i 2 K 2 M M + K N 1 ! 2 K M N = 2 K 2 M M + K 2 K M N 1 ! N
203 198 202 eqtr4i 2 K 2 2 K M M + K + 1 N ! = 2 K 2 M M + K N 1 ! 2 K M N
204 98 recni 2 K 2 2 K
205 100 nncni N !
206 204 78 205 mulassi 2 K 2 2 K M M + K + 1 N ! = 2 K 2 2 K M M + K + 1 N !
207 183 203 206 3eqtr2i 2 K 2 M M + K N 1 ! 2 K N M = 2 K 2 2 K M M + K + 1 N !
208 181 207 breqtrdi 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K N M N 1 M 2 K 2 2 K M M + K + 1 N !
209 124 208 eqbrtrid 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K 2 2 K M M + K + 1 N !
210 102 nn0ge0i 0 M M + K + 1 N !
211 103 210 pm3.2i M M + K + 1 N ! 0 M M + K + 1 N !
212 98 22 211 3pm3.2i 2 K 2 2 K 2 K + 1 2 M M + K + 1 N ! 0 M M + K + 1 N !
213 expadd 2 K 2 0 K 0 2 K 2 + K = 2 K 2 2 K
214 34 93 2 213 mp3an 2 K 2 + K = 2 K 2 2 K
215 20 nn0zi K + 1 2
216 2 nn0rei K
217 17 nnrei K + 1
218 18 nn0ge0i 0 K + 1
219 217 218 pm3.2i K + 1 0 K + 1
220 216 217 219 3pm3.2i K K + 1 K + 1 0 K + 1
221 216 ltp1i K < K + 1
222 216 217 221 ltleii K K + 1
223 lemul1a K K + 1 K + 1 0 K + 1 K K + 1 K K + 1 K + 1 K + 1
224 220 222 223 mp2an K K + 1 K + 1 K + 1
225 186 sqvali K 2 = K K
226 186 mulid1i K 1 = K
227 226 eqcomi K = K 1
228 225 227 oveq12i K 2 + K = K K + K 1
229 186 186 187 adddii K K + 1 = K K + K 1
230 228 229 eqtr4i K 2 + K = K K + 1
231 17 nncni K + 1
232 231 sqvali K + 1 2 = K + 1 K + 1
233 224 230 232 3brtr4i K 2 + K K + 1 2
234 93 2 nn0addcli K 2 + K 0
235 234 nn0zi K 2 + K
236 235 eluz1i K + 1 2 K 2 + K K + 1 2 K 2 + K K + 1 2
237 215 233 236 mpbir2an K + 1 2 K 2 + K
238 leexp2a 2 1 2 K + 1 2 K 2 + K 2 K 2 + K 2 K + 1 2
239 14 37 237 238 mp3an 2 K 2 + K 2 K + 1 2
240 214 239 eqbrtrri 2 K 2 2 K 2 K + 1 2
241 lemul1a 2 K 2 2 K 2 K + 1 2 M M + K + 1 N ! 0 M M + K + 1 N ! 2 K 2 2 K 2 K + 1 2 2 K 2 2 K M M + K + 1 N ! 2 K + 1 2 M M + K + 1 N !
242 212 240 241 mp2an 2 K 2 2 K M M + K + 1 N ! 2 K + 1 2 M M + K + 1 N !
243 242 a1i 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! 2 K 2 2 K M M + K + 1 N ! 2 K + 1 2 M M + K + 1 N !
244 92 105 107 209 243 letrd 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !
245 77 78 205 mulassi 2 K + 1 2 M M + K + 1 N ! = 2 K + 1 2 M M + K + 1 N !
246 244 245 breqtrrdi 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !
247 85 246 jaoian N 1 1 < N N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !
248 7 247 mpan N 1 K M N 1 2 K 2 M M + K N 1 ! N K + 1 M N 2 K + 1 2 M M + K + 1 N !