faclbnd - Metamath Proof Explorer

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

Theorem faclbnd 12410

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 10837	. 2 $\/$
2		oveq1 6284	. . . . . . . 8
3	2	oveq2d 6293	. . . . . . 7
4		fveq2 5848	. . . . . . . 8
5	4	oveq2d 6293	. . . . . . 7
6	3, 5	breq12d 4407	. . . . . 6
7	6	imbi2d 314	. . . . 5
8		oveq1 6284	. . . . . . . 8
9	8	oveq2d 6293	. . . . . . 7
10		fveq2 5848	. . . . . . . 8
11	10	oveq2d 6293	. . . . . . 7
12	9, 11	breq12d 4407	. . . . . 6
13	12	imbi2d 314	. . . . 5
14		oveq1 6284	. . . . . . . 8
15	14	oveq2d 6293	. . . . . . 7
16		fveq2 5848	. . . . . . . 8
17	16	oveq2d 6293	. . . . . . 7
18	15, 17	breq12d 4407	. . . . . 6
19	18	imbi2d 314	. . . . 5
20		oveq1 6284	. . . . . . . 8
21	20	oveq2d 6293	. . . . . . 7
22		fveq2 5848	. . . . . . . 8
23	22	oveq2d 6293	. . . . . . 7
24	21, 23	breq12d 4407	. . . . . 6
25	24	imbi2d 314	. . . . 5
26		nnre 10582	. . . . . . 7
27		nnge1 10601	. . . . . . 7
28		elnnuz 11162	. . . . . . . 8
29	28	biimpi 194	. . . . . . 7
30	26, 27, 29	leexp2ad 12384	. . . . . 6
31		0p1e1 10687	. . . . . . . 8
32	31	oveq2i 6288	. . . . . . 7
33	32	a1i 11	. . . . . 6
34		fac0 12398	. . . . . . . 8
35	34	oveq2i 6288	. . . . . . 7
36		nnnn0 10842	. . . . . . . . . 10
37	26, 36	reexpcld 12369	. . . . . . . . 9
38	37	recnd 9651	. . . . . . . 8
39	38	mulid1d 9642	. . . . . . 7
40	35, 39	syl5eq 2455	. . . . . 6
41	30, 33, 40	3brtr4d 4424	. . . . 5
42	26	ad3antrrr 728	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 761	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 10876	. . . . . . . . . . . . . . 15
45	43, 44	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 12369	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 12369	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49		faccl 12405	. . . . . . . . . . . . . . . 16
50	43, 49	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	nnred 10590	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
52	48, 51	remulcld 9653	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		nn0re 10844	. . . . . . . . . . . . . 14
54		peano2re 9786	. . . . . . . . . . . . . 14
55	43, 53, 54	3syl 20	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
56		nngt0 10604	. . . . . . . . . . . . . . . 16
57	56	ad3antrrr 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
58		0re 9625	. . . . . . . . . . . . . . . 16
59		ltle 9703	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	mpan 668	. . . . . . . . . . . . . . 15
61	42, 57, 60	sylc 59	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
62	42, 45, 61	expge0d 12370	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simplr 754	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64		simprr 758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
65	46, 52, 42, 55, 62, 61, 63, 64	lemul12ad 10527	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	anandis 831	. . . . . . . . . . 11 $/\$ $/\$ $/\$
67		nncn 10583	. . . . . . . . . . . . 13
68		expp1 12215	. . . . . . . . . . . . 13 $/\$
69	67, 44, 68	syl2an 475	. . . . . . . . . . . 12 $/\$
70	69	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
71		facp1 12400	. . . . . . . . . . . . . . 15
72	71	adantl 464	. . . . . . . . . . . . . 14 $/\$
73	72	oveq2d 6293	. . . . . . . . . . . . 13 $/\$
74	38	adantr 463	. . . . . . . . . . . . . 14 $/\$
75	49	nncnd 10591	. . . . . . . . . . . . . . 15
76	75	adantl 464	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 10845	. . . . . . . . . . . . . . . 16
78		peano2cn 9785	. . . . . . . . . . . . . . . 16
79	77, 78	syl 17	. . . . . . . . . . . . . . 15
80	79	adantl 464	. . . . . . . . . . . . . 14 $/\$
81	74, 76, 80	mulassd 9648	. . . . . . . . . . . . 13 $/\$
82	73, 81	eqtr4d 2446	. . . . . . . . . . . 12 $/\$
83	82	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	66, 70, 83	3brtr4d 4424	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 603	. . . . . . . . 9 $/\$
86	85	com23 78	. . . . . . . 8 $/\$
87		nn0ltp1le 10961	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 476	. . . . . . . . . 10 $/\$
89		peano2nn0 10876	. . . . . . . . . . . . . . 15
90	44, 89	syl 17	. . . . . . . . . . . . . 14
91		reexpcl 12225	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 475	. . . . . . . . . . . . 13 $/\$
93	92	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 724	. . . . . . . . . . . 12 $/\$ $/\$
95		faccl 12405	. . . . . . . . . . . . . . . 16
96	44, 95	syl 17	. . . . . . . . . . . . . . 15
97	96	nnred 10590	. . . . . . . . . . . . . 14
98		remulcl 9606	. . . . . . . . . . . . . 14 $/\$
99	37, 97, 98	syl2an 475	. . . . . . . . . . . . 13 $/\$
100	99	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
101	26	ad2antrr 724	. . . . . . . . . . . . 13 $/\$ $/\$
102	27	ad2antrr 724	. . . . . . . . . . . . 13 $/\$ $/\$
103		simpr 459	. . . . . . . . . . . . . 14 $/\$ $/\$
104	90	ad2antlr 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105	104	nn0zd 11005	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		nnz 10926	. . . . . . . . . . . . . . . 16
107	106	ad2antrr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		eluz 11139	. . . . . . . . . . . . . . 15 $/\$
109	105, 107, 108	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$
110	103, 109	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
111	101, 102, 110	leexp2ad 12384	. . . . . . . . . . . 12 $/\$ $/\$
112	37, 97	anim12i 564	. . . . . . . . . . . . . 14 $/\$ $/\$
113		nn0re 10844	. . . . . . . . . . . . . . . . 17
114		id 22	. . . . . . . . . . . . . . . . 17
115		nn0ge0 10861	. . . . . . . . . . . . . . . . 17
116	113, 114, 115	expge0d 12370	. . . . . . . . . . . . . . . 16
117	36, 116	syl 17	. . . . . . . . . . . . . . 15
118	96	nnge1d 10618	. . . . . . . . . . . . . . 15
119	117, 118	anim12i 564	. . . . . . . . . . . . . 14 $/\$ $/\$
120		lemulge11 10444	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	112, 119, 120	syl2anc 659	. . . . . . . . . . . . 13 $/\$
122	121	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
123	93, 94, 100, 111, 122	letrd 9772	. . . . . . . . . . 11 $/\$ $/\$
124	123	ex 432	. . . . . . . . . 10 $/\$
125	88, 124	sylbid 215	. . . . . . . . 9 $/\$
126	125	a1dd 44	. . . . . . . 8 $/\$
127	53, 54	syl 17	. . . . . . . . 9
128		lelttric 9722	. . . . . . . . 9 $/\$ $\/$
129	26, 127, 128	syl2an 475	. . . . . . . 8 $/\$ $\/$
130	86, 126, 129	mpjaod 379	. . . . . . 7 $/\$
131	130	expcom 433	. . . . . 6
132	131	a2d 26	. . . . 5
133	7, 13, 19, 25, 41, 132	nn0ind 10997	. . . 4
134	133	impcom 428	. . 3 $/\$
135		faccl 12405	. . . . . . . 8
136	135	nnnn0d 10892	. . . . . . 7
137	136	nn0ge0d 10895	. . . . . 6
138		nn0p1nn 10875	. . . . . . 7
139	138	0expd 12368	. . . . . 6
140		0exp0e1 12213	. . . . . . . 8
141	140	oveq1i 6287	. . . . . . 7
142	135	nncnd 10591	. . . . . . . 8
143	142	mulid2d 9643	. . . . . . 7
144	141, 143	syl5eq 2455	. . . . . 6
145	137, 139, 144	3brtr4d 4424	. . . . 5
146		oveq1 6284	. . . . . 6
147		oveq12 6286	. . . . . . . 8 $/\$
148	147	anidms 643	. . . . . . 7
149	148	oveq1d 6292	. . . . . 6
150	146, 149	breq12d 4407	. . . . 5
151	145, 150	syl5ibr 221	. . . 4
152	151	imp 427	. . 3 $/\$
153	134, 152	jaoian 785	. 2 $\/$ $/\$
154	1, 153	sylanb 470	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1405

wcel 1842 class class class wbr 4394

cfv 5568 (class class class)co 6277

cc 9519

cr 9520

cc0 9521

c1 9522

caddc 9524

cmul 9526

clt 9657

cle 9658

cn 10575

cn0 10835

cz 10904

cuz 11126

cexp 12208

cfa 12395

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6683 df-2nd 6784 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-er 7347 df-en 7554 df-dom 7555 df-sdom 7556 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-div 10247 df-nn 10576 df-n0 10836 df-z 10905 df-uz 11127 df-rp 11265 df-seq 12150 df-exp 12209 df-fac 12396

This theorem is referenced by: faclbnd2 12411 faclbnd3 12412

W3C validator