faclbnd - Metamath Proof Explorer

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

Theorem faclbnd 12187

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 10696	. 2 $\/$
2		oveq1 6210	. . . . . . . 8
3	2	oveq2d 6219	. . . . . . 7
4		fveq2 5802	. . . . . . . 8
5	4	oveq2d 6219	. . . . . . 7
6	3, 5	breq12d 4416	. . . . . 6
7	6	imbi2d 316	. . . . 5
8		oveq1 6210	. . . . . . . 8
9	8	oveq2d 6219	. . . . . . 7
10		fveq2 5802	. . . . . . . 8
11	10	oveq2d 6219	. . . . . . 7
12	9, 11	breq12d 4416	. . . . . 6
13	12	imbi2d 316	. . . . 5
14		oveq1 6210	. . . . . . . 8
15	14	oveq2d 6219	. . . . . . 7
16		fveq2 5802	. . . . . . . 8
17	16	oveq2d 6219	. . . . . . 7
18	15, 17	breq12d 4416	. . . . . 6
19	18	imbi2d 316	. . . . 5
20		oveq1 6210	. . . . . . . 8
21	20	oveq2d 6219	. . . . . . 7
22		fveq2 5802	. . . . . . . 8
23	22	oveq2d 6219	. . . . . . 7
24	21, 23	breq12d 4416	. . . . . 6
25	24	imbi2d 316	. . . . 5
26		nnre 10444	. . . . . . 7
27		nnge1 10463	. . . . . . 7
28		elnnuz 11012	. . . . . . . 8
29	28	biimpi 194	. . . . . . 7
30	26, 27, 29	leexp2ad 12161	. . . . . 6
31		0p1e1 10548	. . . . . . . 8
32	31	oveq2i 6214	. . . . . . 7
33	32	a1i 11	. . . . . 6
34		fac0 12175	. . . . . . . 8
35	34	oveq2i 6214	. . . . . . 7
36		nnnn0 10701	. . . . . . . . . 10
37	26, 36	reexpcld 12146	. . . . . . . . 9
38	37	recnd 9527	. . . . . . . 8
39	38	mulid1d 9518	. . . . . . 7
40	35, 39	syl5eq 2507	. . . . . 6
41	30, 33, 40	3brtr4d 4433	. . . . 5
42	26	ad3antrrr 729	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 10735	. . . . . . . . . . . . . . 15
45	43, 44	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 12146	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 12146	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49		faccl 12182	. . . . . . . . . . . . . . . 16
50	43, 49	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	nnred 10452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
52	48, 51	remulcld 9529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		nn0re 10703	. . . . . . . . . . . . . 14
54		peano2re 9657	. . . . . . . . . . . . . 14
55	43, 53, 54	3syl 20	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
56		nngt0 10466	. . . . . . . . . . . . . . . 16
57	56	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
58		0re 9501	. . . . . . . . . . . . . . . 16
59		ltle 9578	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	mpan 670	. . . . . . . . . . . . . . 15
61	42, 57, 60	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
62	42, 45, 61	expge0d 12147	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simplr 754	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
65	46, 52, 42, 55, 62, 61, 63, 64	lemul12ad 10390	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	anandis 826	. . . . . . . . . . 11 $/\$ $/\$ $/\$
67		nncn 10445	. . . . . . . . . . . . 13
68		expp1 11993	. . . . . . . . . . . . 13 $/\$
69	67, 44, 68	syl2an 477	. . . . . . . . . . . 12 $/\$
70	69	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
71		facp1 12177	. . . . . . . . . . . . . . 15
72	71	adantl 466	. . . . . . . . . . . . . 14 $/\$
73	72	oveq2d 6219	. . . . . . . . . . . . 13 $/\$
74	38	adantr 465	. . . . . . . . . . . . . 14 $/\$
75	49	nncnd 10453	. . . . . . . . . . . . . . 15
76	75	adantl 466	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 10704	. . . . . . . . . . . . . . . 16
78		peano2cn 9656	. . . . . . . . . . . . . . . 16
79	77, 78	syl 16	. . . . . . . . . . . . . . 15
80	79	adantl 466	. . . . . . . . . . . . . 14 $/\$
81	74, 76, 80	mulassd 9524	. . . . . . . . . . . . 13 $/\$
82	73, 81	eqtr4d 2498	. . . . . . . . . . . 12 $/\$
83	82	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	66, 70, 83	3brtr4d 4433	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 605	. . . . . . . . 9 $/\$
86	85	com23 78	. . . . . . . 8 $/\$
87		nn0ltp1le 10817	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 478	. . . . . . . . . 10 $/\$
89		peano2nn0 10735	. . . . . . . . . . . . . . 15
90	44, 89	syl 16	. . . . . . . . . . . . . 14
91		reexpcl 12003	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 477	. . . . . . . . . . . . 13 $/\$
93	92	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$
95		faccl 12182	. . . . . . . . . . . . . . . 16
96	44, 95	syl 16	. . . . . . . . . . . . . . 15
97	96	nnred 10452	. . . . . . . . . . . . . 14
98		remulcl 9482	. . . . . . . . . . . . . 14 $/\$
99	37, 97, 98	syl2an 477	. . . . . . . . . . . . 13 $/\$
100	99	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
101	26	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
102	27	ad2antrr 725	. . . . . . . . . . . . 13 $/\$ $/\$
103		simpr 461	. . . . . . . . . . . . . 14 $/\$ $/\$
104	90	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105	104	nn0zd 10860	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		nnz 10783	. . . . . . . . . . . . . . . 16
107	106	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		eluz 10989	. . . . . . . . . . . . . . 15 $/\$
109	105, 107, 108	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$
110	103, 109	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
111	101, 102, 110	leexp2ad 12161	. . . . . . . . . . . 12 $/\$ $/\$
112	37, 97	anim12i 566	. . . . . . . . . . . . . 14 $/\$ $/\$
113		nn0re 10703	. . . . . . . . . . . . . . . . 17
114		id 22	. . . . . . . . . . . . . . . . 17
115		nn0ge0 10720	. . . . . . . . . . . . . . . . 17
116	113, 114, 115	expge0d 12147	. . . . . . . . . . . . . . . 16
117	36, 116	syl 16	. . . . . . . . . . . . . . 15
118	96	nnge1d 10479	. . . . . . . . . . . . . . 15
119	117, 118	anim12i 566	. . . . . . . . . . . . . 14 $/\$ $/\$
120		lemulge11 10306	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	112, 119, 120	syl2anc 661	. . . . . . . . . . . . 13 $/\$
122	121	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
123	93, 94, 100, 111, 122	letrd 9643	. . . . . . . . . . 11 $/\$ $/\$
124	123	ex 434	. . . . . . . . . 10 $/\$
125	88, 124	sylbid 215	. . . . . . . . 9 $/\$
126	125	a1dd 46	. . . . . . . 8 $/\$
127	53, 54	syl 16	. . . . . . . . 9
128		lelttric 9596	. . . . . . . . 9 $/\$ $\/$
129	26, 127, 128	syl2an 477	. . . . . . . 8 $/\$ $\/$
130	86, 126, 129	mpjaod 381	. . . . . . 7 $/\$
131	130	expcom 435	. . . . . 6
132	131	a2d 26	. . . . 5
133	7, 13, 19, 25, 41, 132	nn0ind 10853	. . . 4
134	133	impcom 430	. . 3 $/\$
135		faccl 12182	. . . . . . . 8
136	135	nnnn0d 10751	. . . . . . 7
137	136	nn0ge0d 10754	. . . . . 6
138		nn0p1nn 10734	. . . . . . 7
139	138	0expd 12145	. . . . . 6
140		0exp0e1 11991	. . . . . . . 8
141	140	oveq1i 6213	. . . . . . 7
142	135	nncnd 10453	. . . . . . . 8
143	142	mulid2d 9519	. . . . . . 7
144	141, 143	syl5eq 2507	. . . . . 6
145	137, 139, 144	3brtr4d 4433	. . . . 5
146		oveq1 6210	. . . . . 6
147		oveq12 6212	. . . . . . . 8 $/\$
148	147	anidms 645	. . . . . . 7
149	148	oveq1d 6218	. . . . . 6
150	146, 149	breq12d 4416	. . . . 5
151	145, 150	syl5ibr 221	. . . 4
152	151	imp 429	. . 3 $/\$
153	134, 152	jaoian 782	. 2 $\/$ $/\$
154	1, 153	sylanb 472	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1370

