Metamath Proof Explorer


Theorem facavg

Description: The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005)

Ref Expression
Assertion facavg M 0 N 0 M + N 2 ! M ! N !

Proof

Step Hyp Ref Expression
1 nn0readdcl M 0 N 0 M + N
2 1 rehalfcld M 0 N 0 M + N 2
3 flle M + N 2 M + N 2 M + N 2
4 2 3 syl M 0 N 0 M + N 2 M + N 2
5 reflcl M + N 2 M + N 2
6 2 5 syl M 0 N 0 M + N 2
7 nn0re M 0 M
8 7 adantr M 0 N 0 M
9 letr M + N 2 M + N 2 M M + N 2 M + N 2 M + N 2 M M + N 2 M
10 6 2 8 9 syl3anc M 0 N 0 M + N 2 M + N 2 M + N 2 M M + N 2 M
11 4 10 mpand M 0 N 0 M + N 2 M M + N 2 M
12 nn0addcl M 0 N 0 M + N 0
13 12 nn0ge0d M 0 N 0 0 M + N
14 halfnneg2 M + N 0 M + N 0 M + N 2
15 1 14 syl M 0 N 0 0 M + N 0 M + N 2
16 13 15 mpbid M 0 N 0 0 M + N 2
17 flge0nn0 M + N 2 0 M + N 2 M + N 2 0
18 2 16 17 syl2anc M 0 N 0 M + N 2 0
19 simpl M 0 N 0 M 0
20 facwordi M + N 2 0 M 0 M + N 2 M M + N 2 ! M !
21 20 3exp M + N 2 0 M 0 M + N 2 M M + N 2 ! M !
22 18 19 21 sylc M 0 N 0 M + N 2 M M + N 2 ! M !
23 faccl M 0 M !
24 23 nncnd M 0 M !
25 24 mulid1d M 0 M ! 1 = M !
26 25 adantr M 0 N 0 M ! 1 = M !
27 faccl N 0 N !
28 27 nnred N 0 N !
29 28 adantl M 0 N 0 N !
30 23 nnred M 0 M !
31 23 nnnn0d M 0 M ! 0
32 31 nn0ge0d M 0 0 M !
33 30 32 jca M 0 M ! 0 M !
34 33 adantr M 0 N 0 M ! 0 M !
35 27 nnge1d N 0 1 N !
36 35 adantl M 0 N 0 1 N !
37 1re 1
38 lemul2a 1 N ! M ! 0 M ! 1 N ! M ! 1 M ! N !
39 37 38 mp3anl1 N ! M ! 0 M ! 1 N ! M ! 1 M ! N !
40 29 34 36 39 syl21anc M 0 N 0 M ! 1 M ! N !
41 26 40 eqbrtrrd M 0 N 0 M ! M ! N !
42 18 faccld M 0 N 0 M + N 2 !
43 42 nnred M 0 N 0 M + N 2 !
44 30 adantr M 0 N 0 M !
45 remulcl M ! N ! M ! N !
46 30 28 45 syl2an M 0 N 0 M ! N !
47 letr M + N 2 ! M ! M ! N ! M + N 2 ! M ! M ! M ! N ! M + N 2 ! M ! N !
48 43 44 46 47 syl3anc M 0 N 0 M + N 2 ! M ! M ! M ! N ! M + N 2 ! M ! N !
49 41 48 mpan2d M 0 N 0 M + N 2 ! M ! M + N 2 ! M ! N !
50 11 22 49 3syld M 0 N 0 M + N 2 M M + N 2 ! M ! N !
51 nn0re N 0 N
52 51 adantl M 0 N 0 N
53 letr M + N 2 M + N 2 N M + N 2 M + N 2 M + N 2 N M + N 2 N
54 6 2 52 53 syl3anc M 0 N 0 M + N 2 M + N 2 M + N 2 N M + N 2 N
55 4 54 mpand M 0 N 0 M + N 2 N M + N 2 N
56 simpr M 0 N 0 N 0
57 facwordi M + N 2 0 N 0 M + N 2 N M + N 2 ! N !
58 57 3exp M + N 2 0 N 0 M + N 2 N M + N 2 ! N !
59 18 56 58 sylc M 0 N 0 M + N 2 N M + N 2 ! N !
60 27 nncnd N 0 N !
61 60 mulid2d N 0 1 N ! = N !
62 61 adantl M 0 N 0 1 N ! = N !
63 27 nnnn0d N 0 N ! 0
64 63 nn0ge0d N 0 0 N !
65 28 64 jca N 0 N ! 0 N !
66 65 adantl M 0 N 0 N ! 0 N !
67 23 nnge1d M 0 1 M !
68 67 adantr M 0 N 0 1 M !
69 lemul1a 1 M ! N ! 0 N ! 1 M ! 1 N ! M ! N !
70 37 69 mp3anl1 M ! N ! 0 N ! 1 M ! 1 N ! M ! N !
71 44 66 68 70 syl21anc M 0 N 0 1 N ! M ! N !
72 62 71 eqbrtrrd M 0 N 0 N ! M ! N !
73 letr M + N 2 ! N ! M ! N ! M + N 2 ! N ! N ! M ! N ! M + N 2 ! M ! N !
74 43 29 46 73 syl3anc M 0 N 0 M + N 2 ! N ! N ! M ! N ! M + N 2 ! M ! N !
75 72 74 mpan2d M 0 N 0 M + N 2 ! N ! M + N 2 ! M ! N !
76 55 59 75 3syld M 0 N 0 M + N 2 N M + N 2 ! M ! N !
77 avgle M N M + N 2 M M + N 2 N
78 7 51 77 syl2an M 0 N 0 M + N 2 M M + N 2 N
79 50 76 78 mpjaod M 0 N 0 M + N 2 ! M ! N !