Theorem efaddlem15 7302

Description: Lemma for efadd 7316. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 7293. The key theorem used is facavgt 6900, 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 7295	. . . . . 6 |- S e. NN
4	3	nnnn0 6062	. . . . 5 |- S e. NN0
5		facclt 6885	. . . . 5 |- (S e. NN0 -> (!` S) e. NN)
6	4, 5	ax-mp 7	. . . 4 |- (!` S) e. NN
7	6	nnre 5887	. . 3 |- (!` S) e. RR
8	7	a1i 8	. 2 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (!` S) e. RR)
9		nn0addclt 6075	. . . 4 |- ((j e. NN0 /\ k e. NN0) -> (j + k) e. NN0)
10		elfznnt 6434	. . . . . 6 |- (j e. (1...N) -> j e. NN)
11		nnnn0t 6061	. . . . . 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 7289	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN)
15		nnnn0t 6061	. . . . 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 6193	. . . . . 6 |- ((((j + k) / 2) e. RR /\ 0 <_ ((j + k) / 2)) -> (|_` ((j + k) / 2)) e. NN0)
19		nn0ret 6063	. . . . . . 7 |- ((j + k) e. NN0 -> (j + k) e. RR)
20		rehalfclt 5989	. . . . . . 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 6072	. . . . . . 7 |- ((j + k) e. NN0 -> 0 <_ (j + k))
23		halfnneg2t 5993	. . . . . . . 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 6885	. . . . 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 5885	. . . 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 5897	. . . 4 |- (((!` j) e. NN /\ (!` k) e. NN) -> ((!` j) x. (!` k)) e. NN)
33		facclt 6885	. . . . 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 6885	. . . . 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 5885	. . 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 6889	. . . 4 |- ((S e. NN0 /\ (|_` ((j + k) / 2)) e. NN0 /\ S <_ (|_` ((j + k) / 2))) -> (!` S) <_ (!` (|_` ((j + k) / 2))))
41	4, 40	mp3an1 901	. . 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 5887	. . . . . . . 8 |- N e. RR
49		1re 5415	. . . . . . . 8 |- 1 e. RR
50	48, 49	readdcl 5314	. . . . . . 7 |- (N + 1) e. RR
51		2re 5934	. . . . . . 7 |- 2 e. RR
52		2ne0 5945	. . . . . . 7 |- 2 =/= 0
53	50, 51, 52	redivcl 5762	. . . . . 6 |- ((N + 1) / 2) e. RR
54		flwordit 6191	. . . . . 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 901	. . . . 5 |- ((((j + k) / 2) e. RR /\ ((N + 1) / 2) <_ ((j + k) / 2)) -> (|_` ((N + 1) / 2)) <_ (|_` ((j + k) / 2)))
56	1	efaddlem14 7301	. . . . . 6 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (N + 1) <_ (j + k))
57		2pos 5944	. . . . . . . . 9 |- 0 < 2
58		lediv1t 5814	. . . . . . . . 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 695	. . . . . . . 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 905	. . . . . . 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 2643	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> S <_ (|_` ((