Theorem efaddlem20 7316

Description: Lemma for efadd 7325. Further upper bound for the summation terms on the right-hand side of efaddlem6 7302.

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
efaddlem20	|- ((N^2) x. ((T^S) / (!` S))) <_ (((S^2) x. ((4 x. T)^S)) / (!` S))

Proof of Theorem efaddlem20

Step	Hyp	Ref	Expression
1		efaddlem17.1	. . . . . . 7 |- N e. NN
2	1	nnsqcl 6605	. . . . . 6 |- (N^2) e. NN
3	2	nnre 5889	. . . . 5 |- (N^2) e. RR
4		2re 5936	. . . . . . 7 |- 2 e. RR
5		efaddlem17.4	. . . . . . . . 9 |- S = (|_` ((N + 1) / 2))
6	1, 5	efaddlem8 7304	. . . . . . . 8 |- S e. NN
7	6	nnre 5889	. . . . . . 7 |- S e. RR
8	4, 7	remulcl 5318	. . . . . 6 |- (2 x. S) e. RR
9	8	resqcl 6568	. . . . 5 |- ((2 x. S)^2) e. RR
10		efaddlem17.2	. . . . . . . . 9 |- A e. CC
11		efaddlem17.3	. . . . . . . . 9 |- B e. CC
12		efaddlem17.5	. . . . . . . . 9 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
13	10, 11, 12	efaddlem7 7303	. . . . . . . 8 |- T e. NN
14	13	nnre 5889	. . . . . . 7 |- T e. RR
15	6	nnnn0 6064	. . . . . . 7 |- S e. NN0
16		reexpclt 6525	. . . . . . 7 |- ((T e. RR /\ S e. NN0) -> (T^S) e. RR)
17	14, 15, 16	mp2an 696	. . . . . 6 |- (T^S) e. RR
18		facclt 6892	. . . . . . . 8 |- (S e. NN0 -> (!` S) e. NN)
19	15, 18	ax-mp 7	. . . . . . 7 |- (!` S) e. NN
20	19	nnre 5889	. . . . . 6 |- (!` S) e. RR
21		facne0t 6893	. . . . . . 7 |- (S e. NN0 -> (!` S) =/= 0)
22	15, 21	ax-mp 7	. . . . . 6 |- (!` S) =/= 0
23	17, 20, 22	redivcl 5764	. . . . 5 |- ((T^S) / (!` S)) e. RR
24	3, 9, 23	3pm3.2i 817	. . . 4 |- ((N^2) e. RR /\ ((2 x. S)^2) e. RR /\ ((T^S) / (!` S)) e. RR)
25	13	nnnn0 6064	. . . . . . . 8 |- T e. NN0
26		nn0expclt 6522	. . . . . . . 8 |- ((T e. NN0 /\ S e. NN0) -> (T^S) e. NN0)
27	25, 15, 26	mp2an 696	. . . . . . 7 |- (T^S) e. NN0
28	27	nn0ge0 6075	. . . . . 6 |- 0 <_ (T^S)
29	19	nngt0 5908	. . . . . 6 |- 0 < (!` S)
30	17, 20	divge0 5822	. . . . . 6 |- ((0 <_ (T^S) /\ 0 < (!` S)) -> 0 <_ ((T^S) / (!` S)))
31	28, 29, 30	mp2an 696	. . . . 5 |- 0 <_ ((T^S) / (!` S))
32	1	nnre 5889	. . . . . . 7 |- N e. RR
33		0re 5423	. . . . . . . 8 |- 0 e. RR
34	1	nngt0 5908	. . . . . . . 8 |- 0 < N
35	33, 32, 34	ltlei 5564	. . . . . . 7 |- 0 <_ N
36	32, 35	pm3.2i 285	. . . . . 6 |- (N e. RR /\ 0 <_ N)
37		nnzt 6110	. . . . . . . . . 10 |- (N e. NN -> N e. ZZ)
38	1, 37	ax-mp 7	. . . . . . . . 9 |- N e. ZZ
39		flhalft 6201	. . . . . . . . 9 |- (N e. ZZ -> N <_ (2 x. (|_` ((N + 1) / 2))))
40	38, 39	ax-mp 7	. . . . . . . 8 |- N <_ (2 x. (|_` ((N + 1) / 2)))
41	5	opreq2i 3967	. . . . . . . 8 |- (2 x. S) = (2 x. (|_` ((N + 1) / 2)))
42	40, 41	breqtrr 2636	. . . . . . 7 |- N <_ (2 x. S)
43	8, 42	pm3.2i 285	. . . . . 6 |- ((2 x. S) e. RR /\ N <_ (2 x. S))
44		le2sqit 6577	. . . . . 6 |- (((N e. RR /\ 0 <_ N) /\ ((2 x. S) e. RR /\ N <_ (2 x. S))) -> (N^2) <_ ((2 x. S)^2))
45	36, 43, 44	mp2an 696	. . . . 5 |- (N^2) <_ ((2 x. S)^2)
46	31, 45	pm3.2i 285	. . . 4 |- (0 <_ ((T^S) / (!` S)) /\ (N^2) <_ ((2 x. S)^2))
47		lemul1itOLD 5804	. . . 4 |- ((((N^2) e. RR /\ ((2 x. S)^2) e. RR /\ ((T^S) / (!` S)) e. RR) /\ (0 <_ ((T^S) / (!` S)) /\ (N^2) <_ ((2 x. S)^2))) -> ((N^2) x. ((T^S) / (!` S))) <_ (((2 x. S)^2) x. ((T^S) / (!` S))))
48	24, 46, 47	mp2an 696	. . 3 |- ((N^2) x. ((T^S) / (!` S))) <_ (((2 x. S)^2) x. ((T^S) / (!` S)))
49	9	recn 5297	. . . 4 |- ((2 x. S)^2) e. CC
50	17	recn 5297	. . . 4 |- (T^S) e. CC
51	19	nncn 5890	. . . 4 |- (!` S) e. CC
52	49, 50, 51, 22	divass 5719	. . 3 |- ((((2 x. S)^2) x. (T^S)) / (!` S)) = (((2 x. S)^2) x. ((T^S) / (!` S)))
53	48, 52	breqtrr 2636	. 2 |- ((N^2) x. ((T^S) / (!` S))) <_ ((((2 x. S)^2) x. (T^S)) / (!` S))
54		2cn 5937	. . . . . . . 8 |- 2 e. CC
55	6	nncn 5890	. . . . . . . 8 |- S e. CC
56	54, 55	sqmul 6562	. . . . . . 7 |- ((2 x. S)^2) = ((2^2) x. (S^2))
57	54	sqcl 6560	. . . . . . . 8 |- (2^2) e. CC
58	6	nnsqcl 6605	. . . . . . . . 9 |- (S^2) e. NN
59	58	nncn 5890	. . . . . . . 8 |- (S^2) e. CC
60	57, 59	mulcom 5306	. . . . . . 7 |- ((2^2) x. (S^2)) = ((S^2) x. (2^2))
61	56, 60	eqtr 1493	. . . . . 6 |- ((2 x. S)^2) = ((S^2) x. (2^2))
62	61	opreq1i 3966	. . . . 5 |- (((2 x. S)^2) x. (T^S)) = (((S^2) x. (2^2)) x. (T^S))
63	59, 57, 50	mulass 5308	. . . . 5 |- (((S^2) x. (2^2)) x. (T^S)) = ((S^2) x. ((2^2) x. (T^S)))
64	62, 63	eqtr 1493	. . . 4 |- (((2 x. S)^2) x. (T^S)) = ((S^2) x. ((2^2) x. (T^S)))
65	4	resqcl 6568	. . . . . . 7 |- (2^2) e. RR
66	65, 17	remulcl 5318	. . . . . 6 |- ((2^2) x. (T^S)) e. RR
67		4re 5939	. . . . . . . 8 |- 4 e. RR
68	67, 14	remulcl 5318	. . . . . . 7 |- (4 x. T) e. RR
69		reexpclt 6525	. . . . . . 7 |- (((4 x. T) e. RR /\ S e. NN0) -> ((4 x. T)^S) e. RR)
70	68, 15, 69	mp2an 696	. . . . . 6 |- ((4 x. T)^S) e. RR
71	58	nnre 5889	. . . . . 6 |- (S^2) e. RR
72	66, 70, 71	3pm3.2i 817	. . . . 5 |- (((2^2) x. (T^S)) e. RR /\ ((4 x. T)^S) e. RR /\ (S^2) e. RR)
73	58	nngt0 5908	. . . . . . 7 |- 0 < (S^2)
74	33, 71, 73	ltlei 5564	. . . . . 6 |- 0 <_ (S^2)
75		reexpclt 6525	. . . . . . . . . 10 |- ((4 e. RR /\ S e. NN0) -> (4^S) e. RR)
76	67, 15, 75	mp2an 696	. . . . . . . . 9 |- (4^S) e. RR
77	65, 76, 17	3pm3.2i 817	. . . . . . . 8 |- ((2^2) e. RR /\ (4^S) e. RR /\ (T^S) e. RR)
78		sq2 6583	. . . . . . . . . . 11 |- (2^2) = 4
79	67	recn 5297	. . . . . . . . . . . 12 |- 4 e. CC
80		exp1t 6518	. . . . . . . . . . . 12 |- (4 e. CC -> (4^1) = 4)
81	79, 80	ax-mp 7	. . . . . . . . . . 11 |- (4^1) = 4
82	78, 81	eqtr4 1496	. . . . . . . . . 10 |- (2^2) = (4^1)
83		1nn0 6071	. . . . . . . . . . . 12 |- 1 e. NN0
84	67, 83, 15	3pm3.2i 817	. . . . . . . . . . 11 |- (4 e. RR /\ 1 e. NN0 /\ S e. NN0)
85		3re 5938	. . . . . . . . . . . . . . 15 |- 3 e. RR
86		3pos 5948	. . . . . . . . . . . . . . 15 |- 0 < 3
87	33, 85, 86	ltlei 5564	. . . . . . . . . . . . . 14 |- 0 <_ 3
88		1re 5418	. . . . . . . . . . . . . . 15 |- 1 e. RR
89		addge02t 5656	. . . . . . . . . . . . . . 15 |- ((1 e. RR /\ 3 e. RR) -> (0 <_ 3 <-> 1 <_ (3 + 1)))
90	88, 85, 89	mp2an 696	. . . . . . . . . . . . . 14 |- (0 <_ 3 <-> 1 <_ (3 + 1))
91	87, 90	mpbi 189	. . . . . . . . . . . . 13 |- 1 <_ (3 + 1)
92		df-4 5929	. . . . . . . . . . . . 13 |- 4 = (3 + 1)
93	91, 92	breqtrr 2636	. . . . . . . . . . . 12 |- 1 <_ 4
94		nnge1t 5901	. . . . . . . . . . . . 13 |- (S e. NN -> 1 <_ S)
95	6, 94	ax-mp 7	. . . . . . . . . . . 12 |- 1 <_ S
96	93, 95	pm3.2i 285	. . . . . . . . . . 11 |- (1 <_ 4 /\ 1 <_ S)
97		expwordit 6548	. . . . . . . . . . 11 |- (((4 e. RR /\ 1 e. NN0 /\ S e. NN0) /\ (1 <_ 4 /\ 1 <_ S)) -> (4^1) <_ (4^S))
98	84, 96, 97	mp2an 696	. . . . . . . . . 10 |- (4^1) <_ (4^S)
99	82, 98	eqbrtr 2630	. . . . . . . . 9 |- (2^2) <_ (4^S)
100	28, 99	pm3.2i 285	. . . . . . . 8 |- (0 <_ (T^S) /\ (2^2) <_ (4^S))
101		lemul1itOLD 5804	. . . . . . . 8 |- ((((2^2) e. RR /\ (4^S) e. RR /\ (T^S) e. RR) /\ (0 <_ (T^S) /\ (2^2) <_ (4^S))) -> ((2^2) x. (T^S)) <_ ((4^S) x. (T^S)))
102	77, 100, 101	mp2an 696	. . . . . . 7 |- ((2^2) x. (T^S)) <_ ((4^S) x. (T^S))
103	13	nncn 5890	. . . . . . . 8 |- T e. CC
104		mulexpt 6539	. . . . . . . 8 |- ((4 e. CC /\ T e. CC /\ S e. NN0) -> ((4 x. T)^S) = ((4^S) x. (T^S)))
105	79, 103, 15, 104	mp3an 915	. . . . . . 7 |- ((4 x. T)^S