faclbnd4lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > faclbnd4lem1		Structured version Visualization version Unicode version

Theorem faclbnd4lem1 13080

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

**Hypotheses**
Ref	Expression
faclbnd4lem1.1
faclbnd4lem1.2
faclbnd4lem1.3

**Assertion**
Ref	Expression
faclbnd4lem1

**Proof of Theorem faclbnd4lem1**
Step	Hyp	Ref	Expression
1		faclbnd4lem1.1	. . . 4
2	1	nnrei 11029	. . 3
3		1re 10039	. . 3
4		lelttric 10144	. . 3 $/\$ $\/$
5	2, 3, 4	mp2an 708	. 2 $\/$
6		nnge1 11046	. . . . . . 7
7	1, 6	ax-mp 5	. . . . . 6
8	2, 3	letri3i 10153	. . . . . 6 $/\$
9	7, 8	mpbiran2 954	. . . . 5
10		0le1 10551	. . . . . . . . . 10
11	3, 10	pm3.2i 471	. . . . . . . . 9 $/\$
12		2re 11090	. . . . . . . . . 10
13		faclbnd4lem1.2	. . . . . . . . . . . . 13
14		1nn 11031	. . . . . . . . . . . . 13
15		nn0nnaddcl 11324	. . . . . . . . . . . . 13 $/\$
16	13, 14, 15	mp2an 708	. . . . . . . . . . . 12
17	16	nnnn0i 11300	. . . . . . . . . . 11
18		2nn0 11309	. . . . . . . . . . 11
19	17, 18	nn0expcli 12886	. . . . . . . . . 10
20		reexpcl 12877	. . . . . . . . . 10 $/\$
21	12, 19, 20	mp2an 708	. . . . . . . . 9
22	11, 21	pm3.2i 471	. . . . . . . 8 $/\$ $/\$
23		faclbnd4lem1.3	. . . . . . . . . . 11
24	23	nn0rei 11303	. . . . . . . . . 10
25	23	nn0ge0i 11320	. . . . . . . . . 10
26	24, 25	pm3.2i 471	. . . . . . . . 9 $/\$
27		nn0nnaddcl 11324	. . . . . . . . . . . . 13 $/\$
28	23, 16, 27	mp2an 708	. . . . . . . . . . . 12
29	28	nnnn0i 11300	. . . . . . . . . . 11
30	23, 29	nn0expcli 12886	. . . . . . . . . 10
31	30	nn0rei 11303	. . . . . . . . 9
32	26, 31	pm3.2i 471	. . . . . . . 8 $/\$ $/\$
33	22, 32	pm3.2i 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
34		2cn 11091	. . . . . . . . . 10
35		exp0 12864	. . . . . . . . . 10
36	34, 35	ax-mp 5	. . . . . . . . 9
37		1le2 11241	. . . . . . . . . 10
38		nn0uz 11722	. . . . . . . . . . 11
39	19, 38	eleqtri 2699	. . . . . . . . . 10
40		leexp2a 12916	. . . . . . . . . 10 $/\$ $/\$
41	12, 37, 39, 40	mp3an 1424	. . . . . . . . 9
42	36, 41	eqbrtrri 4676	. . . . . . . 8
43		elnn0 11294	. . . . . . . . . 10 $\/$
44		nncn 11028	. . . . . . . . . . . . 13
45	44	exp1d 13003	. . . . . . . . . . . 12
46		nnge1 11046	. . . . . . . . . . . . 13
47		nnuz 11723	. . . . . . . . . . . . . . 15
48	28, 47	eleqtri 2699	. . . . . . . . . . . . . 14
49		leexp2a 12916	. . . . . . . . . . . . . 14 $/\$ $/\$
50	24, 48, 49	mp3an13 1415	. . . . . . . . . . . . 13
51	46, 50	syl 17	. . . . . . . . . . . 12
52	45, 51	eqbrtrrd 4677	. . . . . . . . . . 11
53	30	nn0ge0i 11320	. . . . . . . . . . . 12
54		breq1 4656	. . . . . . . . . . . 12
55	53, 54	mpbiri 248	. . . . . . . . . . 11
56	52, 55	jaoi 394	. . . . . . . . . 10 $\/$
57	43, 56	sylbi 207	. . . . . . . . 9
58	23, 57	ax-mp 5	. . . . . . . 8
59	42, 58	pm3.2i 471	. . . . . . 7 $/\$
60		lemul12a 10881	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	33, 59, 60	mp2 9	. . . . . 6
62		oveq1 6657	. . . . . . . . 9
63	16	nnzi 11401	. . . . . . . . . 10
64		1exp 12889	. . . . . . . . . 10
65	63, 64	ax-mp 5	. . . . . . . . 9
66	62, 65	syl6eq 2672	. . . . . . . 8
67		oveq2 6658	. . . . . . . . 9
68	23	nn0cni 11304	. . . . . . . . . 10
69		exp1 12866	. . . . . . . . . 10
70	68, 69	ax-mp 5	. . . . . . . . 9
71	67, 70	syl6eq 2672	. . . . . . . 8
72	66, 71	oveq12d 6668	. . . . . . 7
73		fveq2 6191	. . . . . . . . . 10
74		fac1 13064	. . . . . . . . . 10
75	73, 74	syl6eq 2672	. . . . . . . . 9
76	75	oveq2d 6666	. . . . . . . 8
77	21	recni 10052	. . . . . . . . . 10
78	30	nn0cni 11304	. . . . . . . . . 10
79	77, 78	mulcli 10045	. . . . . . . . 9
80	79	mulid1i 10042	. . . . . . . 8
81	76, 80	syl6eq 2672	. . . . . . 7
82	72, 81	breq12d 4666	. . . . . 6
83	61, 82	mpbiri 248	. . . . 5
84	9, 83	sylbir 225	. . . 4
85	84	adantr 481	. . 3 $/\$
86		reexpcl 12877	. . . . . . . 8 $/\$
87	2, 17, 86	mp2an 708	. . . . . . 7
88	1	nnnn0i 11300	. . . . . . . 8
89		reexpcl 12877	. . . . . . . 8 $/\$
90	24, 88, 89	mp2an 708	. . . . . . 7
91	87, 90	remulcli 10054	. . . . . 6
92	91	a1i 11	. . . . 5 $/\$
93	13, 18	nn0expcli 12886	. . . . . . . . 9
94		reexpcl 12877	. . . . . . . . 9 $/\$
95	12, 93, 94	mp2an 708	. . . . . . . 8
96	18, 13	nn0expcli 12886	. . . . . . . . 9
97	96	nn0rei 11303	. . . . . . . 8
98	95, 97	remulcli 10054	. . . . . . 7
99		faccl 13070	. . . . . . . . . . 11
100	88, 99	ax-mp 5	. . . . . . . . . 10
101	100	nnnn0i 11300	. . . . . . . . 9
102	30, 101	nn0mulcli 11331	. . . . . . . 8
103	102	nn0rei 11303	. . . . . . 7
104	98, 103	remulcli 10054	. . . . . 6
105	104	a1i 11	. . . . 5 $/\$
106	21, 103	remulcli 10054	. . . . . 6
107	106	a1i 11	. . . . 5 $/\$
108	1	nncni 11030	. . . . . . . . 9
109		expp1 12867	. . . . . . . . 9 $/\$
110	108, 13, 109	mp2an 708	. . . . . . . 8
111		expm1t 12888	. . . . . . . . 9 $/\$
112	68, 1, 111	mp2an 708	. . . . . . . 8
113	110, 112	oveq12i 6662	. . . . . . 7
114		reexpcl 12877	. . . . . . . . . 10 $/\$
115	2, 13, 114	mp2an 708	. . . . . . . . 9
116	115	recni 10052	. . . . . . . 8
117		elnnnn0 11336	. . . . . . . . . . . . 13 $/\$
118	1, 117	mpbi 220	. . . . . . . . . . . 12 $/\$
119	118	simpri 478	. . . . . . . . . . 11
120	23, 119	nn0expcli 12886	. . . . . . . . . 10
121	120, 23	nn0mulcli 11331	. . . . . . . . 9
122	121	nn0cni 11304	. . . . . . . 8
123	116, 108, 122	mulassi 10049	. . . . . . 7
124	113, 123	eqtri 2644	. . . . . 6
125	88, 121	nn0mulcli 11331	. . . . . . . . . . 11
126	125	nn0rei 11303	. . . . . . . . . 10
127	115, 126	remulcli 10054	. . . . . . . . 9
128	127	a1i 11	. . . . . . . 8 $/\$
129	119	nn0rei 11303	. . . . . . . . . . . 12
130		reexpcl 12877	. . . . . . . . . . . 12 $/\$
131	129, 13, 130	mp2an 708	. . . . . . . . . . 11
132	120	nn0rei 11303	. . . . . . . . . . 11
133	131, 132	remulcli 10054	. . . . . . . . . 10
134	96, 88	nn0mulcli 11331	. . . . . . . . . . . 12
135	134, 23	nn0mulcli 11331	. . . . . . . . . . 11
136	135	nn0rei 11303	. . . . . . . . . 10
137	133, 136	remulcli 10054	. . . . . . . . 9
138	137	a1i 11	. . . . . . . 8 $/\$
139	23, 13	nn0addcli 11330	. . . . . . . . . . . . 13
140		reexpcl 12877	. . . . . . . . . . . . 13 $/\$
141	24, 139, 140	mp2an 708	. . . . . . . . . . . 12
142	95, 141	remulcli 10054	. . . . . . . . . . 11
143		faccl 13070	. . . . . . . . . . . . 13
144	119, 143	ax-mp 5	. . . . . . . . . . . 12
145	144	nnrei 11029	. . . . . . . . . . 11
146	142, 145	remulcli 10054	. . . . . . . . . 10
147	146, 136	remulcli 10054	. . . . . . . . 9
148	147	a1i 11	. . . . . . . 8 $/\$
149	97, 131	remulcli 10054	. . . . . . . . . . . 12
150	125	nn0ge0i 11320	. . . . . . . . . . . . 13
151	126, 150	pm3.2i 471	. . . . . . . . . . . 12 $/\$
152	115, 149, 151	3pm3.2i 1239	. . . . . . . . . . 11 $/\$ $/\$ $/\$
153		nnltp1le 11433	. . . . . . . . . . . . . 14 $/\$
154	14, 1, 153	mp2an 708	. . . . . . . . . . . . 13
155		df-2 11079	. . . . . . . . . . . . . 14
156	155	breq1i 4660	. . . . . . . . . . . . 13
157	154, 156	bitr4i 267	. . . . . . . . . . . 12
158		expubnd 12921	. . . . . . . . . . . . 13 $/\$ $/\$
159	2, 13, 158	mp3an12 1414	. . . . . . . . . . . 12
160	157, 159	sylbi 207	. . . . . . . . . . 11
161		lemul1a 10877	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
162	152, 160, 161	sylancr 695	. . . . . . . . . 10
163	96	nn0cni 11304	. . . . . . . . . . . 12
164	131	recni 10052	. . . . . . . . . . . 12
165	163, 164, 108, 122	mul4i 10233	. . . . . . . . . . 11
166	120	nn0cni 11304	. . . . . . . . . . . . 13
167	164, 166, 68	mulassi 10049	. . . . . . . . . . . 12
168	167	oveq2i 6661	. . . . . . . . . . 11
169	134	nn0cni 11304	. . . . . . . . . . . 12
170	133	recni 10052	. . . . . . . . . . . 12
171	169, 170, 68	mul12i 10231	. . . . . . . . . . 11
172	165, 168, 171	3eqtr2i 2650	. . . . . . . . . 10
173	162, 172	syl6breq 4694	. . . . . . . . 9
174	173	adantr 481	. . . . . . . 8 $/\$
175	135	nn0ge0i 11320	. . . . . . . . . . . 12
176	136, 175	pm3.2i 471	. . . . . . . . . . 11 $/\$
177	133, 146, 176	3pm3.2i 1239	. . . . . . . . . 10 $/\$ $/\$ $/\$
178		lemul1a 10877	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
179	177, 178	mpan 706	. . . . . . . . 9
180	179	adantl 482	. . . . . . . 8 $/\$
181	128, 138, 148, 174, 180	letrd 10194	. . . . . . 7 $/\$
182	163, 108, 68	mul32i 10232	. . . . . . . . 9
183	182	oveq2i 6661	. . . . . . . 8
184		expp1 12867	. . . . . . . . . . . . . 14 $/\$
185	68, 139, 184	mp2an 708	. . . . . . . . . . . . 13
186	13	nn0cni 11304	. . . . . . . . . . . . . . 15
187		ax-1cn 9994	. . . . . . . . . . . . . . 15
188	68, 186, 187	addassi 10048	. . . . . . . . . . . . . 14
189	188	oveq2i 6661	. . . . . . . . . . . . 13
190	185, 189	eqtr3i 2646	. . . . . . . . . . . 12
191	190	oveq2i 6661	. . . . . . . . . . 11
192	95	recni 10052	. . . . . . . . . . . 12
193	141	recni 10052	. . . . . . . . . . . 12
194	192, 163, 193, 68	mul4i 10233	. . . . . . . . . . 11
195	191, 194	eqtr3i 2646	. . . . . . . . . 10
196		facnn2 13069	. . . . . . . . . . 11
197	1, 196	ax-mp 5	. . . . . . . . . 10
198	195, 197	oveq12i 6662	. . . . . . . . 9
199	142	recni 10052	. . . . . . . . . 10
200	144	nncni 11030	. . . . . . . . . 10
201	163, 68	mulcli 10045	. . . . . . . . . 10
202	199, 200, 201, 108	mul4i 10233	. . . . . . . . 9
203	198, 202	eqtr4i 2647	. . . . . . . 8
204	98	recni 10052	. . . . . . . . 9
205	100	nncni 11030	. . . . . . . . 9
206	204, 78, 205	mulassi 10049	. . . . . . . 8
207	183, 203, 206	3eqtr2i 2650	. . . . . . 7
208	181, 207	syl6breq 4694	. . . . . 6 $/\$
209	124, 208	syl5eqbr 4688	. . . . 5 $/\$
210	102	nn0ge0i 11320	. . . . . . . . 9
211	103, 210	pm3.2i 471	. . . . . . . 8 $/\$
212	98, 21, 211	3pm3.2i 1239	. . . . . . 7 $/\$ $/\$ $/\$
213		expadd 12902	. . . . . . . . 9 $/\$ $/\$
214	34, 93, 13, 213	mp3an 1424	. . . . . . . 8
215	19	nn0zi 11402	. . . . . . . . . 10
216	13	nn0rei 11303	. . . . . . . . . . . . 13
217	16	nnrei 11029	. . . . . . . . . . . . 13
218	17	nn0ge0i 11320	. . . . . . . . . . . . . 14
219	217, 218	pm3.2i 471	. . . . . . . . . . . . 13 $/\$
220	216, 217, 219	3pm3.2i 1239	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
221	216	ltp1i 10927	. . . . . . . . . . . . 13
222	216, 217, 221	ltleii 10160	. . . . . . . . . . . 12
223		lemul1a 10877	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
224	220, 222, 223	mp2an 708	. . . . . . . . . . 11
225	186	sqvali 12943	. . . . . . . . . . . . 13
226	186	mulid1i 10042	. . . . . . . . . . . . . 14
227	226	eqcomi 2631	. . . . . . . . . . . . 13
228	225, 227	oveq12i 6662	. . . . . . . . . . . 12
229	186, 186, 187	adddii 10050	. . . . . . . . . . . 12
230	228, 229	eqtr4i 2647	. . . . . . . . . . 11
231	16	nncni 11030	. . . . . . . . . . . 12
232	231	sqvali 12943	. . . . . . . . . . 11
233	224, 230, 232	3brtr4i 4683	. . . . . . . . . 10
234	93, 13	nn0addcli 11330	. . . . . . . . . . . 12
235	234	nn0zi 11402	. . . . . . . . . . 11
236	235	eluz1i 11695	. . . . . . . . . 10 $/\$
237	215, 233, 236	mpbir2an 955	. . . . . . . . 9
238		leexp2a 12916	. . . . . . . . 9 $/\$ $/\$
239	12, 37, 237, 238	mp3an 1424	. . . . . . . 8
240	214, 239	eqbrtrri 4676	. . . . . . 7
241		lemul1a 10877	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
242	212, 240, 241	mp2an 708	. . . . . 6
243	242	a1i 11	. . . . 5 $/\$
244	92, 105, 107, 209, 243	letrd 10194	. . . 4 $/\$
245	77, 78, 205	mulassi 10049	. . . 4
246	244, 245	syl6breqr 4695	. . 3 $/\$
247	85, 246	jaoian 824	. 2 $\/$ $/\$
248	5, 247	mpan 706	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990 class class class wbr 4653

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

cexp 12860

cfa 13060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-seq 12802 df-exp 12861 df-fac 13061

This theorem is referenced by: faclbnd4lem2 13081

W3C validator