Theorem efaddlem17 7354

Description: Lemma for efadd 7366. An upper bound for the summation terms on the right-hand side of efaddlem6 7343 that is independent of j and k.

Hypotheses

Ref	Expression
efaddlem17.1	|- N e. NN
efaddlem17.2	|- A e. CC
efaddlem17.3	|- B e. CC
efaddlem17.4	|- S = (|_` ((N + 1) / 2))
efaddlem17.5	|- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)

Assertion

Ref	Expression
efaddlem17	|- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ ((T^S) / (!` S)))

Distinct variable group:   j,k,N

Proof of Theorem efaddlem17

Step	Hyp	Ref	Expression
1		absdivt 6860	. . . 4 |- ((((A^j) x. (B^k)) e. CC /\ ((!` j) x. (!` k)) e. CC /\ ((!` j) x. (!` k)) =/= 0) -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) = ((abs` ((A^j) x. (B^k))) / (abs` ((!` j) x. (!` k)))))
2		axmulcl 5273	. . . . . 6 |- (((A^j) e. CC /\ (B^k) e. CC) -> ((A^j) x. (B^k)) e. CC)
3		efaddlem17.2	. . . . . . 7 |- A e. CC
4		expclt 6581	. . . . . . 7 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
5	3, 4	mpan 695	. . . . . 6 |- (j e. NN0 -> (A^j) e. CC)
6		efaddlem17.3	. . . . . . 7 |- B e. CC
7		expclt 6581	. . . . . . 7 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
8	6, 7	mpan 695	. . . . . 6 |- (k e. NN0 -> (B^k) e. CC)
9	2, 5, 8	syl2an 454	. . . . 5 |- ((j e. NN0 /\ k e. NN0) -> ((A^j) x. (B^k)) e. CC)
10		elfznnt 6494	. . . . . . 7 |- (j e. (1...N) -> j e. NN)
11	10	adantr 389	. . . . . 6 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN)
12		nnnn0t 6106	. . . . . 6 |- (j e. NN -> j e. NN0)
13	11, 12	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN0)
14		efaddlem17.1	. . . . . . 7 |- N e. NN
15	14	efaddlem2 7339	. . . . . 6 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN)
16		nnnn0t 6106	. . . . . 6 |- (k e. NN -> k e. NN0)
17	15, 16	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN0)
18	9, 13, 17	sylanc 471	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((A^j) x. (B^k)) e. CC)
19		nnmulclt 5941	. . . . . . 7 |- (((!` j) e. NN /\ (!` k) e. NN) -> ((!` j) x. (!` k)) e. NN)
20		facclt 6940	. . . . . . 7 |- (j e. NN0 -> (!` j) e. NN)
21		facclt 6940	. . . . . . 7 |- (k e. NN0 -> (!` k) e. NN)
22	19, 20, 21	syl2an 454	. . . . . 6 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. NN)
23	22, 13, 17	sylanc 471	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) e. NN)
24		nncnt 5930	. . . . 5 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) e. CC)
25	23, 24	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) e. CC)
26		nnne0t 5949	. . . . 5 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) =/= 0)
27	23, 26	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) =/= 0)
28	1, 18, 25, 27	syl3anc 858	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) = ((abs` ((A^j) x. (B^k))) / (abs` ((!` j) x. (!` k)))))
29		absidt 6862	. . . . 5 |- ((((!` j) x. (!` k)) e. RR /\ 0 <_ ((!` j) x. (!` k))) -> (abs` ((!` j) x. (!` k))) = ((!` j) x. (!` k)))
30		nnret 5929	. . . . . 6 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) e. RR)
31	23, 30	syl 10	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((!` j) x. (!` k)) e. RR)
32		nnnn0t 6106	. . . . . 6 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) e. NN0)
33		nn0ge0t 6117	. . . . . 6 |- (((!` j) x. (!` k)) e. NN0 -> 0 <_ ((!` j) x. (!` k)))
34	23, 32, 33	3syl 20	. . . . 5 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> 0 <_ ((!` j) x. (!` k)))
35	29, 31, 34	sylanc 471	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` ((!` j) x. (!` k))) = ((!` j) x. (!` k)))
36	35	opreq2d 3976	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((abs` ((A^j) x. (B^k))) / (abs` ((!` j) x. (!` k)))) = ((abs` ((A^j) x. (B^k))) / ((!` j) x. (!` k))))
37	28, 36	eqtrd 1507	. 2 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) = ((abs` ((A^j) x. (B^k))) / ((!` j) x. (!` k))))
38		lediv12it 5896	. . 3 |- (((((abs` ((A^j) x. (B^k))) e. RR /\ (T^S) e. RR) /\ (0 <_ (abs` ((A^j) x. (B^k))) /\ (abs` ((A^j) x. (B^k))) <_ (T^S))) /\ (((!` S) e. RR /\ ((!` j) x. (!` k)) e. RR) /\ (0 < (!` S) /\ (!` S) <_ ((!` j) x. (!` k))))) -> ((abs` ((A^j) x. (B^k))) / ((!` j) x. (!` k))) <_ ((T^S) / (!` S)))
39		absclt 6833	. . . . 5 |- (((A^j) x. (B^k)) e. CC -> (abs` ((A^j) x. (B^k))) e. RR)
40	18, 39	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` ((A^j) x. (B^k))) e. RR)
41		efaddlem17.5	. . . . . . 7 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
42	3, 6, 41	efaddlem7 7344	. . . . . 6 |- T e. NN
43	42	nnre 5931	. . . . 5 |- T e. RR
44		efaddlem17.4	. . . . . . 7 |- S = (|_` ((N + 1) / 2))
45	14, 44	efaddlem8 7345	. . . . . 6 |- S e. NN
46	45	nnnn0 6107	. . . . 5 |- S e. NN0
47		reexpclt 6580	. . . . 5 |- ((T e. RR /\ S e. NN0) -> (T^S) e. RR)
48	43, 46, 47	mp2an 697	. . . 4 |- (T^S) e. RR
49	40, 48	jctir 293	. . 3 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> ((abs` ((A^j) x. (B^k))) e. RR /\ (T^S) e. RR))
50		absge0t 6854	. . . . 5 |- (((A^j) x. (B^k)) e. CC -> 0 <_ (abs` ((A^j) x. (B^k))))
51	18, 50	syl 10	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> 0 <_ (abs` ((A^j) x. (B^k))))
52	14, 3, 6, 44, 41	efaddlem13 7350	. . . 4 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N