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+N2!≤M!⁢N!

Proof

Step Hyp Ref Expression
1 nn0readdcl ⊢M∈ℕ0∧N∈ℕ0→M+N∈ℝ
2 1 rehalfcld ⊢M∈ℕ0∧N∈ℕ0→M+N2∈ℝ
3 flle ⊢M+N2∈ℝ→M+N2≤M+N2
4 2 3 syl ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M+N2
5 reflcl ⊢M+N2∈ℝ→M+N2∈ℝ
6 2 5 syl ⊢M∈ℕ0∧N∈ℕ0→M+N2∈ℝ
7 nn0re ⊢M∈ℕ0→M∈ℝ
8 7 adantr ⊢M∈ℕ0∧N∈ℕ0→M∈ℝ
9 letr ⊢M+N2∈ℝ∧M+N2∈ℝ∧M∈ℝ→M+N2≤M+N2∧M+N2≤M→M+N2≤M
10 6 2 8 9 syl3anc ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M+N2∧M+N2≤M→M+N2≤M
11 4 10 mpand ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M→M+N2≤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+N2
15 1 14 syl ⊢M∈ℕ0∧N∈ℕ0→0≤M+N↔0≤M+N2
16 13 15 mpbid ⊢M∈ℕ0∧N∈ℕ0→0≤M+N2
17 flge0nn0 ⊢M+N2∈ℝ∧0≤M+N2→M+N2∈ℕ0
18 2 16 17 syl2anc ⊢M∈ℕ0∧N∈ℕ0→M+N2∈ℕ0
19 simpl ⊢M∈ℕ0∧N∈ℕ0→M∈ℕ0
20 facwordi ⊢M+N2∈ℕ0∧M∈ℕ0∧M+N2≤M→M+N2!≤M!
21 20 3exp ⊢M+N2∈ℕ0→M∈ℕ0→M+N2≤M→M+N2!≤M!
22 18 19 21 sylc ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M→M+N2!≤M!
23 faccl ⊢M∈ℕ0→M!∈ℕ
24 23 nncnd ⊢M∈ℕ0→M!∈ℂ
25 24 mulridd ⊢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+N2!∈ℕ
43 42 nnred ⊢M∈ℕ0∧N∈ℕ0→M+N2!∈ℝ
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+N2!∈ℝ∧M!∈ℝ∧M!⁢N!∈ℝ→M+N2!≤M!∧M!≤M!⁢N!→M+N2!≤M!⁢N!
48 43 44 46 47 syl3anc ⊢M∈ℕ0∧N∈ℕ0→M+N2!≤M!∧M!≤M!⁢N!→M+N2!≤M!⁢N!
49 41 48 mpan2d ⊢M∈ℕ0∧N∈ℕ0→M+N2!≤M!→M+N2!≤M!⁢N!
50 11 22 49 3syld ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M→M+N2!≤M!⁢N!
51 nn0re ⊢N∈ℕ0→N∈ℝ
52 51 adantl ⊢M∈ℕ0∧N∈ℕ0→N∈ℝ
53 letr ⊢M+N2∈ℝ∧M+N2∈ℝ∧N∈ℝ→M+N2≤M+N2∧M+N2≤N→M+N2≤N
54 6 2 52 53 syl3anc ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M+N2∧M+N2≤N→M+N2≤N
55 4 54 mpand ⊢M∈ℕ0∧N∈ℕ0→M+N2≤N→M+N2≤N
56 simpr ⊢M∈ℕ0∧N∈ℕ0→N∈ℕ0
57 facwordi ⊢M+N2∈ℕ0∧N∈ℕ0∧M+N2≤N→M+N2!≤N!
58 57 3exp ⊢M+N2∈ℕ0→N∈ℕ0→M+N2≤N→M+N2!≤N!
59 18 56 58 sylc ⊢M∈ℕ0∧N∈ℕ0→M+N2≤N→M+N2!≤N!
60 27 nncnd ⊢N∈ℕ0→N!∈ℂ
61 60 mullidd ⊢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+N2!∈ℝ∧N!∈ℝ∧M!⁢N!∈ℝ→M+N2!≤N!∧N!≤M!⁢N!→M+N2!≤M!⁢N!
74 43 29 46 73 syl3anc ⊢M∈ℕ0∧N∈ℕ0→M+N2!≤N!∧N!≤M!⁢N!→M+N2!≤M!⁢N!
75 72 74 mpan2d ⊢M∈ℕ0∧N∈ℕ0→M+N2!≤N!→M+N2!≤M!⁢N!
76 55 59 75 3syld ⊢M∈ℕ0∧N∈ℕ0→M+N2≤N→M+N2!≤M!⁢N!
77 avgle ⊢M∈ℝ∧N∈ℝ→M+N2≤M∨M+N2≤N
78 7 51 77 syl2an ⊢M∈ℕ0∧N∈ℕ0→M+N2≤M∨M+N2≤N
79 50 76 78 mpjaod ⊢M∈ℕ0∧N∈ℕ0→M+N2!≤M!⁢N!