Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem facavgt 6892

Description: The product of two factorials is greater than or equal to the factorial of (the floor of) their average.

Assertion

Ref	Expression
facavgt

---

Proof of Theorem facavgt

Step	Hyp	Ref	Expression
1		avglet 5991	. . 3
2		nn0ret 6055	. . 3
3		nn0ret 6055	. . 3
4	1, 2, 3	syl2an 454	. 2
5		nn0addclt 6067	. . . . . . . 8
6		nn0ret 6055	. . . . . . . 8
7	5, 6	syl 10	. . . . . . 7
8		rehalfclt 5981	. . . . . . 7
9		fllet 6176	. . . . . . 7
10	7, 8, 9	3syl 20	. . . . . 6
11		letrt 5498	. . . . . . 7
12		flclt 6174	. . . . . . . . 9
13		zret 6086	. . . . . . . . 9
14	12, 13	syl 10	. . . . . . . 8
15	7, 8, 14	3syl 20	. . . . . . 7
16	5, 6, 8	3syl 20	. . . . . . 7
17	2	adantr 389	. . . . . . 7
18	11, 15, 16, 17	syl3anc 856	. . . . . 6
19	10, 18	mpand 699	. . . . 5
20		facwordit 6881	. . . . . . 7
21	20	3exp 830	. . . . . 6
22		flge0nn0t 6185	. . . . . . 7
23		nn0ge0t 6064	. . . . . . . . 9
24	5, 23	syl 10	. . . . . . . 8
25		halfnneg2t 5985	. . . . . . . . 9
26	5, 6, 25	3syl 20	. . . . . . . 8
27	24, 26	mpbid 195	. . . . . . 7
28	22, 16, 27	sylanc 471	. . . . . 6
29		pm3.26 319	. . . . . 6
30	21, 28, 29	sylc 68	. . . . 5
31	19, 30	syld 27	. . . 4
32		facclt 6877	. . . . . . . 8
33		nncnt 5878	. . . . . . . 8
34		ax1id 5254	. . . . . . . 8
35	32, 33, 34	3syl 20	. . . . . . 7
36	35	adantr 389	. . . . . 6
37		1re 5407	. . . . . . . 8
38		lemul2itOLD 5796	. . . . . . . 8
39	37, 38	mp3anl1 907	. . . . . . 7
40		facclt 6877	. . . . . . . . . 10
41		nnret 5877	. . . . . . . . . 10
42	40, 41	syl 10	. . . . . . . . 9
43		nnret 5877	. . . . . . . . . 10
44	32, 43	syl 10	. . . . . . . . 9
45	42, 44	anim12i 333	. . . . . . . 8
46	45	ancoms 436	. . . . . . 7
47		nnnn0t 6053	. . . . . . . . 9
48		nn0ge0t 6064	. . . . . . . . 9
49	32, 47, 48	3syl 20	. . . . . . . 8
50		nnge1t 5891	. . . . . . . . 9
51	40, 50	syl 10	. . . . . . . 8
52	49, 51	anim12i 333	. . . . . . 7
53	39, 46, 52	sylanc 471	. . . . . 6
54	36, 53	eqbrtrrd 2627	. . . . 5
55		letrt 5498	. . . . . 6
56		facclt 6877	. . . . . . 7
57		nnret 5877	. . . . . . 7
58	28, 56, 57	3syl 20	. . . . . 6
59	44	adantr 389	. . . . . 6
60		axmulrcl 5246	. . . . . . 7
61	60, 44, 42	syl2an 454	. . . . . 6
62	55, 58, 59, 61	syl3anc 856	. . . . 5