Theorem efaddlem15 7352

Description: Lemma for efadd 7366. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 7343. The key theorem used is facavgt 6955, which says that the factorial of the average of two numbers is less than the product of their factorials.

Hypotheses

Ref	Expression
efaddlem15.1	|- N e. NN
efaddlem15.2	|- S = (|_` ((N + 1) / 2))

Assertion

Ref	Expression
efaddlem15	|- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` S) <_ ((!` j) x. (!` k)))

Proof of Theorem efaddlem15

Step	Hyp	Ref	Expression
1		efaddlem15.1	. . . . . . 7 |- N e. NN
2		efaddlem15.2	. . . . . . 7 |- S = (|_` ((N + 1) / 2))
3	1, 2	efaddlem8 7345	. . . . . 6 |- S e. NN
4	3	nnnn0 6107	. . . . 5 |- S e. NN0
5		facclt 6940	. . . . 5 |- (S e. NN0 -> (!` S) e. NN)
6	4, 5	ax-mp 7	. . . 4 |- (!` S) e. NN
7	6	nnre 5931	. . 3 |- (!` S) e. RR
8	7	a1i 8	. 2 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` S) e. RR)
9		nn0addclt 6120	. . . 4 |- ((j e. NN0 /\ k e. NN0) -> (j + k) e. NN0)
10		elfznnt 6494	. . . . . 6 |- (j e. (1...N) -> j e. NN)
11		nnnn0t 6106	. . . . . 6 |- (j e. NN -> j e. NN0)
12	10, 11	syl 10	. . . . 5 |- (j e. (1...N) -> j e. NN0)
13	12	adantr 389	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN0)
14	1	efaddlem2 7339	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN)
15		nnnn0t 6106	. . . . 5 |- (k e. NN -> k e. NN0)
16	14, 15	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN0)
17	9, 13, 16	sylanc 471	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (j + k) e. NN0)
18		flge0nn0t 6242	. . . . . 6 |- ((((j + k) / 2) e. RR /\ 0 <_ ((j + k) / 2)) -> (|_` ((j + k) / 2)) e. NN0)
19		nn0ret 6108	. . . . . . 7 |- ((j + k) e. NN0 -> (j + k) e. RR)
20		rehalfclt 6034	. . . . . . 7 |- ((j + k) e. RR -> ((j + k) / 2) e. RR)
21	19, 20	syl 10	. . . . . 6 |- ((j + k) e. NN0 -> ((j + k) / 2) e. RR)
22		nn0ge0t 6117	. . . . . . 7 |- ((j + k) e. NN0 -> 0 <_ (j + k))
23		halfnneg2t 6038	. . . . . . . 8 |- ((j + k) e. RR -> (0 <_ (j + k) <-> 0 <_ ((j + k) / 2)))
24	19, 23	syl 10	. . . . . . 7 |- ((j + k) e. NN0 -> (0 <_ (j + k) <-> 0 <_ ((j + k) / 2)))
25	22, 24	mpbid 195	. . . . . 6 |- ((j + k) e. NN0 -> 0 <_ ((j + k) / 2))
26	18, 21, 25	sylanc 471	. . . . 5 |- ((j + k) e. NN0 -> (|_` ((j + k) / 2)) e. NN0)
27		facclt 6940	. . . . 5 |- ((|_` ((j + k) / 2)) e. NN0 -> (!` (|_` ((j + k) / 2))) e. NN)
28	26, 27	syl 10	. . . 4 |- ((j + k) e. NN0 -> (!` (|_` ((j + k) / 2))) e. NN)
29		nnret 5929	. . . 4 |- ((!` (|_` ((j + k) / 2))) e. NN -> (!` (|_` ((j + k) / 2))) e. RR)
30	28, 29	syl 10	. . 3 |- ((j + k) e. NN0 -> (!` (|_` ((j + k) / 2))) e. RR)
31	17, 30	syl 10	. 2 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` (|_` ((j + k) / 2))) e. RR)
32		nnmulclt 5941	. . . 4 |- (((!` j) e. NN /\ (!` k) e. NN) -> ((!` j) x. (!` k)) e. NN)
33		facclt 6940	. . . . 5 |- (j e. NN0 -> (!` j) e. NN)
34	13, 33	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` j) e. NN)
35		facclt 6940	. . . . 5 |- (k e. NN0 -> (!` k) e. NN)
36	16, 35	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` k) e. NN)
37	32, 34, 36	sylanc 471	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) e. NN)
38		nnret 5929	. . 3 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) e. RR)
39	37, 38	syl 10	. 2 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) e. RR)
40		facwordit 6944	. . . 4 |- ((S e. NN0 /\ (|_` ((j + k) / 2)) e. NN0 /\ S <_ (|_` ((j + k) / 2))) -> (!` S) <_ (!` (|_` ((j + k) / 2))))
41	4, 40	mp3an1 903	. . 3 |- (((|_` ((j + k) / 2)) e. NN0 /\ S <_ (|_` ((j + k) / 2))) -> (!` S) <_ (!` (|_` ((j + k) / 2))))
42	17, 19	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (j + k) e. RR)
43	42, 20	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((j + k) / 2) e. RR)
44	17, 22	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> 0 <_ (j + k))
45	42, 23	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (0 <_ (j + k) <-> 0 <_ ((j + k) / 2)))
46	44, 45	mpbid 195	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> 0 <_ ((j + k) / 2))
47	18, 43, 46	sylanc 471	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (|_` ((j + k) / 2)) e. NN0)
48	1	nnre 5931	. . . . . . . 8 |- N e. RR
49		1re 5435	. . . . . . . 8 |- 1 e. RR
50	48, 49	readdcl 5334	. . . . . . 7 |- (N + 1) e. RR
51		2re 5979	. . . . . . 7 |- 2 e. RR
52		2ne0 5990	. . . . . . 7 |- 2 =/= 0
53	50, 51, 52	redivcl 5798	. . . . . 6 |- ((N + 1) / 2) e. RR
54		flwordit 6237	. . . . . 6 |- ((((N + 1) / 2) e. RR /\ ((j + k) / 2) e. RR /\ ((N + 1) / 2) <_ ((j + k) / 2)) -> (|_` ((N + 1) / 2)) <_ (|_` ((j + k) / 2)))
55	53, 54	mp3an1 903	. . . . 5 |- ((((j + k) / 2) e. RR /\ ((N + 1) / 2) <_ ((j + k) / 2)) -> (|_` ((N + 1) / 2)) <_ (|_` ((j + k) / 2)))
56	1	efaddlem14 7351	. . . . . 6 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (N + 1) <_ (j + k))
57		2pos 5989	. . . . . . . . 9 |- 0 < 2
58		lediv1tOLD 5852	. . . . . . . . 9 |- ((((N + 1) e. RR /\ (j + k) e. RR /\ 2 e. RR) /\ 0 < 2) -> ((N + 1) <_ (j + k) <-> ((N + 1) / 2) <_ ((j + k) / 2)))
59	57, 58	mpan2 696	. . . . . . . 8 |- (((N + 1) e. RR /\ (j + k) e. RR /\ 2 e. RR) -> ((N + 1) <_ (j + k) <-> ((N + 1) / 2) <_ ((j + k) / 2)))
60	50, 51, 59	mp3an13 907	. . . . . . 7 |- ((j + k) e. RR -> ((N + 1) <_ (j + k) <-> ((N + 1) / 2) <_ ((j + k) / 2)))
61	42, 60	syl 10	. . . . . 6 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((N + 1) <_ (j + k) <-> ((N + 1) / 2) <_ ((j + k) / 2)))
62	56, 61	mpbid 195	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((N + 1) / 2) <_ ((j + k) / 2))
63	55, 43, 62	sylanc 471	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (|_` ((N + 1) / 2)) <_ (|_` ((j + k) / 2)))
64	63, 2	syl5eqbr 2648	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> S <_ (|_` (