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 !