faclbnd - Metamath Proof Explorer

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

Theorem faclbnd 11536

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)

**Assertion**
Ref	Expression
faclbnd	$/\$

Proof of Theorem faclbnd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnn0 10179	. 2 $\/$
2		oveq1 6047	. . . . . . . 8
3	2	oveq2d 6056	. . . . . . 7
4		fveq2 5687	. . . . . . . 8
5	4	oveq2d 6056	. . . . . . 7
6	3, 5	breq12d 4185	. . . . . 6
7	6	imbi2d 308	. . . . 5
8		oveq1 6047	. . . . . . . 8
9	8	oveq2d 6056	. . . . . . 7
10		fveq2 5687	. . . . . . . 8
11	10	oveq2d 6056	. . . . . . 7
12	9, 11	breq12d 4185	. . . . . 6
13	12	imbi2d 308	. . . . 5
14		oveq1 6047	. . . . . . . 8
15	14	oveq2d 6056	. . . . . . 7
16		fveq2 5687	. . . . . . . 8
17	16	oveq2d 6056	. . . . . . 7
18	15, 17	breq12d 4185	. . . . . 6
19	18	imbi2d 308	. . . . 5
20		oveq1 6047	. . . . . . . 8
21	20	oveq2d 6056	. . . . . . 7
22		fveq2 5687	. . . . . . . 8
23	22	oveq2d 6056	. . . . . . 7
24	21, 23	breq12d 4185	. . . . . 6
25	24	imbi2d 308	. . . . 5
26		nnre 9963	. . . . . . 7
27		nnge1 9982	. . . . . . 7
28		elnnuz 10478	. . . . . . . 8
29	28	biimpi 187	. . . . . . 7
30	26, 27, 29	leexp2ad 11510	. . . . . 6
31		0p1e1 10049	. . . . . . . 8
32	31	oveq2i 6051	. . . . . . 7
33	32	a1i 11	. . . . . 6
34		fac0 11524	. . . . . . . 8
35	34	oveq2i 6051	. . . . . . 7
36		nnnn0 10184	. . . . . . . . . 10
37	26, 36	reexpcld 11495	. . . . . . . . 9
38	37	recnd 9070	. . . . . . . 8
39	38	mulid1d 9061	. . . . . . 7
40	35, 39	syl5eq 2448	. . . . . 6
41	30, 33, 40	3brtr4d 4202	. . . . 5
42	26	ad3antrrr 711	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 736	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 10216	. . . . . . . . . . . . . . 15
45	43, 44	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 11495	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 711	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 11495	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49		faccl 11531	. . . . . . . . . . . . . . . 16
50	43, 49	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	nnred 9971	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
52	48, 51	remulcld 9072	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		nn0re 10186	. . . . . . . . . . . . . 14
54		peano2re 9195	. . . . . . . . . . . . . 14
55	43, 53, 54	3syl 19	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
56		nngt0 9985	. . . . . . . . . . . . . . . 16
57	56	ad3antrrr 711	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
58		0re 9047	. . . . . . . . . . . . . . . 16
59		ltle 9119	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	mpan 652	. . . . . . . . . . . . . . 15
61	42, 57, 60	sylc 58	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
62	42, 45, 61	expge0d 11496	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simplr 732	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64		simprr 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
65	46, 52, 42, 55, 62, 61, 63, 64	lemul12ad 9909	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	anandis 804	. . . . . . . . . . 11 $/\$ $/\$ $/\$
67		nncn 9964	. . . . . . . . . . . . 13
68		expp1 11343	. . . . . . . . . . . . 13 $/\$
69	67, 44, 68	syl2an 464	. . . . . . . . . . . 12 $/\$
70	69	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
71		facp1 11526	. . . . . . . . . . . . . . 15
72	71	adantl 453	. . . . . . . . . . . . . 14 $/\$
73	72	oveq2d 6056	. . . . . . . . . . . . 13 $/\$
74	38	adantr 452	. . . . . . . . . . . . . 14 $/\$
75	49	nncnd 9972	. . . . . . . . . . . . . . 15
76	75	adantl 453	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 10187	. . . . . . . . . . . . . . . 16
78		peano2cn 9194	. . . . . . . . . . . . . . . 16
79	77, 78	syl 16	. . . . . . . . . . . . . . 15
80	79	adantl 453	. . . . . . . . . . . . . 14 $/\$
81	74, 76, 80	mulassd 9067	. . . . . . . . . . . . 13 $/\$
82	73, 81	eqtr4d 2439	. . . . . . . . . . . 12 $/\$
83	82	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	66, 70, 83	3brtr4d 4202	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 589	. . . . . . . . 9 $/\$
86	85	com23 74	. . . . . . . 8 $/\$
87		nn0ltp1le 10288	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 465	. . . . . . . . . 10 $/\$
89		peano2nn0 10216	. . . . . . . . . . . . . . 15
90	44, 89	syl 16	. . . . . . . . . . . . . 14
91		reexpcl 11353	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 464	. . . . . . . . . . . . 13 $/\$
93	92	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$
95		faccl 11531	. . . . . . . . . . . . . . . 16
96	44, 95	syl 16	. . . . . . . . . . . . . . 15
97	96	nnred 9971	. . . . . . . . . . . . . 14
98		remulcl 9031	. . . . . . . . . . . . . 14 $/\$
99	37, 97, 98	syl2an 464	. . . . . . . . . . . . 13 $/\$
100	99	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
101	26	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$
102	27	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$
103		simpr 448	. . . . . . . . . . . . . 14 $/\$ $/\$
104	90	ad2antlr 708	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105	104	nn0zd 10329	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		nnz 10259	. . . . . . . . . . . . . . . 16
107	106	ad2antrr 707	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		eluz 10455	. . . . . . . . . . . . . . 15 $/\$
109	105, 107, 108	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$
110	103, 109	mpbird 224	. . . . . . . . . . . . 13 $/\$ $/\$
111	101, 102, 110	leexp2ad 11510	. . . . . . . . . . . 12 $/\$ $/\$
112	37, 97	anim12i 550	. . . . . . . . . . . . . 14 $/\$ $/\$
113		nn0re 10186	. . . . . . . . . . . . . . . . 17
114		id 20	. . . . . . . . . . . . . . . . 17
115		nn0ge0 10203	. . . . . . . . . . . . . . . . 17
116	113, 114, 115	expge0d 11496	. . . . . . . . . . . . . . . 16
117	36, 116	syl 16	. . . . . . . . . . . . . . 15
118	96	nnge1d 9998	. . . . . . . . . . . . . . 15
119	117, 118	anim12i 550	. . . . . . . . . . . . . 14 $/\$ $/\$
120		lemulge11 9828	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	112, 119, 120	syl2anc 643	. . . . . . . . . . . . 13 $/\$
122	121	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
123	93, 94, 100, 111, 122	letrd 9183	. . . . . . . . . . 11 $/\$ $/\$
124	123	ex 424	. . . . . . . . . 10 $/\$
125	88, 124	sylbid 207	. . . . . . . . 9 $/\$
126	125	a1dd 44	. . . . . . . 8 $/\$
127	53, 54	syl 16	. . . . . . . . 9
128		lelttric 9136	. . . . . . . . 9 $/\$ $\/$
129	26, 127, 128	syl2an 464	. . . . . . . 8 $/\$ $\/$
130	86, 126, 129	mpjaod 371	. . . . . . 7 $/\$
131	130	expcom 425	. . . . . 6
132	131	a2d 24	. . . . 5
133	7, 13, 19, 25, 41, 132	nn0ind 10322	. . . 4
134	133	impcom 420	. . 3 $/\$
135		faccl 11531	. . . . . . . 8
136	135	nnnn0d 10230	. . . . . . 7
137	136	nn0ge0d 10233	. . . . . 6
138		nn0p1nn 10215	. . . . . . 7
139	138	0expd 11494	. . . . . 6
140		0cn 9040	. . . . . . . . 9
141		exp0 11341	. . . . . . . . 9
142	140, 141	ax-mp 8	. . . . . . . 8
143	142	oveq1i 6050	. . . . . . 7
144	135	nncnd 9972	. . . . . . . 8
145	144	mulid2d 9062	. . . . . . 7
146	143, 145	syl5eq 2448	. . . . . 6
147	137, 139, 146	3brtr4d 4202	. . . . 5
148		oveq1 6047	. . . . . 6
149		oveq12 6049	. . . . . . . 8 $/\$
150	149	anidms 627	. . . . . . 7
151	150	oveq1d 6055	. . . . . 6
152	148, 151	breq12d 4185	. . . . 5
153	147, 152	syl5ibr 213	. . . 4
154	153	imp 419	. . 3 $/\$
155	134, 154	jaoian 760	. 2 $\/$ $/\$
156	1, 155	sylanb 459	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359

wceq 1649

wcel 1721 class class class wbr 4172

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cn 9956

cn0 10177

cz 10238

cuz 10444

cexp 11337

cfa 11521

This theorem is referenced by: faclbnd2 11537 faclbnd3 11538

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-seq 11279 df-exp 11338 df-fac 11522

W3C validator