Theorem efaddlem12 7291

Description: Lemma for efadd 7308. Further upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7285.

Hypotheses

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

Assertion

Ref	Expression
efaddlem12	|- (((|_` ((abs` A) + 1))^N) x. ((|_` ((abs` B) + 1))^N)) <_ (T^S)

Proof of Theorem efaddlem12

Step	Hyp	Ref	Expression
1		efaddlem12.2	. . . . . . . . 9 |- A e. CC
2	1	abscl 6774	. . . . . . . 8 |- (abs` A) e. RR
3		1re 5407	. . . . . . . 8 |- 1 e. RR
4	2, 3	readdcl 5306	. . . . . . 7 |- ((abs` A) + 1) e. RR
5		flclt 6174	. . . . . . 7 |- (((abs` A) + 1) e. RR -> (|_` ((abs` A) + 1)) e. ZZ)
6	4, 5	ax-mp 7	. . . . . 6 |- (|_` ((abs` A) + 1)) e. ZZ
7	6	zre 6088	. . . . 5 |- (|_` ((abs` A) + 1)) e. RR
8		efaddlem12.3	. . . . . . . . 9 |- B e. CC
9	8	abscl 6774	. . . . . . . 8 |- (abs` B) e. RR
10	9, 3	readdcl 5306	. . . . . . 7 |- ((abs` B) + 1) e. RR
11		flclt 6174	. . . . . . 7 |- (((abs` B) + 1) e. RR -> (|_` ((abs` B) + 1)) e. ZZ)
12	10, 11	ax-mp 7	. . . . . 6 |- (|_` ((abs` B) + 1)) e. ZZ
13	12	zre 6088	. . . . 5 |- (|_` ((abs` B) + 1)) e. RR
14	7, 13	remulcl 5307	. . . 4 |- ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. RR
15		efaddlem12.1	. . . . 5 |- N e. NN
16	15	nnnn0 6054	. . . 4 |- N e. NN0
17		2nn0 6062	. . . . 5 |- 2 e. NN0
18	15	nnre 5879	. . . . . . . 8 |- N e. RR
19	18, 3	readdcl 5306	. . . . . . 7 |- (N + 1) e. RR
20		2re 5926	. . . . . . 7 |- 2 e. RR
21		2ne0 5937	. . . . . . 7 |- 2 =/= 0
22	19, 20, 21	redivcl 5754	. . . . . 6 |- ((N + 1) / 2) e. RR
23		0re 5412	. . . . . . . . 9 |- 0 e. RR
24	16	nn0ge0 6065	. . . . . . . . 9 |- 0 <_ N
25		letrp1t 5772	. . . . . . . . 9 |- ((0 e. RR /\ N e. RR /\ 0 <_ N) -> 0 <_ (N + 1))
26	23, 18, 24, 25	mp3an 913	. . . . . . . 8 |- 0 <_ (N + 1)
27		2cn 5927	. . . . . . . . 9 |- 2 e. CC
28	27	mul02 5404	. . . . . . . 8 |- (0 x. 2) = 0
29	19	recn 5286	. . . . . . . . 9 |- (N + 1) e. CC
30	27, 29, 21	divcan1 5686	. . . . . . . 8 |- (((N + 1) / 2) x. 2) = (N + 1)
31	26, 28, 30	3brtr4 2633	. . . . . . 7 |- (0 x. 2) <_ (((N + 1) / 2) x. 2)
32		2pos 5936	. . . . . . . 8 |- 0 < 2
33	23, 22, 20	lemul1 5791	. . . . . . . 8 |- (0 < 2 -> (0 <_ ((N + 1) / 2) <-> (0 x. 2) <_ (((N + 1) / 2) x. 2)))
34	32, 33	ax-mp 7	. . . . . . 7 |- (0 <_ ((N + 1) / 2) <-> (0 x. 2) <_ (((N + 1) / 2) x. 2))
35	31, 34	mpbir 190	. . . . . 6 |- 0 <_ ((N + 1) / 2)
36		flge0nn0t 6185	. . . . . 6 |- ((((N + 1) / 2) e. RR /\ 0 <_ ((N + 1) / 2)) -> (|_` ((N + 1) / 2)) e. NN0)
37	22, 35, 36	mp2an 695	. . . . 5 |- (|_` ((N + 1) / 2)) e. NN0
38	17, 37	nn0mulcl 6069	. . . 4 |- (2 x. (|_` ((N + 1) / 2))) e. NN0
39	14, 16, 38	3pm3.2i 816	. . 3 |- (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. RR /\ N e. NN0 /\ (2 x. (|_` ((N + 1) / 2))) e. NN0)
40		elnnz1 6102	. . . . . . 7 |- ((|_` ((abs` A) + 1)) e. NN <-> ((|_` ((abs` A) + 1)) e. ZZ /\ 1 <_ (|_` ((abs` A) + 1))))
41	1	absge0 6775	. . . . . . . . 9 |- 0 <_ (abs` A)
42		addge02t 5646	. . . . . . . . . 10 |- ((1 e. RR /\ (abs` A) e. RR) -> (0 <_ (abs` A) <-> 1 <_ ((abs` A) + 1)))
43	3, 2, 42	mp2an 695	. . . . . . . . 9 |- (0 <_ (abs` A) <-> 1 <_ ((abs` A) + 1))
44	41, 43	mpbi 189	. . . . . . . 8 |- 1 <_ ((abs` A) + 1)
45		1z 6106	. . . . . . . . 9 |- 1 e. ZZ
46		flget 6178	. . . . . . . . 9 |- ((((abs` A) + 1) e. RR /\ 1 e. ZZ) -> (1 <_ ((abs` A) + 1) <-> 1 <_ (|_` ((abs` A) + 1))))
47	4, 45, 46	mp2an 695	. . . . . . . 8 |- (1 <_ ((abs` A) + 1) <-> 1 <_ (|_` ((abs` A) + 1)))
48	44, 47	mpbi 189	. . . . . . 7 |- 1 <_ (|_` ((abs` A) + 1))
49	40, 6, 48	mpbir2an 728	. . . . . 6 |- (|_` ((abs` A) + 1)) e. NN
50		elnnz1 6102	. . . . . . 7 |- ((|_` ((abs` B) + 1)) e. NN <-> ((|_` ((abs` B) + 1)) e. ZZ /\ 1 <_ (|_` ((abs` B) + 1))))
51	8	absge0 6775	. . . . . . . . 9 |- 0 <_ (abs` B)
52		addge02t 5646	. . . . . . . . . 10 |- ((1 e. RR /\ (abs` B) e. RR) -> (0 <_ (abs` B) <-> 1 <_ ((abs` B) + 1)))
53	3, 9, 52	mp2an 695	. . . . . . . . 9 |- (0 <_ (abs` B) <-> 1 <_ ((abs` B) + 1))
54	51, 53	mpbi 189	. . . . . . . 8 |- 1 <_ ((abs` B) + 1)
55		flget 6178	. . . . . . . . 9 |- ((((abs` B) + 1) e. RR /\ 1 e. ZZ) -> (1 <_ ((abs` B) + 1) <-> 1 <_ (|_` ((abs` B) + 1))))
56	10, 45, 55	mp2an 695	. . . . . . . 8 |- (1 <_ ((abs` B) + 1) <-> 1 <_ (|_` ((abs` B) + 1)))
57	54, 56	mpbi 189	. . . . . . 7 |- 1 <_ (|_` ((abs` B) + 1))
58	50, 12, 57	mpbir2an 728	. . . . . 6 |- (|_` ((abs` B) + 1)) e. NN
59		nnmulclt 5889	. . . . . 6 |- (((|_` ((abs` A) + 1)) e. NN /\ (|_` ((abs` B) + 1)) e. NN) -> ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. NN)
60	49, 58, 59	mp2an 695	. . . . 5 |- ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. NN
61		nnge1t 5891	. . . . 5 |- (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. NN -> 1 <_ ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))))
62	60, 61	ax-mp 7	. . . 4 |- 1 <_ ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))
63		nnzt 6100	. . . . . 6 |- (N e. NN -> N e. ZZ)
64	15, 63	ax-mp 7	. . . . 5 |- N e. ZZ
65		flhalft 6189	. . . . 5 |- (N e. ZZ -> N <_ (2 x. (|_` ((N + 1) / 2))))
66	64, 65	ax-mp 7	. . . 4 |- N <_ (2 x. (|_` ((N + 1) / 2)))
67	62, 66	pm3.2i 285	. . 3 |- (1 <_ ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) /\ N <_ (2 x. (|_` ((N + 1) / 2))))
68		expwordit 6534	. . 3 |- (((((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) e. RR /\ N e. NN0 /\ (2 x. (|_` ((N + 1) / 2))) e. NN0) /\ (1 <_ ((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1))) /\ N <_ (2 x. (|_` ((N + 1) / 2))))) -> (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^N) <_ (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^(2 x. (|_` ((N + 1) / 2)))))
69	39, 67, 68	mp2an 695	. 2 |- (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^N) <_ (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^(2 x. (|_` ((N + 1) / 2))))
70		zcnt 6087	. . . 4 |- ((|_` ((abs` A) + 1)) e. ZZ -> (|_` ((abs` A) + 1)) e. CC)
71	6, 70	ax-mp 7	. . 3 |- (|_` ((abs` A) + 1)) e. CC
72		zcnt 6087	. . . 4 |- ((|_` ((abs` B) + 1)) e. ZZ -> (|_` ((abs` B) + 1)) e. CC)
73	12, 72	ax-mp 7	. . 3 |- (|_` ((abs` B) + 1)) e. CC
74		mulexpt 6525	. . 3 |- (((|_` ((abs` A) + 1)) e. CC /\ (|_` ((abs` B) + 1)) e. CC /\ N e. NN0) -> (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^N) = ((