Theorem efaddlem22 7301

Description: Lemma for efadd 7308. The final upper bound for the summation on the right-hand side of efaddlem6 7285. The key theorem used is faclbnd5 6890, which shows that the factorial grows faster than powers. As the number of terms N grows to infinity, the sum shrinks to zero, since R is independent of N.

Hypotheses

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

Assertion

Ref	Expression
efaddlem22	|- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) < ((2 x. R) / N)

Distinct variable groups:   j,k,N   S,j,k   T,j,k

Proof of Theorem efaddlem22

Step	Hyp	Ref	Expression
1		efaddlem22.1	. . . . . 6 |- N e. NN
2		efaddlem22.2	. . . . . 6 |- A e. CC
3		efaddlem22.3	. . . . . 6 |- B e. CC
4		efaddlem22.4	. . . . . 6 |- S = (|_` ((N + 1) / 2))
5		efaddlem22.5	. . . . . 6 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
6	1, 2, 3, 4, 5	efaddlem19 7298	. . . . 5 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S))
7	2, 3, 5	efaddlem7 7286	. . . . . . . . 9 |- T e. NN
8	7	nnre 5879	. . . . . . . 8 |- T e. RR
9	1, 4	efaddlem8 7287	. . . . . . . . 9 |- S e. NN
10	9	nnnn0 6054	. . . . . . . 8 |- S e. NN0
11		reexpclt 6512	. . . . . . . 8 |- ((T e. RR /\ S e. NN0) -> (T^S) e. RR)
12	8, 10, 11	mp2an 695	. . . . . . 7 |- (T^S) e. RR
13		facclt 6877	. . . . . . . . 9 |- (S e. NN0 -> (!` S) e. NN)
14	10, 13	ax-mp 7	. . . . . . . 8 |- (!` S) e. NN
15	14	nnre 5879	. . . . . . 7 |- (!` S) e. RR
16	14	nnne0 5899	. . . . . . 7 |- (!` S) =/= 0
17	12, 15, 16	redivcl 5754	. . . . . 6 |- ((T^S) / (!` S)) e. RR
18	7	nnnn0 6054	. . . . . . . . 9 |- T e. NN0
19		nn0expclt 6509	. . . . . . . . 9 |- ((T e. NN0 /\ S e. NN0) -> (T^S) e. NN0)
20	18, 10, 19	mp2an 695	. . . . . . . 8 |- (T^S) e. NN0
21	20	nn0ge0 6065	. . . . . . 7 |- 0 <_ (T^S)
22	14	nngt0 5898	. . . . . . 7 |- 0 < (!` S)
23	12, 15	divge0 5812	. . . . . . 7 |- ((0 <_ (T^S) /\ 0 < (!` S)) -> 0 <_ ((T^S) / (!` S)))
24	21, 22, 23	mp2an 695	. . . . . 6 |- 0 <_ ((T^S) / (!` S))
25	1, 17, 24	efaddlem16 7295	. . . . 5 |- sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S)) <_ ((N^2) x. ((T^S) / (!` S)))
26	1, 2, 3	efaddlem4 7283	. . . . . 6 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR
27	1, 2, 3, 4, 5	efaddlem18 7297	. . . . . 6 |- sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S)) e. RR
28	1	nnsqcl 6590	. . . . . . . 8 |- (N^2) e. NN
29	28	nnre 5879	. . . . . . 7 |- (N^2) e. RR
30	29, 17	remulcl 5307	. . . . . 6 |- ((N^2) x. ((T^S) / (!` S))) e. RR
31	26, 27, 30	letr 5562	. . . . 5 |- (((abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S)) /\ sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S)) <_ ((N^2) x. ((T^S) / (!` S)))) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ ((N^2) x. ((T^S) / (!` S))))
32	6, 25, 31	mp2an 695	. . . 4 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ ((N^2) x. ((T^S) / (!` S)))
33	1, 2, 3, 4, 5	efaddlem20 7299	. . . 4 |- ((N^2) x. ((T^S) / (!` S))) <_ (((S^2) x. ((4 x. T)^S)) / (!` S))
34	9	nnre 5879	. . . . . . . 8 |- S e. RR
35	34	resqcl 6554	. . . . . . 7 |- (S^2) e. RR
36		4re 5929	. . . . . . . . 9 |- 4 e. RR
37	36, 8	remulcl 5307	. . . . . . . 8 |- (4 x. T) e. RR
38		reexpclt 6512	. . . . . . . 8 |- (((4 x. T) e. RR /\ S e. NN0) -> ((4 x. T)^S) e. RR)
39	37, 10, 38	mp2an 695	. . . . . . 7 |- ((4 x. T)^S) e. RR
40	35, 39	remulcl 5307	. . . . . 6 |- ((S^2) x. ((4 x. T)^S)) e. RR
41	40, 15, 16	redivcl 5754	. . . . 5 |- (((S^2) x. ((4 x. T)^S)) / (!` S)) e. RR
42	26, 30, 41	letr 5562	. . . 4 |- (((abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ ((N^2) x. ((T^S) / (!` S))) /\ ((N^2) x. ((T^S) / (!` S))) <_ (((S^2) x. ((4 x. T)^S)) / (!` S))) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ (((S^2) x. ((4 x. T)^S)) / (!` S)))
43	32, 33, 42	mp2an 695	. . 3 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ (((S^2) x. ((4 x. T)^S)) / (!` S))
44		3nn 5947	. . . . . . 7 |- 3 e. NN
45	44	nnnn0 6054	. . . . . 6 |- 3 e. NN0
46		4nn 5949	. . . . . . 7 |- 4 e. NN
47		nnmulclt 5889	. . . . . . 7 |- ((4 e. NN /\ T e. NN) -> (4 x. T) e. NN)
48	46, 7, 47	mp2an 695	. . . . . 6 |- (4 x. T) e. NN
49		faclbnd5 6890	. . . . . 6 |- ((S e. NN0 /\ 3 e. NN0 /\ (4 x. T) e. NN) -> ((S^3) x. ((4 x. T)^S)) < ((2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3)))) x. (!` S)))
50	10, 45, 48, 49	mp3an 913	. . . . 5 |- ((S^3) x. ((4 x. T)^S)) < ((2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3)))) x. (!` S))
51	35	recn 5286	. . . . . . 7 |- (S^2) e. CC
52	39	recn 5286	. . . . . . 7 |- ((4 x. T)^S) e. CC
53	9	nncn 5880	. . . . . . 7 |- S e. CC
54	51, 52, 53	mul23 5396	. . . . . 6 |- (((S^2) x. ((4 x. T)^S)) x. S) = (((S^2) x. S) x. ((4 x. T)^S))
55		df-3 5918	. . . . . . . . 9 |- 3 = (2 + 1)
56	55	opreq2i 3957	. . . . . . . 8 |- (S^3) = (S^(2 + 1))
57		2nn0 6062	. . . . . . . . 9 |- 2 e. NN0
58		expp1t 6506	. . . . . . . . 9 |- ((S e. CC /\ 2 e. NN0) -> (S^(2 + 1)) = ((S^2) x. S))
59	53, 57, 58	mp2an 695	. . . . . . . 8 |- (S^(2 + 1)) = ((S^2) x. S)
60	56, 59	eqtr 1487	. . . . . . 7 |- (S^3) = ((S^2) x. S)
61	60	opreq1i 3956	. . . . . 6 |- ((S^3) x. ((4 x. T)^S)) = (((S^2) x. S) x. ((4 x. T)^S))
62	54, 61	eqtr4 1490	. . . . 5 |- (((S^2) x. ((4 x. T)^S)) x. S) = ((S^3) x. ((4 x. T)^S))
63		efaddlem22.6	. . . . . 6 |- R = (2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3))))
64	63	opreq1i 3956	. . . . 5 |- (R x. (!` S)) = ((2 x. ((2^(3^2)) x. ((4 x. T)^((