Theorem facavgt 6907

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

Assertion

Ref	Expression
facavgt	|- ((M e. NN0 /\ N e. NN0) -> (!` (|_` ((M + N) / 2))) <_ ((!` M) x. (!` N)))

Proof of Theorem facavgt

Step	Hyp	Ref	Expression
1		avglet 6001	. . 3 |- ((M e. RR /\ N e. RR) -> (((M + N) / 2) <_ M \/ ((M + N) / 2) <_ N))
2		nn0ret 6065	. . 3 |- (M e. NN0 -> M e. RR)
3		nn0ret 6065	. . 3 |- (N e. NN0 -> N e. RR)
4	1, 2, 3	syl2an 454	. 2 |- ((M e. NN0 /\ N e. NN0) -> (((M + N) / 2) <_ M \/ ((M + N) / 2) <_ N))
5		nn0addclt 6077	. . . . . . . 8 |- ((M e. NN0 /\ N e. NN0) -> (M + N) e. NN0)
6		nn0ret 6065	. . . . . . . 8 |- ((M + N) e. NN0 -> (M + N) e. RR)
7	5, 6	syl 10	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> (M + N) e. RR)
8		rehalfclt 5991	. . . . . . 7 |- ((M + N) e. RR -> ((M + N) / 2) e. RR)
9		fllet 6187	. . . . . . 7 |- (((M + N) / 2) e. RR -> (|_` ((M + N) / 2)) <_ ((M + N) / 2))
10	7, 8, 9	3syl 20	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (|_` ((M + N) / 2)) <_ ((M + N) / 2))
11		letrt 5508	. . . . . . 7 |- (((|_` ((M + N) / 2)) e. RR /\ ((M + N) / 2) e. RR /\ M e. RR) -> (((|_` ((M + N) / 2)) <_ ((M + N) / 2) /\ ((M + N) / 2) <_ M) -> (|_` ((M + N) / 2)) <_ M))
12		flreclt 6185	. . . . . . . 8 |- (((M + N) / 2) e. RR -> (|_` ((M + N) / 2)) e. RR)
13	7, 8, 12	3syl 20	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> (|_` ((M + N) / 2)) e. RR)
14	5, 6, 8	3syl 20	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> ((M + N) / 2) e. RR)
15	2	adantr 389	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> M e. RR)
16	11, 13, 14, 15	syl3anc 857	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (((|_` ((M + N) / 2)) <_ ((M + N) / 2) /\ ((M + N) / 2) <_ M) -> (|_` ((M + N) / 2)) <_ M))
17	10, 16	mpand 700	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (((M + N) / 2) <_ M -> (|_` ((M + N) / 2)) <_ M))
18		facwordit 6896	. . . . . . 7 |- (((|_` ((M + N) / 2)) e. NN0 /\ M e. NN0 /\ (|_` ((M + N) / 2)) <_ M) -> (!` (|_` ((M + N) / 2))) <_ (!` M))
19	18	3exp 831	. . . . . 6 |- ((|_` ((M + N) / 2)) e. NN0 -> (M e. NN0 -> ((|_` ((M + N) / 2)) <_ M -> (!` (|_` ((M + N) / 2))) <_ (!` M))))
20		flge0nn0t 6197	. . . . . . 7 |- ((((M + N) / 2) e. RR /\ 0 <_ ((M + N) / 2)) -> (|_` ((M + N) / 2)) e. NN0)
21		nn0ge0t 6074	. . . . . . . . 9 |- ((M + N) e. NN0 -> 0 <_ (M + N))
22	5, 21	syl 10	. . . . . . . 8 |- ((M e. NN0 /\ N e. NN0) -> 0 <_ (M + N))
23		halfnneg2t 5995	. . . . . . . . 9 |- ((M + N) e. RR -> (0 <_ (M + N) <-> 0 <_ ((M + N) / 2)))
24	5, 6, 23	3syl 20	. . . . . . . 8 |- ((M e. NN0 /\ N e. NN0) -> (0 <_ (M + N) <-> 0 <_ ((M + N) / 2)))
25	22, 24	mpbid 195	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> 0 <_ ((M + N) / 2))
26	20, 14, 25	sylanc 471	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (|_` ((M + N) / 2)) e. NN0)
27		pm3.26 319	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> M e. NN0)
28	19, 26, 27	sylc 68	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> ((|_` ((M + N) / 2)) <_ M -> (!` (|_` ((M + N) / 2))) <_ (!` M)))
29	17, 28	syld 27	. . . 4 |- ((M e. NN0 /\ N e. NN0) -> (((M + N) / 2) <_ M -> (!` (|_` ((M + N) / 2))) <_ (!` M)))
30		facclt 6892	. . . . . . . 8 |- (M e. NN0 -> (!` M) e. NN)
31		nncnt 5888	. . . . . . . 8 |- ((!` M) e. NN -> (!` M) e. CC)
32		ax1id 5265	. . . . . . . 8 |- ((!` M) e. CC -> ((!` M) x. 1) = (!` M))
33	30, 31, 32	3syl 20	. . . . . . 7 |- (M e. NN0 -> ((!` M) x. 1) = (!` M))
34	33	adantr 389	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((!` M) x. 1) = (!` M))
35		1re 5418	. . . . . . . 8 |- 1 e. RR
36		lemul2itOLD 5806	. . . . . . . 8 |- (((1 e. RR /\ (!` N) e. RR /\ (!` M) e. RR) /\ (0 <_ (!` M) /\ 1 <_ (!` N))) -> ((!` M) x. 1) <_ ((!` M) x. (!` N)))
37	35, 36	mp3anl1 909	. . . . . . 7 |- ((((!` N) e. RR /\ (!` M) e. RR) /\ (0 <_ (!` M) /\ 1 <_ (!` N))) -> ((!` M) x. 1) <_ ((!` M) x. (!` N)))
38		facclt 6892	. . . . . . . . . 10 |- (N e. NN0 -> (!` N) e. NN)
39		nnret 5887	. . . . . . . . . 10 |- ((!` N) e. NN -> (!` N) e. RR)
40	38, 39	syl 10	. . . . . . . . 9 |- (N e. NN0 -> (!` N) e. RR)
41		nnret 5887	. . . . . . . . . 10 |- ((!` M) e. NN -> (!` M) e. RR)
42	30, 41	syl 10	. . . . . . . . 9 |- (M e. NN0 -> (!` M) e. RR)
43	40, 42	anim12i 333	. . . . . . . 8 |- ((N e. NN0 /\ M e. NN0) -> ((!` N) e. RR /\ (!` M) e. RR))
44	43	ancoms 436	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> ((!` N) e. RR /\ (!` M) e. RR))
45		nnnn0t 6063	. . . . . . . . 9 |- ((!` M) e. NN -> (!` M) e. NN0)
46		nn0ge0t 6074	. . . . . . . . 9 |- ((!` M) e. NN0 -> 0 <_ (!` M))
47	30, 45, 46	3syl 20	. . . . . . . 8 |- (M e. NN0 -> 0 <_ (!` M))
48		nnge1t 5901	. . . . . . . . 9 |- ((!` N) e. NN -> 1 <_ (!` N))
49	38, 48	syl 10	. . . . . . . 8 |- (N e. NN0 -> 1 <_ (!` N))
50	47, 49	anim12i 333	. . . . . . 7 |- ((M e. NN0 /\ N e. NN0) -> (0 <_ (!` M) /\ 1 <_ (!` N)))
51	37, 44, 50	sylanc 471	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((!` M) x. 1) <_ ((!` M) x. (!` N)))
52	34, 51	eqbrtrrd 2633	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (!` M) <_ ((!` M) x. (!` N)))
53		letrt 5508	. . . . . 6 |- (((!` (|_` ((M + N) / 2))) e. RR /\ (!` M) e. RR /\ ((!` M) x. (!` N)) e. RR) -> (((!` (|_` ((M + N) / 2))) <_ (!` M) /\ (!` M) <_ ((!` M) x. (!` N))) -> (!` (|_` ((M + N) / 2))) <_ ((!` M) x. (!` N))))
54		facclt 6892	. . . . . . 7 |- ((|_` ((M + N) / 2)) e. NN0 -> (!` (|_` ((M + N) / 2))) e. NN)
55		nnret 5887	. . . . . . 7 |- ((!` (|_` ((M + N) / 2))) e. NN -> (!` (|_` ((M + N) / 2))) e. RR)
56	26, 54, 55	3syl 20	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (!` (|_` ((M + N) / 2))) e. RR)
57	42	adantr 389	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (!` M) e. RR)
58		axmulrcl 5257	. . . . . . 7 |- (((!` M) e. RR /\ (!` N) e. RR) -> ((!` M) x. (!` N)) e. RR)
59	58, 42, 40	syl2an 454	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((!` M) x. (!` N)) e. RR)
60	53, 56, 57, 59	syl3anc 857	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (((!` (|_` ((M + N) / 2))) <_ (!` M) /\ (!` M) <_ ((!` M) x. (!` N))) -> (!` (|_` ((M + N) / 2))) <_ ((!` M)