wcel 1758 class class class wbr 4403

cfv 5529 (class class class)co 6203

cc 9395

cr 9396

cc0 9397

c1 9398

caddc 9400

cmul 9402

clt 9533

cle 9534

cn 10437

cn0 10694

cz 10761

cuz 10976

cexp 11986

cfa 12172

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-cnex 9453 ax-resscn 9454 ax-1cn 9455 ax-icn 9456 ax-addcl 9457 ax-addrcl 9458 ax-mulcl 9459 ax-mulrcl 9460 ax-mulcom 9461 ax-addass 9462 ax-mulass 9463 ax-distr 9464 ax-i2m1 9465 ax-1ne0 9466 ax-1rid 9467 ax-rnegex 9468 ax-rrecex 9469 ax-cnre 9470 ax-pre-lttri 9471 ax-pre-lttrn 9472 ax-pre-ltadd 9473 ax-pre-mulgt0 9474

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rmo 2807 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-om 6590 df-2nd 6691 df-recs 6945 df-rdg 6979 df-er 7214 df-en 7424 df-dom 7425 df-sdom 7426 df-pnf 9535 df-mnf 9536 df-xr 9537 df-ltxr 9538 df-le 9539 df-sub 9712 df-neg 9713 df-div 10109 df-nn 10438 df-n0 10695 df-z 10762 df-uz 10977 df-rp 11107 df-seq 11928 df-exp 11987 df-fac 12173

This theorem is referenced by: faclbnd2 12188 faclbnd3 12189

W3C validator